[笔记] Z3prover 学习记录

• z3作为微软开发的求解器，其提供的接口在很多应用程序和编程语言中都可以使用。
  > z3prover在CHAINSAW和NAVEX中均有使用
• 在这里关键的作用是想要配和CodeQL，通过CodeQL提取路径约束，然后用Z3求解约束
• 其实关于如何用CodeQL提取出可以作为z3输入的约束还是一头雾水...但是这不妨碍先学习z3的使用，说不定可以找到一些灵感完成两者的结合。（应该会有办法的，要不这条研究路线就断了）
• 后期可能需要造一些轮子，这么说来还是需要花挺多时间的（尤其是假期即将结束，需要挺多时间复习开学期考功课）
• 官方使用文档：https://rise4fun.com/z3/tutorialcontent/guide
• z3py功能手册：https://z3prover.github.io/api/html/namespacez3py.html
• z3py使用文档：https://ericpony.github.io/z3py-tutorial/guide-examples.htm
  > 如果二进制版的z3不便于后期结合，还需要花时间学下z3py
• z3所使用的语法标准：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
• 最后，关于细节本文记录得不是很多，所以需要一些基础来阅读

环境安装

编译好的二进制版

1. Github下载最新版：https://github.com/Z3Prover/z3/releases
   
2. 解压后将其中的bin目录添加到环境变量（Unix-like系统可以添加软连接到/usr/bin中）
3. z3 <filename> 使用

z3py

1. pip install z3-prover
2. from z3 import * 使用
   > 注意在z3py中，很多语句被封装成了对象/类方法，但是基本求解逻辑还是一样的，取决于后期打算采用何种形式

基本语法

指令结构

z3指令有一套自己的结构，一般称为三地址码，其遵循的标准在引言中有链接。
基本的构成为 操作符 操作数1 操作数2

常量(constants)和函数(functions)

这是z3指令中最常见的两种结构，然而本质上常量只是作为一个没有参数的函数，其求解结果也以函数结构所表现。

(declare-fun f (Int) Int) ; 这里f是接受Int类型的函数
(declare-fun a () Int) ; a可以看成常量
(declare-const b Int) ; 语法糖写法，声明一个常量

与编程语言中函数不同的是，z3中的函数可以视为一个未解释的公式，不会在运行时抛出异常，也不会出现没有返回值的情况。专业术语将其称之为一阶逻辑或者谓词演算——百度百科。一阶逻辑中的“函数”是“未定义”的，意思就是不存在一种类似于四则运算一般固定的解释模式(model)。只要任何符合约束条件的model，都可以作为一种解释，而check-set就是用来求解的。

很抽象，可以看下面例子大概理解下。

用z3证明 f(f(x)) = x, f(x)=y, x!=y约束的存在性（给出一种可能性解释），并且还定义了一个抽象的类型（sort在z3中表示类型，使用declare-sort定义类型）：

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)

需要特别注意下z3函数的使用方式与编程语言不同：编程语言通过(x1,x2,x3)方式传参，而z3将函数视为一个运算符号通过类似三地址码的方式传参 —— 函数符号 x1 x2 x3

输出：

sat
(model
  ;; universe for A:
  ;;   A!val!0 A!val!1
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!0 () A)
  (declare-fun A!val!1 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!0) (= x A!val!1)))
  ;; -----------
  (define-fun x () A
    A!val!0)
  (define-fun y () A
    A!val!1)
  (define-fun f ((x!0 A)) A
    (ite (= x!0 A!val!1) A!val!0
      A!val!1))
)

生成的模型为A引入了抽象值。

算数运算

基本运算

z3内置了对于整数和实数等数学类型的支持，而且貌似最新版已经合并了原先的插件——z3str，可以进行字符串处理，关于这部分文档似乎没有详细说明...

declare-const可以用于声明整数和实数常量

如：

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)

声明完常量后，就可以在后续的式子中使用这些变量，式子中可以包含常用的数学运算符如:
+ - x div/mod/ram。

check-sat & get-model

check-sat是高频使用的命令，用于对表达式求解，基本上就是为每个常数分配一个数字。如果存在一种解使得所有式子为真，那么结果就为sat，并且称这个解释为一个model，使用get-model可以查看；如果不存在解释，则结果为unsat，也无法获取可行的model。
例子：

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun c () Int
    0)
  (define-fun b () Int
    0)
  (define-fun e () Real
    0.0)
  (define-fun d () Real
    0.0)
  (define-fun a () Int
    10)
)

类型转换

在z3中Int类型和Real类型不会自动互相转换，但是借助函数to-Real（参数为一个整数）可以将整数化为实数。
例子：

(assert (> e (+ (to_real (+ a b)) 2.0)))
(assert (= d (+ (to_real c) 0.5)))

非线性运算特性

当式子中有类似(* t s)的实数运算时称为非线性式，这种式子求解极其困难，导致z3在求解非线性问题的时候不一定总能确定是否有解。当无法确定是否可以求解时使用check-sat会返回unknow；当然，部分特殊的非线性式依然可以确定可满足性。
例子：

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 does not always find solutions to non-linear problems")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)

(reset)
(echo "When presented only non-linear constraints over reals, Z3 uses a specialized complete solver")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun a () Int
    (- 3))
)
Z3 does not always find solutions to non-linear problems
unknown
yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...
unsat
When presented only non-linear constraints over reals, Z3 uses a specialized complete solver
sat
(model
  (define-fun b () Real
    (/ 1.0 8.0))
  (define-fun c () Real
    (/ 1535.0 64.0))
)

除法运算

z3支持除法、求模和求余运算，这些运算在底层都会被映射成乘法。

注意在实数除法的时候用符号/，因为实数没有求模和取余。

例子：

(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(declare-const r5 Int)
(declare-const r6 Int)
(assert (= a 10))
(assert (= r1 (div a 4))) ; integer division
(assert (= r2 (mod a 4))) ; mod
(assert (= r3 (rem a 4))) ; remainder
(assert (= r4 (div a (- 4)))) ; integer division
(assert (= r5 (mod a (- 4)))) ; mod
(assert (= r6 (rem a (- 4)))) ; remainder
(declare-const b Real)
(declare-const c Real)
(assert (>= b (/ c 3.0)))
(assert (>= c 20.0))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun c () Real
    20.0)
  (define-fun b () Real
    (/ 20.0 3.0))
  (define-fun r6 () Int
    (- 2))
  (define-fun r5 () Int
    2)
  (define-fun r4 () Int
    (- 2))
  (define-fun r3 () Int
    2)
  (define-fun r2 () Int
    2)
  (define-fun r1 () Int
    2)
  (define-fun a () Int
    10)
)

z3有一个很有意思的地方，就是不会发生除0错误，因为除0操作是未定义的，在求解的时候可以被定义为一个函数。
例如：

(declare-const a Real)
; The following formula is satisfiable since division by zero is not specified.
(assert (= (/ a 0.0) 10.0)) 
(check-sat)
(get-model)

; Although division by zero is not specified, division is still a function.
; So, (/ a 0.0) cannot evaluated to 10.0 and 2.0.
(assert (= (/ a 0.0) 2.0)) 
(check-sat)

输出：

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    10.0)
)
unsat

如果对上述行为不满意还可以使用ite语句自定义除法规则：

; defining my own division operator where x/0.0 == 0.0 for every x.
(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))
(declare-const a Real)
(declare-const b Real)
(assert (>= (mydiv a b) 1.0))
(assert (= b 0.0))
(check-sat)

关于ite语句：
其实就是if-then-else语句，其结构为(if 条件 真返回值 假返回值)
此处判断被除数是否为0来返回不同结果

位向量

暂略，用到的不多

数组

常用数组操作

• 数组定义：(declare-const a1 (Array Int Int))
  
  

  这是使用了语法糖的定义方式，原生定义方式如下：

  (define-fun a1 () (Array Int Int) [val])
  例如：

  (define-fun a2 () (Array Int Int)
  ((as const (Array Int Int)) 0))
  

• 取出值：(select a i)
  
  

  a-数组；i-下标；返回：a数组下标对应值

• 存入值：(store a i v)
  
  

  a-数组；i-下标；v-新值；返回：数组本身

例子：

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun y () Int
    0)
  (define-fun a1 () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 0 0))
  (define-fun x () Int
    0)
  (define-fun z () Int
    0)
  (define-fun a2 () (Array Int Int)
    ((as const (Array Int Int)) 0))
  (define-fun a3 () (Array Int Int)
    ((as const (Array Int Int)) 0))
)

常数数组

当数组中每个索引都指向同一个值就变成了常数数组。可以使用as const (Array T1 T2)结构构造一个常数数组，该结构会返回指定类型的数组。原文档对这块的介绍不是很详细，我提取了主要的语句结构如下：

(declare-const a (Array Int Int))
(assert (= a ((as const (Array Int Int)) 1)))

第一句声明一个数组，第二句用断言的方式将该数组约束为常数数组。
例子：

(declare-const all1 (Array Int Int))
(declare-const a Int)
(declare-const i Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= a (select all1 i)))
(check-sat)
(get-model)
(assert (not (= a 1)))
(check-sat)

输出：

sat
(model
  (define-fun a () Int
    1)
  (define-fun all1 () (Array Int Int)
    ((as const (Array Int Int)) 1))
  (define-fun i () Int
    0)
)
unsat