[z3env] add ReadCallExp relation

prosyslab · Jun 20, 2024 · 3c190d0 · 3c190d0
1 parent 30be1a6
commit 3c190d0
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 3 deletions.
diff --git a/src/chc.ml b/src/chc.ml
@@ -520,6 +520,7 @@ let from_node_to_ast ?(leaf = empty) terms = function
       if (not (mem l1 leaf)) && mem l1 terms then (true, add l2 terms)
       else (false, terms)
   | FuncApply ("CallExp", [ e; _; arg_list ])
+  | FuncApply ("ReadCallExp", [ e; _; arg_list ])
   | FuncApply ("LibCallExp", [ e; _; arg_list ]) ->
       if (not (mem e leaf)) && mem e terms then (true, add arg_list terms)
       else (false, terms)
@@ -568,6 +569,7 @@ let is_child var = function
   | FuncApply ("UnOpExp", hd :: _)
   | FuncApply ("LvalExp", hd :: _)
   | FuncApply ("CallExp", hd :: _)
+  | FuncApply ("ReadCallExp", hd :: _)
   | FuncApply ("LibCallExp", hd :: _)
   | FuncApply ("AllocExp", hd :: _)
   | FuncApply ("SAllocExp", hd :: _) ->
@@ -652,6 +654,7 @@ let from_ast_to_node terms = function
   | FuncApply ("Field", [ l1; l2 ]) ->
       if mem l2 terms then (true, add l1 terms) else (false, terms)
   | FuncApply ("CallExp", [ e; _; arg_list ])
+  | FuncApply ("ReadCallExp", [ e; _; arg_list ])
   | FuncApply ("LibCallExp", [ e; _; arg_list ]) ->
       if mem arg_list terms then (true, add e terms) else (false, terms)
   | FuncApply ("AllocExp", [ e; size_e ]) ->
@@ -701,7 +704,8 @@ let filter_by_node =
       if List.length sort_id = 2 then
         match name with
         | "Exp" | "CallExp" | "LibCallExp" | "SallocExp" | "AllocExp"
-        | "ArgList" | "Lval" | "Loc" | "Val" | "Pos" | "AstNode" ->
+        | "ReadCallExp" | "ArgList" | "Lval" | "Loc" | "Val" | "Pos" | "AstNode"
+          ->
             false
         | _ -> true
       else false)

diff --git a/src/dug.ml b/src/dug.ml
@@ -131,8 +131,9 @@ let mapping_func_lvmap lval_map v lvs g =
     let orig_lvmap = Hashtbl.find g.lvmap_per_func func_name in
     LvalMap.union
       (fun _ a_sym b_sym ->
-        if String.equal a_sym b_sym |> not then
+        if String.equal a_sym b_sym |> not then (
           L.warn "There are two symbols of same lv in one func";
+          L.warn "a_sym: %s, b_sym: %s" a_sym b_sym);
         Some a_sym)
       orig_lvmap lvm
     |> Hashtbl.replace g.lvmap_per_func func_name

diff --git a/src/parser.ml b/src/parser.ml
@@ -85,6 +85,7 @@ let file2func = function
   | "BinOpExp.facts" -> "BinOpExp"
   | "UnOpExp.facts" -> "UnOpExp"
   | "CallExp.facts" -> "CallExp"
+  | "ReadCallExp.facts" -> "ReadCallExp"
   | "CFPath.facts" -> "CFPath"
   | "DetailedDUEdge.facts" -> "DetailedDUEdge"
   | "DUEdge.facts" -> "DUEdge"
@@ -106,6 +107,7 @@ let file2func = function
 type facts4sparrow = {
   set_facts : Chc.elt list list;
   callexp_facts : Chc.elt list list;
+  readcall_facts : Chc.elt list list;
   libcall_facts : Chc.elt list list;
   args_facts : Chc.elt list list;
   alloc_exp_facts : Chc.elt list list;

diff --git a/src/z3env.ml b/src/z3env.ml
@@ -40,6 +40,7 @@ type t = {
   addrof : Z3.FuncDecl.func_decl;
   call : Z3.FuncDecl.func_decl;
   libcall : Z3.FuncDecl.func_decl;
+  readcall : Z3.FuncDecl.func_decl;
   arg : Z3.FuncDecl.func_decl;
   constexp : Z3.FuncDecl.func_decl;
   ret : Z3.FuncDecl.func_decl;
@@ -106,6 +107,7 @@ let reg_rel_to_solver env solver =
   Z3.Fixedpoint.register_relation solver env.addrof;
   Z3.Fixedpoint.register_relation solver env.call;
   Z3.Fixedpoint.register_relation solver env.libcall;
+  Z3.Fixedpoint.register_relation solver env.readcall;
   Z3.Fixedpoint.register_relation solver env.arg;
   Z3.Fixedpoint.register_relation solver env.constexp;
   Z3.Fixedpoint.register_relation solver env.ret;
@@ -141,6 +143,7 @@ let fact_files =
     "DUEdge.facts";
     "DUPath.facts";
     "LibCallExp.facts";
+    "ReadCallExp.facts";
     "LvalExp.facts";
     "Index.facts";
     "Mem.facts";
@@ -236,6 +239,10 @@ let mk_env sort_size =
     Z3.FuncDecl.mk_func_decl_s z3ctx "LibCallExp" [ expr; expr; arg_list ]
       boolean_sort
   in
+  let readcall =
+    Z3.FuncDecl.mk_func_decl_s z3ctx "ReadCallExp" [ expr; expr; arg_list ]
+      boolean_sort
+  in
   let arg =
     Z3.FuncDecl.mk_func_decl_s z3ctx "Arg"
       [ arg_list; int_sort; expr ]
@@ -351,6 +358,7 @@ let mk_env sort_size =
     addrof;
     call;
     libcall;
+    readcall;
     arg;
     constexp;
     ret;

diff --git a/src/z3utils.ml b/src/z3utils.ml
@@ -21,6 +21,7 @@ let match_func z3env f =
   | "AddrOf" -> z3env.addrof
   | "CallExp" -> z3env.call
   | "LibCallExp" -> z3env.libcall
+  | "ReadCallExp" -> z3env.readcall
   | "Arg" -> z3env.arg
   | "ConstExp" -> z3env.constexp
   | "Return" -> z3env.ret
@@ -130,7 +131,9 @@ let match_sort z3env s =
     else z3env.bv_sort
   else
     match name with
-    | "Exp" | "CallExp" | "LibCallExp" | "SallocExp" | "AllocExp" -> z3env.expr
+    | "Exp" | "CallExp" | "LibCallExp" | "SallocExp" | "AllocExp"
+    | "ReadCallExp" ->
+        z3env.expr
     | "ArgList" -> z3env.arg_list
     | "Lval" -> z3env.lval
     | "Loc" -> z3env.loc