如何通过LLVM和Z3实现程序验证器

Question

我需要用LLVM和Z3，实现一个程序验证器原型，例如对于以下程序

int main() {
  int n, k, j;
  n = input();
  assume(n > 0);
  k = input();
  assume(k > n);
  j = 0;
  while (j < n) {
    j++;
    k--;
  }
  assert(k >= 0);
  return 0;
}

其通过llvm生成的ll文件主要内容如下

define dso_local i32 @main() #0 {
entry:
  %call = call i32 (...) @input()
  %cmp = icmp sgt i32 %call, 0
  %conv = zext i1 %cmp to i32
  call void @assume(i32 %conv)
  %call1 = call i32 (...) @input()
  %cmp2 = icmp sgt i32 %call1, %call
  %conv3 = zext i1 %cmp2 to i32
  call void @assume(i32 %conv3)
  br label %while.cond

while.cond:                                       ; preds = %while.body, %entry
  %k.0 = phi i32 [ %call1, %entry ], [ %dec, %while.body ]
  %j.0 = phi i32 [ 0, %entry ], [ %inc, %while.body ]
  %cmp4 = icmp slt i32 %j.0, %call
  br i1 %cmp4, label %while.body, label %while.end

while.body:                                       ; preds = %while.cond
  %inc = add nsw i32 %j.0, 1
  %dec = add nsw i32 %k.0, -1
  br label %while.cond

while.end:                                        ; preds = %while.cond
  %cmp6 = icmp sge i32 %k.0, 0
  br i1 %cmp6, label %if.then, label %if.else

if.then:                                          ; preds = %while.end
  br label %if.end

if.else:                                          ; preds = %while.end
  call void @__assert_fail(i8* getelementptr inbounds ([7 x i8], [7 x i8]* @.str, i64 0, i64 0), i8* getelementptr inbounds ([10 x i8], [10 x i8]* @.str.1, i64 0, i64 0), i32 14, i8* getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #3
  unreachable

if.end:                                           ; preds = %if.then
  ret i32 0
}

我需要通过Z3验证__assert_fail不可达

目前已经有基本框架

using namespace llvm;

using InstMapTy = std::map<Value *, unsigned int>;
using DefMapTy = std::map<Value *, std::set<Value *>>;

class Extractor {
public:
  Extractor() : AllVariableVector(C), Queries(C) {
    Solver = new z3::fixedpoint(C);
    Params = new z3::params(C);
    Params->set("engine", "spacer");
    Solver->set(*Params);
  }

  ~Extractor() {
    delete Solver;
    delete Params;
  }

  z3::fixedpoint *getSolver() { return Solver; }
  z3::context &getContext() { return C; }
  z3::func_decl_vector &getQueries() { return Queries; }

  void initialize(Function &F);
  void extractConstraints(Instruction *I, z3::expr_vector &Assertions);
  void extractConstraints(BasicBlock *BB);
  void addQuery(z3::func_decl &Q) { Queries.push_back(Q); }
  z3::expr_vector transition(BasicBlock *BB, BasicBlock *Succ);

private:
  z3::context C;
  z3::fixedpoint *Solver;
  z3::params *Params;
  z3::check_result Result;
  z3::func_decl_vector Queries;
  std::map<BasicBlock *, std::set<Value *>> FreeVariables;
  std::map<BasicBlock *, z3::func_decl> BBRelations;
  std::map<BasicBlock *, z3::expr_vector> FreeVariableVector;
  z3::expr_vector AllVariableVector;
};

在对直接跳转分支进行处理时

if (BranchInst *BI = dyn_cast<BranchInst>(&BB->back())) {
  if (BI->isUnconditional()) {
    BasicBlock *Succ = BI->getSuccessor(0);
    z3::func_decl &SuccRel = BBRelations.at(Succ);
    z3::expr_vector Propagation = transition(BB, Succ);
    z3::expr SuccTuple = SuccRel(Propagation);

    z3::expr R0
             = z3::forall(allVariableVector, z3::implies(BBTuple && And, SuccTuple));
    
    Solver->add_rule(R0, C.str_symbol(“”));
  }
}

目前问题在于，我不知道 z3::func_decl &SuccRel、 transition(BB, Succ)的作用是什么，z3::forall(allVariableVector, z3::implies(BBTuple && And, SuccTuple))不知道怎么写，不知道BBTuple和SuccTuple的内容。请结合代码示例给我几个z3::forall(allVariableVector, z3::implies(BBTuple && And, SuccTuple))的具体内容，同时对SuccRel、transition做出一定的解释

Answer 1

z3::func_decl代表一个关系函数,SuccRel就是后继基本块的关系函数，BBTuple和SuccTuple分别代表当前基本块和后继基本块的表达式,内容可以是基本块中的变量等
参考 http://rightingcode.org/tutorials/popl20/index.html