文档信息
- 文献标题： The reference manual for the KQuery language
- 文献作者： The KLEE Team.
- 文献来源：
- 阅读日期： 2016-12-07 21:43:30
- 阅读程度： 速读
- 文档备注 : 不完全,有错,待更新.
简介
约束指的是路径约束,由符号执行工具在执行过程中收集路径分支条件,生成的基于符号表达式的一阶无量词逻辑表达式,通过约束求解可以得到该路径对应的一个真实输入.
KQuery语言是用来描述约束表达式,作为Kleaver约束求解的输入.该语言的语法使用BNF范式描述.
巴克斯范式(BNF范式)
巴科斯范式的内容
- 在双引号中的字("word")代表着这些字符本身。而double_quote用来代表双引号。
- 在双引号外的字（有可能有下划线）代表着语法部分。
- 尖括号( < > )内包含的为必选项。
- 方括号( [ ] )内包含的为可选项。
- 大括号( { } )内包含的为可重复0至无数次的项。
- 竖线( | )表示在其左右两边任选一项，相当于"OR"的意思。
- ::= 是“被定义为”的意思。
巴科斯范式示例,这是用BNF来定义的Java语言中的For语句的实例：
FOR_STATEMENT ::=
"for" "(" ( variable_declaration ";") | ( expression ";" ) | ";" ) [ expression ] ";" [ expression ] ")"
statement
约束文件的生成
- klee中和约束生成相关的参数为:
- -use-query-log=all:pc
- -use-query-log=all:smt2
- -use-query-log=solver:pc
- -use-query-log=solver:smt2
其中,pc表示记录格式为KQuery,smt2表示记录格式为SMT-LIBv2,all表示生成的约束全记录,而solver则表示只记录交于约束求解器求解的约束.
- 生成约束的流程一般为
$ clang -I ../../include -emit-llvm -c -g get_sign.c
$ klee -use-query-log=all:pc get_sign.bc
上述命令之后,在生成的结果文件中,记录约束信息的文件名为all-queriers.pc
具体约束文件的解析
- KQuery文件结构
kquery = { array-declaration | query-command }
Array Declarations: 用于描述随后表达式中的bit向量数组
Query Commands: 提交给约束求解器的约束查询,包括:约束集,查询表达式,可选表达式,需要计算的数组.
注释用"#""表示
- 数组描述(arrays)
- 语法:
array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range "=" array-initializer
array-initializer = "symbolic" | "[" number-list "]"
number-list = number | number "," number-list
- 例子:
array foo[10] : w32 -> w8 = symbolic # 具有10个元素的符号数组
array foo[] : w8 -> w1 = [ true, false, false, true ] # 具有4个布尔值的数组
疑问:domain,range,->,分别是什么意思?
- query命令(query-command):
- 语法
query-command = "(" "query" constraint-list query-expression [ eval-expr-list [ eval-array-list ] ] ")"
query-expression = expression
constraint-list = "[" { expression } "]"
eval-expr-list = "[" { expression } "]"
eval-array-list = "[" { identifier } "]"
- 例子
(query [] false)
(query [(Eq w8 (Read w8 0 mem) 10)] false [] [ mem ])
一般一个求解的查询命令包括5个元素:元素1为关键字"query";元素2个由[]包裹,表示一个待解约束表达式列表 ;元素3表示期望元素2合取后不满足的布尔值(即求得的解使得元素2与元素3不等);元素4由[]包裹,表示约束求解过程中,要顺带计算的表达式列表,如果元素5不存在,元素4可以不存在;如果元素5存在,又没有什么表达式需要计算时,此处应为[];元素5由[]包裹,表示元素2中需要求解的变量列表.
- KQuery文件样例
# Query 1 -- Type: InitialValues, Instructions: 13
array a[4] : w32 -> w8 = symbolic
(query [] (Eq false
(Eq 21
(ReadLSB w32 0 a))) []
[a])
# OK -- Elapsed: 7.439852e-04
# Solvable: true
# a = [21,0,0,0]
计算结果:a = [21,0,0,0], 这是一个w32类型的数,[]内每一个数字是8位的十进制表示,大尾存储(高字节放在低地址),a=21;假如a=[3,1,0,0],那么a=1*2^8+3=259
KQuery语法
- 数据类型
- 语法:
type = "w[0-9]+"
- 例子:
w32 # 32bit位宽的数据
- 比较
- 语法
comparison-expr-kind = ( "Eq" | "Ne" | "Ult" | "Ule" | "Ugt" | "Uge" | "Slt" | "Sle" | "Sgt" | "Sge" )
expression = "(" comparison-expr-kind [ type ] expression expression ")"
# Eq 等于;Ne 不等于;Ult 无符号小于;Ule;无符号小于等于;Ugt 无符号大于;Uge 无符号大于等于
- 运算操作
arithmetic-expr-kind = ( "Add" | "Sub" | "Mul" | "UDiv" | "URem" | "SDiv" | "SRem" )
# 加,减,乘,无符号除,无符号取余,有符号除,有符号取余
expression = "(" arithmetic-expr-kind type expression expression ")"
- 比特运算
expression = "(" "Not" [ type ] expression ")"
bitwise-expr-kind = ( "And" | "Or" | "Xor" | "Shl" | "LShr" | "AShr" )
expression = "(" bitwise-expr-kind type expression expression ")"
# 与,或,异或,逻辑左移,逻辑右移,算术右移
- 二元向量操作
expression = "(" "Concat" [type] msb-expression lsb-expression ")" # 将lsb连接到msb后面
expression = "(" "Extract" type offset-number child-expression ")" #从child-expression中的第offset-number个位置提取出type位.
expression = "(" "ZExt" type child-expression ")" #ZExt evaluates to the lowest type bits of child-expression, with undefined bits set to zero.
expression = "(" "SExt" type input-expression ")"
- 特殊表达式
expression = "(" "Read" type index-expression version ")"
expression = "(" "Select" type cond-expression true-expression false-expression ")"
- 宏表达式
expression = "(" "Neg" [ type ] expression ")"
expression = "(" "ReadLSB" type index-expression version ")"
expression = "(" "ReadMSB" type index-expression version ")"
