diff --git a/lib/analysis/ide_live.ml b/lib/analysis/ide_live.ml index 565c69d3..2241f522 100644 --- a/lib/analysis/ide_live.ml +++ b/lib/analysis/ide_live.ml @@ -330,11 +330,11 @@ proc @fun2(f:bv64, global_in:bv64) -> (out2:bv64) { } {| @fun2 (L,L->IdEdge), (L,f->ConstEdge true), (L,f_2->ConstEdge true), (L,f_1->ConstEdge true), (out2,global_in->IdEdge), (out2,out2->IdEdge), (out2,global_1->IdEdge), (out2,g_2->IdEdge), (out2,g_1->IdEdge), (out2,f_3->IdEdge), (out2,g_3->IdEdge) - global_in, f, out2, global_1, f_2, g_2, f_1, g_1, f_3, g_3 + f, global_in, out2, global_1, f_2, g_2, f_1, g_1, f_3, g_3 @main (L,L->IdEdge), (L,b->ConstEdge true), (L,global_in->ConstEdge true), (L,y->ConstEdge true), (L,global_1->ConstEdge true), (L,a->ConstEdge true), (L,x->ConstEdge true), (L,b_1->ConstEdge true), (L,x_1->ConstEdge true), (L,y_1->ConstEdge true) b, global_in, y, global_1, a, x, b_1, x_1, y_1 @fun1 - (L,L->IdEdge), (L,d->ConstEdge true), (out,global_in->IdEdge), (out,c->IdEdge), (out,out->IdEdge), (out,global_1->IdEdge), (out,e->IdEdge) - global_in, c, d, out, global_1, e + (L,L->IdEdge), (L,d->ConstEdge true), (out,c->IdEdge), (out,global_in->IdEdge), (out,out->IdEdge), (out,global_1->IdEdge), (out,e->IdEdge) + c, d, global_in, out, global_1, e |}] diff --git a/lib/analysis/linear_const.ml b/lib/analysis/linear_const.ml index df9c26ef..7ca22f40 100644 --- a/lib/analysis/linear_const.ml +++ b/lib/analysis/linear_const.ml @@ -106,7 +106,8 @@ module LF = struct Linear (a, b) | _ -> Join (a, b, c) - (* Should make join edges with top become TopEdges (and probably similar for effectively id Linear and Join edges...) *) + (** Should make join edges with top become TopEdges (and probably similar for + effectively id Linear and Join edges...) *) let join a b = assert (canonical a && canonical b); match (a, b) with @@ -348,42 +349,39 @@ module LinearIDE = struct end module LinearConstAnalysis = IDESSI (LinearIDE) - -(* For each linear assign and phi node, we create edges from the lhs to all - copied-from variables. For assignments we associate a function encoding the - linear expression. The function should be thought of pointing opposite to - the direction of the edge, so we compose functions backwards (opposite - category). We perform path compression (with composition) on linear paths of - this graph to get a partial intraprocedural copy propagation analysis! - However with just this, we miss out on propagation through phi nodes, where - every variable in a phi is a function, and the same function, from the same - source. To fix this, we recursively check whether the copied-from (parent) - variables and functions for all successor vertices are all equal, and if so - we create a path from the parent of these successors. (This is probably hard - to follow with words, so here is an example: - ``` - if ( * ) { x1 = a + 1 } else { x2 = a + 1 } x3 = phi(x1, x2) - ``` - in this hypothetical program, x3 points to x1 and x2, which both point to a - with (+1), so we can update x3 to point to a with (+1). This gives an - analysis that works through phi nodes! - - To make it interprocedural, we perform a some small iteration steps. For - each output variable of each procedure, we see whether it is a function of - only input variables, by doing an all-path-tracking dfs on the path - compressed graph. If this is the case, we go to every caller of this - procedure, and see whether all input variables that map into the output - variable are linear expressions such that their composite functions are all - equal. (Example: - ``` - proc f(x) = { return g(x + 1, x) } - proc g(x, y) = { if ( * ) { z1 = x - 1 } else { z2 = y } return phi(z1, x2) } - ``` - here the return value of g is the same from the call of f! Hence f's output - is a function of x. In this case, we can create an edge from the output - variable in the caller graph to the input variable that copies into it. If - this ever actually happens, we'll want to re-iterate on this procedure as we - may have new edges to propagate to other procedures. *) +(** For each linear assign and phi node, we create edges from the lhs to all + copied-from variables. For assignments we associate a function encoding the + linear expression. The function should be thought of pointing opposite to + the direction of the edge, so we compose functions backwards (opposite + category). We perform path compression (with composition) on linear paths of + this graph to get a partial intraprocedural copy propagation analysis! + However with just this, we miss out on propagation through phi nodes, where + every variable in a phi is a function, and the same function, from the same + source. To fix this, we recursively check whether the copied-from (parent) + variables and functions for all successor vertices are all equal, and if so + we create a path from the parent of these successors. (This is probably hard + to follow with words, so here is an example: + {v if ( * ) { x1 = a + 1 } else { x2 = a + 1 } x3 = phi(x1, x2) v} + in this hypothetical program, x3 points to x1 and x2, which both point to a + with (+1), so we can update x3 to point to a with (+1). This gives an + analysis that works through phi nodes! + + To make it interprocedural, we perform a some small iteration steps. For + each output variable of each procedure, we see whether it is a function of + only input variables, by doing an all-path-tracking dfs on the path + compressed graph. If this is the case, we go to every caller of this + procedure, and see whether all input variables that map into the output + variable are linear expressions such that their composite functions are all + equal. (Example: + {v + proc f(x) = { return g(x + 1, x) } + proc g(x, y) = { if ( * ) { z1 = x - 1 } else { z2 = y } return phi(z1, x2) } + v} + here the return value of g is the same from the call of f! Hence f's output + is a function of x. In this case, we can create an edge from the output + variable in the caller graph to the input variable that copies into it. If + this ever actually happens, we'll want to re-iterate on this procedure as we + may have new edges to propagate to other procedures. *) module CopyNode = struct type content = { @@ -549,7 +547,7 @@ module CopyGraph = struct let default_vertex_attributes _ = [] let graph_attributes _ = [] let default_edge_attributes _ = [] - let get_subgraph _ = None + let get_subgraph _ = Option.None let edge_attributes (_, f, _) = match f with diff --git a/lib/analysis/wp_dual.ml b/lib/analysis/wp_dual.ml index 8f0e094c..8954b98d 100644 --- a/lib/analysis/wp_dual.ml +++ b/lib/analysis/wp_dual.ml @@ -178,6 +178,8 @@ let%expect_test "wp_dual" = let prog = (Loader.Loadir.ast_of_string {| +var $x:bv64; + prog entry @main; proc @main () -> () [ @@ -211,10 +213,4 @@ proc @main () -> () in IntraAnalysis.A.M.find Procedure.Vert.Entry res |> IntraDomain.to_pred |> BasilExpr.to_string |> print_endline; - [%expect - {| - Warn: global undeclared $x assuming mutable unshared - Warn: global undeclared $x assuming mutable unshared - Warn: global undeclared $x assuming mutable unshared - true - |}] + [%expect {| true |}] diff --git a/lib/backends/boogie.ml b/lib/backends/boogie.ml index 509e825c..1c4bd361 100644 --- a/lib/backends/boogie.ml +++ b/lib/backends/boogie.ml @@ -176,7 +176,8 @@ let pretty_apply_intrinsic (op : Ops.AllOps.intrin) match args with | [ (ty1, arg1); (ty2, arg2) ] -> ( match Transforms.Boogie_prepass.Builtins.name op [ ty1; ty2; t ] with - | Function name -> text name ^ pretty_call_args [ arg1; arg2 ] + | Function name -> + text "$" ^ text name ^ pretty_call_args [ arg1; arg2 ] | Infix name -> bracket "(" (arg1 ^+ text name ^+ arg2) ")" | _ -> failwith "Unsupported binary-reduced intrinsic expr ") | _ -> @@ -509,7 +510,8 @@ let pretty_declaration (d : Program.declaration) = ")" ^ bracket " returns (" (text (type_to_string rt)) ")" ^ text ";" - | Program.Type { binding; typ } -> pretty_type_declaration binding typ + | Program.Type { binding; typ } -> + pretty_type_declaration (ID.name binding) typ | Procedure { definition } -> pretty_procedure definition let pretty_program (p : Program.t) = diff --git a/lib/gtirb/conf.ml b/lib/gtirb/conf.ml index 9bf98f5f..d2dc3e3e 100644 --- a/lib/gtirb/conf.ml +++ b/lib/gtirb/conf.ml @@ -2,12 +2,12 @@ open Lang.Common type config = { opcode_length : int; (** arm64 opcode size constant *) - pc_var : Var.t; (* variable to use as PC*) + pc_var : string * Types.t; (* variable to use as PC*) disas : bool; (** include disassembly of opcodes if llvm-mc is available *) direct : bool; (** when true, don't attempt to perform any cleanup of gtirb's cfg *) } let conf = - let pc_var = Var.create "$PC" ~scope:Var.GlobalVar (Bitvector 64) in + let pc_var = ("$PC", Types.(Bitvector 64)) in { opcode_length = 4; pc_var; disas = true; direct = false } diff --git a/lib/gtirb/gfir_to_bincaml.ml b/lib/gtirb/gfir_to_bincaml.ml index e08a1b56..968aefc2 100644 --- a/lib/gtirb/gfir_to_bincaml.ml +++ b/lib/gtirb/gfir_to_bincaml.ml @@ -15,21 +15,23 @@ open Conf module Result = OResult open struct - let addr_equal_expr addr = + let addr_equal_expr pc_var addr = Lang.Expr.BasilExpr.( - binexp ~op:`EQ (bvconst (Bitvec.of_int ~size:64 addr)) (rvar conf.pc_var)) + binexp ~op:`EQ + (bvconst (Bitvec.of_int ~size:64 addr)) + (Lang.Expr.BasilExpr.rvar pc_var)) let sanitize_proc_name p = List.fold_left (fun a sub -> String.replace ~sub ~by:"" a) p [ "@"; "." ] end -let add_proxy_block ?(attrib = StringMap.empty) succ_addr (proc, blockmap) uuid - = +let add_proxy_block pc_var ?(attrib = StringMap.empty) succ_addr + (proc, blockmap) uuid = let open Lang in let open Option in let ensure = succ_addr uuid - |> Iter.map (fun addr -> addr_equal_expr addr) + |> Iter.map (fun addr -> addr_equal_expr pc_var addr) |> Iter.to_list |> Expr.BasilExpr.applyintrin ~op:`OR in @@ -44,13 +46,13 @@ let add_proxy_block ?(attrib = StringMap.empty) succ_addr (proc, blockmap) uuid (* Update (procedure, uuidmap) with a newly created IR block containing stmts and PC address contract*) -let add_new_simple_block ?(name_suffix = "") ?(attrib = StringMap.empty) +let add_new_simple_block pc_var ?(name_suffix = "") ?(attrib = StringMap.empty) succ_addr (proc, blockmap) (uuid, addr, stmts) = let open Lang in let open Option in let guard = let* addr = addr in - let guard = addr_equal_expr addr in + let guard = addr_equal_expr pc_var addr in let guard = Stmt.Instr_Assume { body = guard; branch = false; attrib = Attrib.empty } in @@ -58,7 +60,7 @@ let add_new_simple_block ?(name_suffix = "") ?(attrib = StringMap.empty) in let ensure = succ_addr uuid - |> Iter.map (fun addr -> addr_equal_expr addr) + |> Iter.map (fun addr -> addr_equal_expr pc_var addr) |> Iter.to_list |> Expr.BasilExpr.applyintrin ~op:`OR in @@ -80,8 +82,8 @@ let address_of_uuid all_blocks uuid = (* Update (procedure, uuidmap) with a newly created IR block with opcodes and PC address contract *) -let add_new_code_block (all_blocks : block UUIDMap.t) temp_proc succ_addr - (proc, blockmap) (b : Gtirb.block) = +let add_new_code_block (pc_var : Var.t) (all_blocks : block UUIDMap.t) temp_proc + succ_addr (proc, blockmap) (b : Gtirb.block) = let open Lang in let open Option in match b with @@ -137,10 +139,11 @@ let add_new_code_block (all_blocks : block UUIDMap.t) temp_proc succ_addr in match b with | Code { address } | Data { address } -> - add_new_simple_block ~name_suffix:"_code" ~attrib succ_addr + add_new_simple_block pc_var ~name_suffix:"_code" ~attrib succ_addr (proc, blockmap) (Gtirb.uuid b, Some address, instrs) - | Proxy uuid -> add_proxy_block ~attrib succ_addr (proc, blockmap) uuid) + | Proxy uuid -> + add_proxy_block pc_var ~attrib succ_addr (proc, blockmap) uuid) | Data _ | Proxy _ -> (proc, blockmap) (** For each successor set containing a fallthrough edge, remove fallthrough @@ -256,7 +259,7 @@ let transform_cfg_calls procs = { p with cfg }) procs -let temp_proc_to_ir_proc all_blocks m (p : temp_proc) = +let temp_proc_to_ir_proc pc_var all_blocks m (p : temp_proc) = let entry_addrs = UUIDSet.to_iter p.entries |> Iter.filter_map (fun x -> UUIDMap.find x p.code_blocks |> Gtirb.address) @@ -266,7 +269,9 @@ let temp_proc_to_ir_proc all_blocks m (p : temp_proc) = entry_addrs |> Iter.map (fun i -> Lang.Expr.BasilExpr.( - binexp ~op:`EQ (bvconst (Bitvec.of_int ~size:64 i)) (rvar conf.pc_var))) + binexp ~op:`EQ + (bvconst (Bitvec.of_int ~size:64 i)) + (Lang.Expr.BasilExpr.rvar pc_var))) |> Iter.to_list |> fun conj -> Lang.Expr.BasilExpr.applyintrin ~op:`OR conj |> fun pc_init -> [ pc_init ] @@ -292,7 +297,7 @@ let temp_proc_to_ir_proc all_blocks m (p : temp_proc) = let proc, blocks = p.code_blocks |> UUIDMap.to_iter |> Iter.map snd |> Iter.fold - (add_new_code_block all_blocks p succ_addr) + (add_new_code_block pc_var all_blocks p succ_addr) (proc, UUIDMap.empty) in let proc, blocks = @@ -308,7 +313,7 @@ let temp_proc_to_ir_proc all_blocks m (p : temp_proc) = (UUIDMap.find_opt uuid all_blocks) | _ -> None) |> Iter.fold - (add_new_simple_block ~name_suffix:"_ext" succ_addr) + (add_new_simple_block pc_var ~name_suffix:"_ext" succ_addr) (proc, blocks) in @@ -328,7 +333,8 @@ let temp_proc_to_ir_proc all_blocks m (p : temp_proc) = (** Convert Gtirb Protobuf module to a Bincaml IR program*) let module_to_ir_prog ir_cfg (m : Module.t) = let prog = Lang.Program.empty ~name:m.name () in - let prog = Lang.Program.decl_global prog conf.pc_var in + let pc_n, pc_ty = conf.pc_var in + let prog, pc_var = Lang.Program.decl_global_var prog pc_n Var.None pc_ty in (* (1) build Gfir CFG *) let entry_proc, procs = gtirb_to_gfir prog ir_cfg m in (* collect map of all blocks in order to fixup interprocedural control-flow @@ -351,7 +357,7 @@ let module_to_ir_prog ir_cfg (m : Module.t) = *) let prog = UUIDMap.fold - (fun _ proc prog -> temp_proc_to_ir_proc all_blocks prog proc) + (fun _ proc prog -> temp_proc_to_ir_proc pc_var all_blocks prog proc) procs prog in let entry_proc = UUIDMap.find entry_proc procs in diff --git a/lib/lang/algsimp.ml b/lib/lang/algsimp.ml index 1f3af5d7..96115254 100644 --- a/lib/lang/algsimp.ml +++ b/lib/lang/algsimp.ml @@ -331,13 +331,14 @@ let normalise e = BasilExpr.rewrite_typed_two normalise e let%expect_test "normalise" = + let gs = Var.mk_gen () in let e = BasilExpr.boolnot @@ BasilExpr.boolnot @@ BasilExpr.boolnot @@ BasilExpr.applyintrin ~op:`AND [ BasilExpr.boolnot - (BasilExpr.boolnot (BasilExpr.rvar (Var.create "b" Boolean))); - BasilExpr.rvar (Var.create "a" Boolean); + (BasilExpr.boolnot (BasilExpr.rvar (gs.fresh Boolean))); + BasilExpr.rvar (gs.fresh Boolean); ] in print_endline (BasilExpr.to_string e); @@ -345,6 +346,6 @@ let%expect_test "normalise" = print_endline (BasilExpr.to_string e); [%expect {| - boolnot(boolnot(boolnot(booland(boolnot(boolnot(b:bool)), a:bool)))) - boolor(boolnot(b:bool), boolnot(a:bool)) + boolnot(boolnot(boolnot(booland(boolnot(boolnot(v_1:bool)), v:bool)))) + boolor(boolnot(v_1:bool), boolnot(v:bool)) |}] diff --git a/lib/lang/check.ml b/lib/lang/check.ml index d26f8130..f0847da0 100644 --- a/lib/lang/check.ml +++ b/lib/lang/check.ml @@ -20,18 +20,14 @@ let formal_params p = let sigil_ok v = let s = Var.name v |> String.take 1 in - let sgl = Var.scope v in - match sgl with - | (Var.LocalVar | Var.LocalConst) when String.equal s "$" -> - raise - @@ IRWellformed - ("local " ^ Var.to_string v ^ "should not have global sigil $") - | (Var.GlobalVar | Var.GlobalVarShared | Var.GlobalConst) - when not @@ String.equal s "$" -> - raise - @@ IRWellformed - ("global " ^ Var.to_string v ^ " should have global sigil $") - | _ -> () + if Var.is_local v && String.equal s "$" then + raise + @@ IRWellformed + ("local " ^ Var.to_string v ^ "should not have global sigil $"); + if Var.is_global v && (not @@ String.equal s "$") then + raise + @@ IRWellformed ("global " ^ Var.to_string v ^ " should have global sigil $"); + () let variables_wf p = let ref_vars = ref StringMap.empty in @@ -49,33 +45,32 @@ let variables_wf p = let var_is_ok n = sigil_ok n; ref_var n; - match Var.scope n with - | Var.LocalConst | Var.LocalVar -> ( - try ignore @@ Procedure.lookup_local_decl p (Var.name n) - with Not_found -> - raise - (IRWellformed - ("local " ^ Var.to_string n ^ " is not declared in " - ^ ID.to_string (Procedure.id p)))) - | (Var.GlobalVar | Var.GlobalVarShared) - when not @@ List.exists (fun v -> Var.equal v n) spec.captures_globs -> - raise - (IRWellformed - ("global " ^ Var.to_string n ^ " is not in capture list of " - ^ (Procedure.id p |> ID.to_string))) - | _ -> () + (if Var.is_local n then + try ignore @@ Procedure.lookup_local_decl p (Var.name n) + with Not_found -> + raise + (IRWellformed + ("local " ^ Var.to_string n ^ " is not declared in " + ^ ID.to_string (Procedure.id p)))); + if + Var.is_global n + && (not (Var.is_const n)) + && (not @@ List.exists (fun v -> Var.equal v n) spec.captures_globs) + then + raise + (IRWellformed + ("global " ^ Var.to_string n ^ " is not in capture list of " + ^ (Procedure.id p |> ID.to_string))) in let m = ref VarSet.empty in let write v = - match Var.scope v with - | LocalConst -> - if VarSet.mem v !m then - raise - (IRWellformed - ("constant local written more than once: " ^ Var.to_string v)) - else m := VarSet.add v !m - | _ -> () + if Var.is_local v && Var.is_const v then + if VarSet.mem v !m then + raise + (IRWellformed + ("constant local written more than once: " ^ Var.to_string v)) + else m := VarSet.add v !m in let check_lvar v = (*sigil_ok v;*) @@ -92,6 +87,18 @@ let variables_wf p = ^ (Procedure.id p |> ID.to_string)))) else () in + begin + let check_modset s vs = + vs |> List.filter Var.is_local |> function + | [] -> () + | ls -> + raise + (IRWellformed + ("local vars in " ^ s ^ " : " ^ List.to_string Var.show ls)) + in + check_modset "modifies" spec.modifies_globs; + check_modset "captures" spec.captures_globs + end; let check e = Expr.BasilExpr.free_vars_iter e |> Iter.iter var_is_ok in List.iter check spec.requires; List.iter check spec.ensures; diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml index 0bfc1223..44562389 100644 --- a/lib/lang/expr.ml +++ b/lib/lang/expr.ml @@ -469,6 +469,18 @@ module BasilExpr = struct (** substitute subexpression sbased on parameter *) let rewrite ?visit ~(rw_fun : t abstract_expr -> rewrite) (expr : t) = + let rw_alg e = + let orig s = fix s in + match rw_fun e with + | SomeInfo { v; __LINE__; __FILE__ } -> + log_rw visit ~__LINE__ ~__FILE__ (fix e) v + | Keep -> orig e + in + cata rw_alg expr + + (** substitute subexpression sbased on parameter *) + let rewrite_checktype ?visit ~(rw_fun : t abstract_expr -> rewrite) (expr : t) + = let rw_alg e = let orig s = fix s in match rw_fun e with diff --git a/lib/lang/expr_eval.ml b/lib/lang/expr_eval.ml index 37aafe14..b7f976f9 100644 --- a/lib/lang/expr_eval.ml +++ b/lib/lang/expr_eval.ml @@ -118,10 +118,11 @@ let%expect_test _ = let%expect_test _ = let open BasilExpr in let ten = bv_of_int ~size:10 10 in + let vg = Var.mk_gen () in let e = binexp ~op:`BVMUL (applyintrin ~op:`BVADD [ ten; ten ]) - (BasilExpr.rvar (Var.create "beans" Types.(Bitvector 10))) + (BasilExpr.rvar (vg.fresh ~name:"beans" Types.(Bitvector 10))) in print_endline (to_string e); let r = to_string @@ partial_eval_expr e in diff --git a/lib/lang/expr_smt.ml b/lib/lang/expr_smt.ml index e51b0378..d9df7fac 100644 --- a/lib/lang/expr_smt.ml +++ b/lib/lang/expr_smt.ml @@ -17,15 +17,17 @@ module SMTLib2 = struct preamble : CCSexp.t list; commands : CCSexp.t list; var_decls : var_decl VarMap.t; + var_gen : Var.generator; logics : LSet.t; } - let empty = + let empty () = { preamble = []; commands = []; var_decls = VarMap.empty; logics = LSet.empty; + var_gen = Var.mk_gen (); } type 'e t = builder -> 'e * builder @@ -86,7 +88,7 @@ module SMTLib2 = struct let commands = List.rev b.commands |> List.to_iter in preamble <+> decls <+> commands - let run (e : 'e t) = e empty + let run (e : 'e t) = e (empty ()) let extract s = let* b = get s in @@ -202,19 +204,20 @@ module SMTLib2 = struct Some (Types.Map (k, v)) | _ -> None - let expr_of_smt vardefs (e : Sexp.t) = + let expr_of_smt ?(vargen : Var.generator option) vardefs (e : Sexp.t) = let open Option.Infix in let module T = List.Traverse (Option) in (* One generator for the whole decode. Reserve every Basil variable already in scope -- the free vars of the values of [vardefs] -- so the quantifier binders minted below stay disjoint from them. *) - let gen = ID.make_gen () in + let vargen = match vargen with Some v -> v | None -> Var.mk_gen () in StringMap.iter (fun _ e -> - BasilExpr.free_vars_iter e - |> Iter.iter (fun v -> ignore (gen.decl_or_get (Var.name v)))) + BasilExpr.free_vars_iter e (* reserve used names *) + |> Iter.iter (fun v -> + ignore (vargen.with_name (Var.name v) (Var.typ v)))) vardefs; - let fresh_var typ = Var.create (ID.name (gen.fresh ~name:"x" ())) typ in + let fresh_var typ = vargen.fresh ~name:"x" typ in (* Give each binder a fresh variable rather than reusing the name the solver chose. This accounts for names that are not valid identifiers (e.g., include [!]) and names that clash with existing variables. *) @@ -314,6 +317,7 @@ module SMTLib2 = struct go vardefs e let decl_var (v : Var.t) s = + let v = s.var_gen.of_var v in VarMap.find_opt v s.var_decls |> function | Some { decl_cmd; var } -> (var, s) | None -> @@ -450,7 +454,7 @@ module SMTLib2 = struct let e = (BasilExpr.rewrite_typed_two Algsimp.drop_assoc) e in BasilExpr.cata smt_alg e b - let of_bexpr e = fst @@ (bind_of_bexpr e) empty + let of_bexpr e = fst @@ (bind_of_bexpr e) (empty ()) let trans_decl (decl : Program.declaration) = let* x = return () in @@ -522,11 +526,11 @@ module SMTLib2 = struct let* _ = assert_bexpr e in add_command (list [ atom "check-sat" ]) in - let ex = (extract x) empty in + let ex = (extract x) (empty ()) in fst ex let%expect_test _ = - let assert_bexpr e = fst @@ (assert_bexpr e |> extract) empty in + let assert_bexpr e = fst @@ (assert_bexpr e |> extract) (empty ()) in let open BasilExpr in let e = binexp ~op:`EQ @@ -544,13 +548,14 @@ module SMTLib2 = struct end let%expect_test "datatypes" = + let g = ID.make_gen () in let x : Program.declaration = - Type { binding = "test"; typ = Types.mk_sort "Opaque" } + Type { binding = g.decl_or_get "test"; typ = Types.mk_sort "Opaque" } in let y : Program.declaration = Type { - binding = "list"; + binding = g.decl_or_get "list"; typ = Types.mk_adt "list" [ @@ -564,8 +569,10 @@ let%expect_test "datatypes" = } in - fst @@ SMTLib2.trans_decl x SMTLib2.empty |> Sexp.to_string |> print_endline; - fst @@ SMTLib2.trans_decl y SMTLib2.empty |> Sexp.to_string |> print_endline; + fst @@ SMTLib2.trans_decl x (SMTLib2.empty ()) + |> Sexp.to_string |> print_endline; + fst @@ SMTLib2.trans_decl y (SMTLib2.empty ()) + |> Sexp.to_string |> print_endline; [%expect {| (declare-datatype Opaque ()) diff --git a/lib/lang/interp.ml b/lib/lang/interp.ml index 9c7c720c..df133d2c 100644 --- a/lib/lang/interp.ml +++ b/lib/lang/interp.ml @@ -420,6 +420,11 @@ module IState = struct exception InterpreterError of (t * string) + let () = + Printexc.register_printer (function + | InterpreterError (_, msg) -> Some ("InterpreterError: " ^ msg) + | _ -> None) + let tick st = match st.fuel with | None -> st @@ -530,10 +535,9 @@ module IState = struct let stack_top st = List.hd st.stack let lookup_var v st = - (match Var.scope v with - | LocalVar | LocalConst -> VarMap.find_opt v (stack_top st).locals - | GlobalVar | GlobalVarShared | GlobalConst -> - VarMap.find_opt v st.globals) + (match Var.is_local v with + | true -> VarMap.find_opt v (stack_top st).locals + | false -> VarMap.find_opt v st.globals) |> function | Some v -> v | None -> raise (ReadUninit v) @@ -546,22 +550,25 @@ module IState = struct | _ -> failwith "unsupported memory type" let lookup_memory v st = - match Var.scope v with - | GlobalVar | GlobalConst | GlobalVarShared -> VarMap.find v st.memories - | _ -> failwith "unsupported" + if Var.is_global v then + VarMap.find_opt v st.memories + |> Option.get_exn_or + ("no memory found : " ^ Var.show v ^ " in " + ^ Iter.to_string Var.show (VarMap.keys st.memories)) + else failwith "unsupported" let write_var var value st = let value = IValue.of_constant value in - match Var.scope var with - | LocalVar | LocalConst -> - let stack = - match st.stack with - | h :: tl -> { h with locals = VarMap.add var value h.locals } :: tl - | _ -> failwith "no stack" - in - { st with stack } - | GlobalVar | GlobalVarShared | GlobalConst -> - { st with globals = VarMap.add var value st.globals } + if Var.is_local var then + let stack = + match st.stack with + | h :: tl -> { h with locals = VarMap.add var value h.locals } :: tl + | _ -> failwith "no stack" + in + { st with stack } + else if Var.is_global var then + { st with globals = VarMap.add var value st.globals } + else failwith "local and global mutually exclusive" let map f v = (fst v, f (snd v)) @@ -656,9 +663,7 @@ module IState = struct | Stmt.Instr_IndirectCall _ -> failwith "unsupported" and eval_stmt (stmt : Program.stmt) (st : t) = - try eval_stmt_unsafe stmt st with - | AssumeFail _ as e -> raise e - | e -> raise (InterpreterError (st, Printexc.to_string e)) + try eval_stmt_unsafe stmt st with AssumeFail _ as e -> raise e and exec_edge st e = let b, l, e = e in diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 8b421db7..377987d5 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -113,6 +113,7 @@ module PG : sig val create : ID.t -> + ?local_id_gen:ID.generator -> ?is_stub:bool -> ?formal_in_params:'a StringMap.t -> ?formal_out_params:'a StringMap.t -> @@ -126,6 +127,21 @@ module PG : sig unit -> ('a, 'b) t + val create_p : + IDSet.elt -> + ?is_stub:bool -> + ?formal_in_params:(string * Types.t) list -> + ?formal_out_params:(string * Types.t) list -> + ?captures_globs:(string * Types.t) list -> + ?modifies_globs:(string * Types.t) list -> + ?requires:BasilExpr.t list -> + ?ensures:BasilExpr.t list -> + ?rely:BasilExpr.t list -> + ?guarantee:BasilExpr.t list -> + ?attrib:Attrib.attrib_map -> + unit -> + (Var.t, 'a) t + val attrib : ('a, 'b) t -> Attrib.attrib_map val set_attrib : ('a, 'b) t -> Attrib.t -> string -> ('a, 'b) t val set_attribs : ('a, 'b) t -> Attrib.attrib_map -> ('a, 'b) t @@ -142,7 +158,7 @@ module PG : sig val local_ids : ('a, 'b) t -> ID.generator (** return mutable generator for fresh local variable IDS *) - val local_decls : ('a, 'b) t -> 'a Var.Decls.t + val local_decls : ('a, 'b) t -> (string, 'a) Hashtbl.t (** return mutable declaration map for local var IDS *) val formal_in_params : ('a, 'b) t -> 'a StringMap.t @@ -176,7 +192,7 @@ end = struct formal_in_params : 'v StringMap.t; formal_out_params : 'v StringMap.t; graph : G.t option; - locals : 'v Var.Decls.t; + locals : (string, 'v) Hashtbl.t; topo_fwd : Vert.t Graph.WeakTopological.t lazy_t; topo_rev : Vert.t Graph.WeakTopological.t lazy_t; local_ids : ID.generator; @@ -235,19 +251,96 @@ end = struct let graph = G.add_vertex graph Return in graph - let create id ?(is_stub = false) ?(formal_in_params = StringMap.empty) + (** Create a generic procedure *) + let create id ?local_id_gen ?(is_stub = false) + ?(formal_in_params = StringMap.empty) ?(formal_out_params = StringMap.empty) ?(captures_globs = []) ?(modifies_globs = []) ?(requires = []) ?(ensures = []) ?(rely = []) ?(guarantee = []) ?(attrib = Attrib.empty) () = let specification = { captures_globs; modifies_globs; requires; ensures; rely; guarantee } in - let local_ids = ID.make_gen () in + let local_ids = + match local_id_gen with + | Some g -> g + | None -> + let g = ID.make_gen ~scope_name:(ID.name id) () in + (* Oh no: we could have used a _different_ generator to build the in-params *) + StringMap.iter (fun k v -> ignore @@ g.decl_exn k) formal_in_params; + StringMap.iter (fun k v -> ignore @@ g.decl_exn k) formal_out_params; + g + in + let block_ids = ID.make_gen () in + let locals = + Hashtbl.create + (StringMap.cardinal formal_in_params + + StringMap.cardinal formal_out_params) + in + Hashtbl.add_iter locals + (Iter.append + (StringMap.to_iter formal_in_params) + (StringMap.to_iter formal_out_params)); + + let graph = if is_stub then None else Some empty_graph in + { + id; + attrib; + formal_in_params; + formal_out_params; + graph; + locals; + local_ids; + block_ids; + specification; + topo_fwd = + lazy + (WTO.recursive_scc + (Option.get_exn_or "no graph to iterate" graph) + Entry); + topo_rev = + lazy + (RevWTO.recursive_scc + (Option.get_exn_or "no graph to iterate" graph) + Return); + } + + (** Create a (Var.t, Expr.BasilExpr.t) procedure *) + let create_p id ?(is_stub = false) ?(formal_in_params = []) + ?(formal_out_params = []) ?(captures_globs = []) ?(modifies_globs = []) + ?(requires = []) ?(ensures = []) ?(rely = []) ?(guarantee = []) + ?(attrib = Attrib.empty) () = + let local_ids = ID.make_gen ~scope_name:(ID.name id) () in + let vg = Var.mk_gen ~id_generator:local_ids () in + let vars_of_list = + List.map (fun (name, ty) -> + let v = vg.with_name name ty in + (Var.name v, v)) + in + let formal_in_params = + formal_in_params |> vars_of_list |> StringMap.of_list + in + let specification = + { + captures_globs = + (List.map (uncurry @@ vg.with_name ~access:None)) captures_globs; + modifies_globs = + (List.map (uncurry @@ vg.with_name ~access:None)) modifies_globs; + requires; + ensures; + rely; + guarantee; + } + in + let formal_out_params = + formal_out_params |> vars_of_list |> StringMap.of_list + in let block_ids = ID.make_gen () in - StringMap.iter (fun k v -> ignore @@ local_ids.decl_exn k) formal_in_params; - StringMap.iter (fun k v -> ignore @@ local_ids.decl_exn k) formal_out_params; - let locals = Var.Decls.empty () in - Var.Decls.add_iter locals + let locals = + Hashtbl.create + (StringMap.cardinal formal_in_params + + StringMap.cardinal formal_out_params) + in + Hashtbl.add_iter locals (Iter.append (StringMap.to_iter formal_in_params) (StringMap.to_iter formal_out_params)); @@ -479,23 +572,40 @@ let transplant_incoming_edges p ~from ~to_ : _ t = p |> map_graph (replace_incoming_uses ~from:(Begin from) ~to_:(Begin to_)) let lookup_local_decl p v = - Var.Decls.find_opt (local_decls p) v + Hashtbl.find_opt (local_decls p) v |> Option.or_lazy ~else_:(fun () -> StringMap.find_opt v (formal_out_params p)) |> Option.or_lazy ~else_:(fun () -> StringMap.find_opt v (formal_in_params p)) -let decl_local p v = - let _ = (local_ids p).decl_or_get (Var.name v) in - Var.Decls.replace (local_decls p) (Var.name v) v; +let lookup_local_decl_exn p v = + Hashtbl.find_opt (local_decls p) v + |> Option.or_lazy ~else_:(fun () -> + StringMap.find_opt v (formal_out_params p)) + |> Option.or_lazy ~else_:(fun () -> StringMap.find_opt v (formal_in_params p)) + |> Option.get_exn_or ("no local decl : " ^ v) + +let var_generator p = + let g = Var.mk_gen ~id_generator:(local_ids p) ~scope:`Local () in + g + +let get_local p ?(pure = false) name typ : Var.t = + let access = Var.None in + let v = (var_generator p).with_name name ~access typ in + Hashtbl.replace (local_decls p) (Var.name v) v; + v + +let decl_local p ?(pure = false) name typ : Var.t = + let access = Var.None in + let v = (var_generator p).create_exn name ~access typ in + Hashtbl.replace (local_decls p) (Var.name v) v; v let fresh_var p ?(pure = false) ?name typ : Var.t = let name = Option.map (String.drop_while (Char.equal '$')) name in + let access = Var.None in let name = Option.get_or ~default:"v" name in - let n = ID.name @@ (local_ids p).fresh ~name () in - let scope = if pure then Var.LocalConst else LocalVar in - let v = Var.create n typ ~scope in - Var.Decls.replace (local_decls p) (Var.name v) v; + let v = (var_generator p).fresh ~name typ ~access in + Hashtbl.replace (local_decls p) (Var.name v) v; v let blocks_to_list p = @@ -577,6 +687,16 @@ let fold_blocks_topo_rev_headers let fold_blocks_topo_rev (f : 'a -> ID.t -> Edge.block -> 'a) init p = fold_blocks_topo_rev_headers (fun acc i -> f acc) init p +(** get map for formal params assuming in and out are disjointly named (they + should be) *) +let get_formal_params p = + StringMap.merge_safe + ~f:(fun _ -> function + | `Both _ -> failwith "present in both" + | `Left l -> Some l + | `Right r -> Some r) + (formal_in_params p) (formal_out_params p) + let map_blocks_nondet f p = iter_blocks p |> Iter.fold diff --git a/lib/lang/program.ml b/lib/lang/program.ml index 1ba360b3..ddb53336 100644 --- a/lib/lang/program.ml +++ b/lib/lang/program.ml @@ -30,15 +30,16 @@ type func_type = Axiom of e | Uninterpreted | Function of e type implicit_declaration = | VariantCase of { - variant : string; + variant : ID.t; belongs_to : Types.t; constructor : Var.t; (* function to construct a value of this case *) } type declaration = - | Type of { binding : string; typ : Types.t } + | Type of { binding : ID.t; typ : Types.t } | Function of { binding : Var.t; + var_gen : Common.Var.generator; attrib : Attrib.attrib_map; definition : func_type; } (** pure functions *) @@ -50,10 +51,21 @@ type declaration = | Procedure of { definition : proc } let decl_binding = function - | Type { binding } -> binding + | Type { binding } -> ID.name binding | Variable { binding } -> Var.name binding | Function { binding } -> Var.name binding - | Procedure { definition } -> ID.to_string (Procedure.id definition) + | Procedure { definition } -> ID.name (Procedure.id definition) + +let decl_id = function + | Type { binding } -> binding + | Variable { binding } -> Var.id binding + | Function { binding } -> Var.id binding + | Procedure { definition } -> Procedure.id definition + +let decl_bound_var = function + | Variable { binding } -> Some binding + | Function { binding } -> Some binding + | _ -> None let pretty_proc p = let show_lvar v = Containers_pp.text @@ Var.to_string_il_lvar v in @@ -191,16 +203,13 @@ let declare_name_exn name prog = prog.global_names.decl_exn name let declare_name name prog = prog.global_names.decl_or_get name let get_id_by_name name prog = prog.global_names.get_id name -let add_decl ?(attrib = StringMap.empty) p decl = - let d = p.global_names.decl_or_get (decl_binding decl) in - { p with declarations = IDMap.add d decl p.declarations } - let remove_decl p decl = - let d = p.global_names.decl_or_get (decl_binding decl) in + let d = decl_id decl in { p with declarations = IDMap.remove d p.declarations } -let update_decl ?(attrib = StringMap.empty) prog decl = - add_decl ~attrib prog decl +let update_decl ?(attrib = StringMap.empty) p decl = + let id = decl_id decl in + { p with declarations = IDMap.add id decl p.declarations } let add_proc p prog = let id = Procedure.id p in @@ -247,6 +256,10 @@ let prog_pretty (p : t) = let declarations p = p.declarations |> IDMap.to_iter +let var_generator p = + let g = Var.mk_gen ~id_generator:p.global_names ~scope:`Global () in + g + let filter_decls f p = declarations p |> Iter.fold @@ -274,8 +287,7 @@ let flat_map_decls f p = (fun prog (i, decl) -> let ex = ref false in let update_decl prog decl = - get_decl_by_name_id (decl_binding decl) prog - |> Option.iter (fun (id, _) -> if ID.equal id i then ex := true); + (decl_id decl |> fun id -> if ID.equal id i then ex := true); update_decl prog decl in let next = f i decl in @@ -291,41 +303,60 @@ let pretty_to_chan chan (p : t) = Containers_pp.Pretty.to_format ~width:80 fmt p; Format.flush fmt () -let decl_global ?(attrib = StringMap.empty) ?(classification = None) p v = - let id : ID.t = p.global_names.decl_exn (Var.name v) in - let decl = Variable { binding = v; attrib; classification } in - { p with declarations = IDMap.add id decl p.declarations } +let add_decl p decl = + decl_bound_var decl |> Option.iter (fun v -> assert (Var.is_global v)); + { p with declarations = IDMap.add (decl_id decl) decl p.declarations } + +(** add var decl for with id exising in generator *) +let add_var_decl p ?(attrib = Attrib.empty) ?classification v = + assert (Var.is_global v); + let id = Var.id v in + (try assert (ID.equal id (p.global_names.get_name (ID.index id))) + with Not_found -> failwith "Id not created with programs' generator"); + { + p with + declarations = + IDMap.add id + (Variable { attrib; classification; binding = v }) + p.declarations; + } + +let decl_global_var p ?(attrib = StringMap.empty) ?(classification = None) name + access_tag typ = + let vg = var_generator p in + let v = vg.with_name name ~access:access_tag typ in + let p = add_var_decl p ~attrib ?classification v in + (p, v) + +let global_ids p = p.global_names + +let decl_or_get_var p name scope typ = + let vr = (var_generator p).with_name name ~access:scope typ in + IDMap.find_opt (Var.id vr) p.declarations |> function + | Some (Variable { binding }) -> (p, binding) + | _ -> (add_var_decl p vr, vr) let decl_typ ?(attrib = StringMap.empty) p t = match t with | Sort (type_name, []) as s -> let id : ID.t = p.global_names.decl_exn type_name in - { - p with - declarations = - IDMap.add id (Type { binding = type_name; typ = s }) p.declarations; - } + add_decl p (Type { binding = id; typ = s }) | Sort (name, variants) as s -> let id : ID.t = p.global_names.decl_exn name in - { - p with - declarations = - IDMap.add id (Type { binding = name; typ = s }) p.declarations; - implicit_decls = - IDMap.add_list p.implicit_decls - (variants - |> List.map (function { variant; fields } -> - let variant = p.global_names.decl_exn variant in - let args = List.map (function { field; typ } -> typ) fields in - let ty = Types.curry args s in - let constructor = - Var.create (ID.name variant) ty ~scope:GlobalConst - in - ( variant, - VariantCase - { variant = ID.name variant; belongs_to = s; constructor } - ))); - } + let implicit_decls = + IDMap.add_list p.implicit_decls + (variants + |> List.map (function { variant; fields } -> + let args = List.map (function { field; typ } -> typ) fields in + let ty = Types.curry args s in + let vg = var_generator p in + let constructor = vg.with_name variant ~access:Var.Const ty in + ( Var.id constructor, + VariantCase + { variant = Var.id constructor; belongs_to = s; constructor } + ))) + in + { (add_decl p (Type { binding = id; typ = s })) with implicit_decls } | _ -> failwith "not declarable type" let create_single_proc ?(name = "") () = diff --git a/lib/lang/program.mli b/lib/lang/program.mli index ea49abae..5273806d 100644 --- a/lib/lang/program.mli +++ b/lib/lang/program.mli @@ -30,16 +30,13 @@ type prog_spec = { rely : e list; guarantee : e list } type func_type = Axiom of e | Uninterpreted | Function of e type implicit_declaration = - | VariantCase of { - variant : string; - belongs_to : Types.t; - constructor : Var.t; - } + | VariantCase of { variant : ID.t; belongs_to : Types.t; constructor : Var.t } type declaration = - | Type of { binding : string; typ : Types.t } + | Type of { binding : ID.t; typ : Types.t } | Function of { binding : Var.t; + var_gen : Var.generator; attrib : Attrib.attrib_map; definition : func_type; } @@ -51,6 +48,7 @@ type declaration = | Procedure of { definition : proc } val decl_binding : declaration -> string +val decl_id : declaration -> ID.t val pretty_proc : (Var.t, 'a) Procedure.t -> Containers_pp.t val pretty_declaration : declaration -> Containers_pp.t @@ -79,7 +77,6 @@ val get_proc : ID.t -> t -> proc val get_implicit_decl_by_name : string -> t -> implicit_declaration option val declare_name : string -> t -> ID.t val declare_name_exn : string -> t -> ID.t -val add_decl : ?attrib:'a Types.StringMap.t -> t -> declaration -> t val remove_decl : t -> declaration -> t val update_decl : ?attrib:'a Types.StringMap.t -> t -> declaration -> t val add_proc : (Var.t, Expr.BasilExpr.t) Procedure.t -> t -> t @@ -98,14 +95,24 @@ val map_decls : (ID.t -> declaration -> declaration) -> t -> t val filter_map_decls : (ID.t -> declaration -> declaration option) -> t -> t val flat_map_decls : (ID.t -> declaration -> declaration Iter.t) -> t -> t val pretty_to_chan : out_channel -> t -> unit +val add_decl : t -> declaration -> t +val var_generator : t -> Var.generator + +val add_var_decl : + t -> ?attrib:Attrib.attrib_map -> ?classification:e -> Var.t -> t -val decl_global : +val decl_global_var : + t -> ?attrib:Attrib.t Types.StringMap.t -> ?classification:e option -> - t -> - Var.t -> - t - + string -> + Var.access_tag -> + Types.t -> + t * Var.t + +val decl_bound_var : declaration -> Var.t option +val decl_or_get_var : t -> string -> Var.access_tag -> Types.t -> t * Var.t +val global_ids : t -> ID.generator val decl_typ : ?attrib:'a Types.StringMap.t -> t -> Types.t -> t val create_single_proc : diff --git a/lib/lang/spec_modifies.ml b/lib/lang/spec_modifies.ml index 9b2b324d..94c273bb 100644 --- a/lib/lang/spec_modifies.ml +++ b/lib/lang/spec_modifies.ml @@ -5,6 +5,7 @@ open Common module RWSets = struct type property = VarSet.t * VarSet.t [@@deriving eq, ord] + (** (read, written) *) let bottom = (VarSet.empty, VarSet.empty) let equal = equal_property @@ -26,9 +27,17 @@ end module FixProp = Fix.Fix.ForOrderedType (ID) (RWSets) -let solve (prog : Program.t) = +let solve ?(add_existing = false) (prog : Program.t) = let local_rw (p : ID.t) (valuations : FixProp.valuation) = let p = Program.proc prog p in + let spec_read = + if not add_existing then VarSet.empty + else VarSet.of_list (Procedure.specification p).captures_globs + in + let spec_write = + if not add_existing then VarSet.empty + else VarSet.of_list (Procedure.specification p).modifies_globs + in let read, written = match Procedure.graph p with | Some _ -> @@ -48,8 +57,7 @@ let solve (prog : Program.t) = | _ -> None) in Iter.cons local calls |> Iter.fold RWSets.leq_join a) - (VarSet.empty, VarSet.empty) - p + (spec_read, spec_write) p | None -> let globs = Program.global_vars prog |> VarSet.of_iter in (globs, globs) @@ -59,7 +67,7 @@ let solve (prog : Program.t) = FixProp.lfp local_rw let set_modsets ?(add_only = false) prog = - let rwset = solve prog in + let rwset = solve ~add_existing:false prog in prog |> Program.map_procedures (fun i p -> let read, written = rwset i in @@ -77,7 +85,7 @@ let set_modsets ?(add_only = false) prog = |> Iter.filter Var.is_global |> VarSet.of_iter in let captures_globs = - List.filter (not % Var.is_constant) + List.filter (not % Var.is_const) @@ VarSet.elements @@ VarSet.union vs @@ VarSet.union exist_captures @@ VarSet.union read written @@ -91,4 +99,4 @@ let set_modsets ?(add_only = false) prog = let spec = { spec with captures_globs; modifies_globs } in Procedure.set_specification p spec) -let analyse prog = solve prog +let analyse prog = solve ~add_existing:false prog diff --git a/lib/loadir.ml b/lib/loadir.ml index 2957c3ba..4a36ae7e 100644 --- a/lib/loadir.ml +++ b/lib/loadir.ml @@ -36,15 +36,25 @@ let rec to_attrib k l : Attrib.t option = type load_st = { prog : Program.t; curr_proc : Program.proc option; + local_id_gen : ID.generator option; params_order : (string, (string * Var.t) list * (string * Var.t) list) Hashtbl.t; } +let local_var_gen pst = + let idg = + pst.local_id_gen |> Option.get_exn_or "local id context not defiend" + in + Var.mk_gen ~id_generator:idg ~scope:`Local () + +let global_var_gen pst = pst.prog |> Program.var_generator + let load_st_empty ?(name = "") () = { prog = Program.empty ~name (); params_order = Hashtbl.create 30; curr_proc = None; + local_id_gen = None; } exception @@ -162,9 +172,8 @@ module BasilASTLoader = struct map_prog (fun prog -> Spec_modifies.set_modsets ~add_only:true prog) prog and var_modifiers_shared (m : varModifiers list) = - if not @@ List.exists (function Shared | Observable -> true) m then - Var.GlobalVar - else Var.GlobalVarShared + if List.exists (function Shared | Observable -> true) m then Var.Shared + else Var.None and trans_varspec prog (v : varSpec) = let trans_one v = @@ -207,20 +216,20 @@ module BasilASTLoader = struct let scope = var_modifiers_shared modifiers in map_prog (fun p -> - Program.decl_global p ~classification - (Var.create + fst + @@ Program.decl_global_var p ~classification (unsafe_unsigil (`Global bident)) - ~scope (trans_type type'))) + scope (trans_type type')) prog | Decl_Var (modifiers, bident, type', spec) -> let classification = trans_varspec prog spec in let scope = var_modifiers_shared modifiers in map_prog (fun p -> - Program.decl_global p ~classification - (Var.create + fst + @@ Program.decl_global_var p ~classification (unsafe_unsigil (`Global bident)) - ~scope (trans_type type'))) + scope (trans_type type')) prog | Decl_ProgEmpty (ProcIdent (_, id), attr) -> prog | Decl_ProgWithSpec (ProcIdent (_, id), attr, spec) -> prog @@ -228,37 +237,47 @@ module BasilASTLoader = struct let ftype = trans_type rettype in map_prog (fun p -> - Program.decl_global p - (Var.create + fst + @@ Program.decl_global_var p (unsafe_unsigil (`Global glident)) - ~scope:GlobalConst ftype)) + Const ftype) prog | Decl_FunNoType (glident, _, _) -> prog | Decl_Fun (glident, params, _, typ, _) -> + let local_id_gen = Some (ID.make_gen ()) in + let prog = { prog with local_id_gen } in let bound = unpac_lambdaparen ~bound:StringMap.empty prog params in let arg_types = List.map Var.typ bound in let rtype = Types.curry arg_types (trans_type typ) in - let bvar = - Var.create (unsafe_unsigil (`Global glident)) ~scope:GlobalConst rtype - in + let name = unsafe_unsigil (`Global glident) in let fundef : Program.declaration = Function { attrib = StringMap.empty; - binding = bvar; + var_gen = local_var_gen prog; + binding = + (Program.var_generator prog.prog).with_name name ~access:Const + rtype; definition = Uninterpreted; } in - map_prog (fun prog -> Program.add_decl prog fundef) prog + map_prog + (fun prog -> + let p = Program.add_decl prog fundef in + p) + prog + |> fun p -> { p with local_id_gen = None } | Decl_Axiom (name, _, _) -> - let bvar = - Var.create (unsafe_unsigil (`Global name)) ~scope:GlobalConst Boolean - in - + let name = unsafe_unsigil (`Global name) in + let local_id_gen = Some (ID.make_gen ()) in + let prog = { prog with local_id_gen } in let fundef : Program.declaration = + let vg = Program.var_generator prog.prog in + let bvar = vg.with_name name ~access:Const Boolean in Function { attrib = StringMap.empty; + var_gen = local_var_gen prog; binding = bvar; definition = Uninterpreted; } @@ -276,18 +295,23 @@ module BasilASTLoader = struct spec, definition ) -> let proc_id = Program.declare_name id prog.prog in - let formal_in_params_order = List.map param_to_formal in_params in - let formal_in_params = formal_in_params_order |> StringMap.of_list in - let formal_out_params_order = List.map param_to_formal out_params in - let formal_out_params = StringMap.of_list formal_out_params_order in - let _, attrib = trans_attrib_set prog ~binds:formal_in_params attrib in - Hashtbl.add prog.params_order id - (formal_in_params_order, formal_out_params_order); + let formal_in_params = List.map param_names in_params in + let formal_out_params = List.map param_names out_params in + let _, attrib = trans_attrib_set prog ~binds:StringMap.empty attrib in let is_stub = Stdlib.(definition = ProcDef_Empty) in let p = - Procedure.create proc_id ~attrib ~is_stub ~formal_in_params + Procedure.create_p proc_id ~attrib ~is_stub ~formal_in_params ~formal_out_params () in + let param n = StringMap.find n @@ Procedure.get_formal_params p in + let formal_in_params_order = + formal_in_params |> List.map (fun (n, _) -> (n, param n)) + in + let formal_out_params_order = + formal_out_params |> List.map (fun (n, _) -> (n, param n)) + in + Hashtbl.add prog.params_order id + (formal_in_params_order, formal_out_params_order); let prog = map_prog (Program.add_proc p) prog in prog @@ -307,6 +331,8 @@ module BasilASTLoader = struct (** desugar let definition function *) and create_fun prog glident args attrList typ body = + let v = ID.make_gen () in + let prog = { prog with local_id_gen = Some v } in let bound = unpac_lambdaparen ~bound:StringMap.empty prog args in let definition : Program.func_type = match body with @@ -342,12 +368,10 @@ module BasilASTLoader = struct })) in let _, attrib = trans_attrib_set ~binds:StringMap.empty prog attrList in - let binding = - Var.create (unsafe_unsigil (`Global glident)) ~scope:GlobalConst rtype - in - + let name = unsafe_unsigil (`Global glident) in let fundef : Program.declaration = - Function { attrib; binding; definition } + let binding = (global_var_gen prog).with_name name ~access:Const rtype in + Function { attrib; binding; definition; var_gen = Var.mk_gen () } in map_prog (fun prog -> Program.add_decl prog fundef) prog @@ -362,15 +386,25 @@ module BasilASTLoader = struct create_fun prog glident args attrList (Some typ) (Some body) | Decl_Axiom (name, attr, body) -> let _, attrib = trans_attrib_set ~binds:StringMap.empty prog attr in + let v = ID.make_gen () in + let prog = { prog with local_id_gen = Some v } in let body = trans_expr prog body in - let bvar = - Var.create (unsafe_unsigil (`Global name)) ~scope:GlobalConst Boolean - in + let name = unsafe_unsigil (`Global name) in let fundef : Program.declaration = - Function { attrib; binding = bvar; definition = Axiom body } + let bvar = + (global_var_gen prog).with_name name ~access:Const Boolean + in + Function + { + attrib; + binding = bvar; + definition = Axiom body; + var_gen = Var.mk_gen ~id_generator:v (); + } in - map_prog (fun prog -> Program.add_decl prog fundef) prog + map_prog (fun prog -> Program.add_decl prog fundef) prog |> fun p -> + { p with local_id_gen = None } | Decl_ProgEmpty (ProcIdent (_, id), attr) -> let _, nattrib = trans_attrib_set ~binds:StringMap.empty prog attr in prog @@ -402,7 +436,10 @@ module BasilASTLoader = struct spec_list, proc_def ) -> let p = Program.get_proc_by_name id prog.prog in - let prog = { prog with curr_proc = Some p } in + let id_gen = Procedure.local_ids p in + let prog = + { prog with curr_proc = Some p; local_id_gen = Some id_gen } + in let prog, blocks = match proc_def with | ProcDef_Some (bl, blocks, el) -> sequence_st prog trans_block blocks @@ -412,7 +449,9 @@ module BasilASTLoader = struct if List.is_empty blocks then p else Procedure.add_empty_impl p in let open Procedure.Vert in - let formal_out_params_order = List.map param_to_formal out_params in + let formal_out_params_order = + List.map (param_to_formal (local_var_gen prog)) out_params + in (* add blocks *) let p, blocks_id = List.fold_left @@ -542,10 +581,11 @@ module BasilASTLoader = struct | VarLocalVar (LocalTyped (localVar, ty)) -> ( try lookup_local_decl ~binds localVar p_st with e -> + let name = unsafe_unsigil (`Local localVar) in let v = - Var.create ~scope:LocalVar - (unsafe_unsigil (`Local localVar)) - (trans_type ty) + Procedure.get_local + (p_st.curr_proc |> Option.get_exn_or "no current proc") + name (trans_type ty) in Logs.warn (fun m -> m "global undeclared %s. assuming mutable unshared" @@ Var.name v); @@ -553,12 +593,11 @@ module BasilASTLoader = struct | VarLocalVar (LocalUntyped localVar) -> lookup_local_decl ~binds localVar p_st | VarGlobalVar (GlobalTyped (globalVar, ty)) -> ( - try lookup_global_decl globalVar p_st + let name = unsafe_unsigil (`Global globalVar) in + try lookup_global_decl ~typ:(trans_type ty) globalVar p_st with e -> - let v = - Var.create ~scope:GlobalVar - (unsafe_unsigil (`Global globalVar)) - (trans_type ty) + let p, v = + Program.decl_or_get_var p_st.prog name Var.None (trans_type ty) in Logs.warn (fun m -> m "Warn: global undeclared %s. assuming mutable unshared" @@ -882,11 +921,13 @@ module BasilASTLoader = struct and unpack_local_lvars ?(bound = StringMap.empty) p_st const lvs : Var.t list = - let scope = if const then Var.LocalConst else LocalVar in + (* let scope = if const then Var.Const else Var.None in*) lvs |> List.map (function | LocalTyped (i, t) -> - Var.create ~scope (unsafe_unsigil (`Local i)) (trans_type t) + (local_var_gen p_st).with_name + (unsafe_unsigil (`Local i)) + (trans_type t) | LocalUntyped i -> lookup_local_decl ~binds:bound i p_st) and unpac_lambdaparen ?(bound = StringMap.empty) p_st lvs : Var.t list = @@ -904,13 +945,15 @@ module BasilASTLoader = struct | Jump_ProcReturn -> `ProcReturn and assign_var (prog : load_st) v = - let p = Option.get_exn_or "no active proc" prog.curr_proc in - match Var.scope v with - | Var.LocalVar | Var.LocalConst -> - (prog, Procedure.decl_local p v) (* decl is side-effecting *) - | Var.GlobalVar | Var.GlobalVarShared -> - (map_curr_proc (fun p -> write_global p v) prog, v) - | Var.GlobalConst -> failwith "assignment to global constant" + match Var.is_global v with + | true when Var.is_const v -> failwith "assign to global const" + | true -> (map_curr_proc (fun p -> write_global p v) prog, v) + | false -> + ignore + @@ Option.map + (fun proc -> Procedure.get_local proc (Var.name v) (Var.typ v)) + prog.curr_proc; + (prog, v) and loc_lvar (x : BasilIR.AbsBasilIR.lVar) : Attrib.attrib_map = let l = @@ -927,29 +970,20 @@ module BasilASTLoader = struct and trans_lvar prog (x : BasilIR.AbsBasilIR.lVar) : load_st * Var.t = match x with | LVar_Local (LocalTyped (bident, type')) -> + let proc = prog.curr_proc |> Option.get_exn_or "no current proc" in assign_var prog - (Var.create ~scope:LocalVar + @@ Procedure.get_local proc (unsafe_unsigil (`Local bident)) - (trans_type type')) + ~pure:false (trans_type type') | LVar_LocalConst (LocalTyped (bident, type')) -> + let proc = prog.curr_proc |> Option.get_exn_or "no current proc" in assign_var prog - (Var.create ~scope:LocalConst + @@ Procedure.get_local proc (unsafe_unsigil (`Local bident)) - (trans_type type')) + ~pure:true (trans_type type') | LVar_LocalConst (LocalUntyped _) -> failwith "type annotation needed" | LVar_Global (GlobalTyped (bident, type')) -> - let v = - try lookup_global_decl bident prog - with e -> - let v = - Var.create ~scope:GlobalVar - (unsafe_unsigil (`Global bident)) - (trans_type type') - in - print_endline @@ "Warn: global undeclared " ^ Var.name v - ^ " assuming mutable unshared"; - v - in + let v = lookup_global_decl bident ~typ:(trans_type type') prog in assign_var prog v | LVar_Local (LocalUntyped bident) -> let v = lookup_local_decl bident prog in @@ -1038,13 +1072,13 @@ module BasilASTLoader = struct EndList _ ) -> tx name attribs phi statements jump - and param_to_lvar (pp : params) : Var.t = + and param_to_formal (p : Var.generator) (pp : params) : string * Var.t = match pp with - | Params1 (LocalIdent (pos, id), t) -> Var.create id (trans_type t) + | Params1 (LocalIdent (pos, id), t) -> + (id, p.with_name id ~access:None (trans_type t)) - and param_to_formal (pp : params) : string * Var.t = - match pp with - | Params1 (LocalIdent (pos, id), t) -> (id, Var.create id (trans_type t)) + and param_names (pp : params) : string * Types.t = + match pp with Params1 (LocalIdent (pos, id), t) -> (id, trans_type t) and trans_funspec prog bound_post (spec : (Var.t, BasilExpr.t) Procedure.proc_spec) (s : funSpec) : @@ -1129,22 +1163,25 @@ module BasilASTLoader = struct | _ -> fail ()) | _ -> fail () - and lookup_global_decl ident p_st = + and lookup_global_decl ?typ ident p_st = + (* FIXME: evantually should not need lookup, should be able to locally construct compatible var*) let vn = unsafe_unsigil (`Global ident) in let token_char_offset_range = Some (loc_ident (`Global ident)) in - match Program.get_decl_by_name vn p_st.prog with - | Some (Variable { binding }) -> binding - | Some (Function { binding }) -> binding - | Some (Type _) -> + match (typ, Program.get_decl_by_name vn p_st.prog) with + | _, Some (Variable { binding }) -> binding + | _, Some (Function { binding }) -> binding + | _, Some (Type _) -> let msg = "found type declaration when looking for variable:" ^ vn in raise (LoadError { token_char_offset_range; msg; input = None }) - | None -> ( + | Some ty, None -> + Program.var_generator p_st.prog |> fun v -> v.with_name vn ty + | None, None -> ( match Program.get_implicit_decl_by_name vn p_st.prog with | Some (VariantCase { constructor }) -> constructor | None -> let msg = "global variable used before declaration : " ^ vn in raise (LoadError { token_char_offset_range; msg; input = None })) - | Some (Procedure _) -> failwith "" + | _, Some (Procedure _) -> failwith "got proc when expecting global var" and trans_bv_val v : Bitvec.t = match v with @@ -1184,7 +1221,8 @@ module BasilASTLoader = struct failwith ("Invalid type constuctor name: " ^ g ^ " must start with lowercase.") - | `Global (GlobalIdent (pos, g)) -> g + | `Global (GlobalIdent (pos, g)) -> + String.chop_prefix ~pre:"$" g |> Option.get_or ~default:g | `Local (LocalIdent (pos, g)) -> g | `Proc (ProcIdent (pos, g)) -> g | `Block (BlockIdent (pos, g)) -> g @@ -1243,19 +1281,7 @@ module BasilASTLoader = struct | Expr_Global (GlobalUntyped g) -> BasilExpr.rvar @@ lookup_global_decl g p_st | Expr_Global (GlobalTyped (g, type')) -> - let v = - try lookup_global_decl g p_st - with e -> - let v = - Var.create ~scope:GlobalVar - (unsafe_unsigil (`Global g)) - (trans_type type') - in - Logs.warn (fun m -> - m "Warn: undeclared global referenced in expr, %s" - (Var.to_string v)); - v - in + let v = lookup_global_decl g p_st in BasilExpr.rvar v | Expr_Local (LocalUntyped g) -> BasilExpr.rvar @@ lookup_local_decl ~binds g p_st @@ -1263,7 +1289,8 @@ module BasilASTLoader = struct try BasilExpr.rvar @@ lookup_local_decl ~binds g p_st with Not_found | LoadError _ -> let v = - Var.create ~scope:LocalVar + Procedure.get_local + (p_st.curr_proc |> Option.get_exn_or "no current proc") (unsafe_unsigil (`Local g)) (trans_type type') in @@ -1353,10 +1380,11 @@ module BasilASTLoader = struct let _, attrib = trans_attrib_set ~binds p_st attrs in BasilExpr.lambda ~attrib ~bound (trans_expr ~nbinds:bound e) | Expr_Let (id, param, rt, body, in_expr) -> - let id = unsafe_unsigil (`Local id) in let bound = unpac_lambdaparen ~bound:StringMap.empty p_st param in let funct = Types.curry (List.map Var.typ bound) (trans_type rt) in - let funvar = Var.create id funct ~scope:LocalConst in + let id = unsafe_unsigil (`Local id) in + (* assume no shadowing *) + let funvar = (local_var_gen p_st).with_name id funct ~access:Const in let func = match bound with | [] -> trans_expr ~nbinds:bound body @@ -1588,7 +1616,14 @@ let protect_parse parsefun = let load_single_block_proc ?(proc = "") ?input lexbuf = let block = protect_parse BasilIR.ParBasilIR.pBlock input lexbuf in let prog, proc = Program.create_single_proc ~name:proc () in - let st = { prog; params_order = Hashtbl.create 30; curr_proc = Some proc } in + let st = + { + prog; + params_order = Hashtbl.create 30; + curr_proc = Some proc; + local_id_gen = Some (Procedure.local_ids proc); + } + in let st, bl = BasilASTLoader.trans_block st block in let bl = BasilASTLoader.conv_lblock [] proc bl in let proc, bid = @@ -1601,7 +1636,14 @@ let load_single_block_proc ?(proc = "") ?input lexbuf = Procedure.G.add_edge g (End bid) Return) proc in - let bl = Procedure.get_block proc bid |> Option.get_exn_or "" in + let bl = + Procedure.get_block proc bid |> Option.get_exn_or "no current proc" + in + let prog = + Block.free_vars bl |> VarSet.filter Var.is_global |> fun vs -> + VarSet.fold (fun v p -> Program.add_var_decl p v) vs prog + in + let prog = Spec_modifies.set_modsets prog in let inparam = Block.free_vars bl |> VarSet.filter Var.is_local |> VarSet.to_list |> List.map (fun x -> (Var.name x, x)) @@ -1609,16 +1651,6 @@ let load_single_block_proc ?(proc = "") ?input lexbuf = in let proc = Procedure.map_formal_in_params (fun _ -> inparam) proc in let prog = Program.add_proc proc prog in - let prog = - Iter.append (Block.read_vars_iter bl) (Block.assigned_vars_iter bl) - |> Iter.filter Var.is_global - |> Iter.fold - (fun prog v -> - Program.add_decl prog - (Program.Variable - { binding = v; attrib = StringMap.empty; classification = None })) - prog - in (prog, proc, bl) let load_single_block ?proc ~input lexbuf = @@ -1864,6 +1896,7 @@ proc @c() -> () ]; |} in + print_endline "globals: "; let res = analyse prog.prog in Iter.iter (fun (pid, proc) -> @@ -1871,6 +1904,7 @@ proc @c() -> () (Program.procs prog.prog); [%expect {| + globals: @entry: read: $R0:bv64,$R1:bv64,$mem:(bv64->bv8) written: $R0:bv64,$mem:(bv64->bv8) @@ -1882,7 +1916,7 @@ proc @c() -> () written: $mem:(bv64->bv8) |}] -let%test_unit "parses parenthesised lambda param" = +let%expect_test "parses parenthesised lambda param" = let s = {| let $memory_load32_le : (bv64 -> bv8) -> bv64 -> bv32 = fun (#memory: bv64 -> bv8), (#index: bv64) :: @@ -1892,6 +1926,7 @@ let%test_unit "parses parenthesised lambda param" = load_le(8, #memory, #index))))); |} in + Printexc.record_backtrace true; let _ = ast_of_string ~__LINE__ ~__FILE__ ~__FUNCTION__ s in () diff --git a/lib/script.ml b/lib/script.ml index 6c5ed5cb..687a0cc5 100644 --- a/lib/script.ml +++ b/lib/script.ml @@ -317,7 +317,12 @@ let load_gtirb st fname = | Ok e -> Loader.Loadir.( Some - { prog = e; curr_proc = None; params_order = Hashtbl.create 0 }) + { + prog = e; + curr_proc = None; + params_order = Hashtbl.create 0; + local_id_gen = None; + }) | _ -> None in { st with load_st = p }) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index bea9f319..a8aafd23 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -88,7 +88,7 @@ let next_aarch64_stmt stmts = (** Returns the Bincaml global variable representing heap memory. *) let aarch64_mem_of_prog prog = - Program.get_decl_by_name "$mem" prog |> function + Program.get_decl_by_name "mem" prog |> function | Some (Variable { binding }) -> binding | _ -> failwith "aarch64_mem_of_prog: no $mem found" @@ -175,9 +175,9 @@ let rec transform_block (module I : Bincaml_ibi.IBI) ~proc bid = (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics of all blocks within the given procedure. *) -let transform_procedure ~memory proc = +let transform_procedure prog ~memory proc = let memory = Fun.const memory in - let module I = (val Bincaml_ibi.from_bincaml_procedure ~memory proc) in + let module I = (val Bincaml_ibi.from_bincaml_procedure prog ~memory proc) in Procedure.iter_blocks proc |> Iter.fold (fun proc (bid, _) -> transform_block (module I) ~proc bid) proc @@ -192,8 +192,12 @@ let add_aarch64_global_declarations ?(add_all = false) prog = |> Iter.to_set (module VarSet)) in - Lazy.force Aslp_lexpr.global_vars - |> List.to_iter |> Iter.filter include_var + let gen = + Aslp_lexpr.aslp_ids_from_generators ~local_var:(Var.mk_gen ()) + ~global_var:(Program.var_generator prog) + in + + Aslp_lexpr.global_vars gen |> List.to_iter |> Iter.filter include_var |> Iter.fold (fun prog var -> let attrib = Attrib.empty and classification = None in @@ -210,7 +214,7 @@ let transform_program prog = let memory = aarch64_mem_of_prog prog in prog - |> Program.map_procedures (fun _ -> transform_procedure ~memory) + |> Program.map_procedures (fun _ -> transform_procedure prog ~memory) |> add_aarch64_global_declarations (** {1 Supplementary transformation} *) diff --git a/lib/transforms/aslp/aslp_lexpr.ml b/lib/transforms/aslp/aslp_lexpr.ml index ceaeff31..2d041f2c 100644 --- a/lib/transforms/aslp/aslp_lexpr.ml +++ b/lib/transforms/aslp/aslp_lexpr.ml @@ -38,6 +38,15 @@ type t = | ExclusiveLocal [@@deriving show { with_path = false }] +let predefined = + [ PC; SP_EL0 ] + @ List.init 31 (fun i -> R (Some i)) + @ List.init 31 (fun i -> Z (Some i)) + @ [ FPSR; FPCR; PSTATE_N; PSTATE_Z; PSTATE_C; PSTATE_V ] + @ [ PSTATE_A; PSTATE_D; PSTATE_DIT; PSTATE_F; PSTATE_I ] + @ [ PSTATE_PAN; PSTATE_SP; PSTATE_SSBS; PSTATE_TCO; PSTATE_UAO; PSTATE_BTYPE ] + @ [ BTypeCompatible; BranchTaken; BTypeNext; ExclusiveLocal ] + let typ (x : t) = let bv = Types.bv in match x with @@ -58,7 +67,7 @@ let typ (x : t) = | ExclusiveLocal -> Types.Boolean | R None | Z None -> failwith "typeof_lexpr: array lexpr has no bincaml type" -let name = function +let name : _ -> string = function | Local (v, _) -> v | SP_EL0 -> "SP" | R (Some n) -> Printf.sprintf "R%d" n @@ -66,30 +75,40 @@ let name = function | R None | Z None -> failwith "name_of_lexpr: array lexpr has no bincaml name" | v -> show v -let scope = function - | Local _ -> Var.LocalVar - | BranchTaken | BTypeCompatible | BTypeNext -> LocalVar - | _ -> GlobalVar +type aslp_ids = { local_var : Var.generator; global_var : Var.generator } +(** Generators for unique IDs used by the offline lifter. The {!aslp_ids} is + stateful and the same {!aslp_ids} should be used by all opcodes within the + same procedure, to ensure that IDs are unique.*) -let to_var x = - let ty = typ x and name = name x and scope = scope x in - let name = match scope with GlobalVar -> "$" ^ name | _ -> name in - Var.create ~scope name ty +(** Construct a new {!aslp_ids} with no pre-existing IDs. -let pc_var = to_var PC -let branchtaken_var = to_var BranchTaken + Be careful! You should use {!aslp_ids_from_generators} if you will use the + lifted statements within an existing Bincaml IR. *) +let empty_aslp_ids () = + let local_var = Var.mk_gen () in + let global_var = Var.mk_gen ~scope:`Global () in + { local_var; global_var } -let predefined = - lazy - ([ PC; SP_EL0 ] - @ List.init 31 (fun i -> R (Some i)) - @ List.init 31 (fun i -> Z (Some i)) - @ [ FPSR; FPCR; PSTATE_N; PSTATE_Z; PSTATE_C; PSTATE_V ] - @ [ PSTATE_A; PSTATE_D; PSTATE_DIT; PSTATE_F; PSTATE_I ] - @ [ - PSTATE_PAN; PSTATE_SP; PSTATE_SSBS; PSTATE_TCO; PSTATE_UAO; PSTATE_BTYPE; - ] - @ [ BTypeCompatible; BranchTaken; BTypeNext; ExclusiveLocal ]) +(** {2 ID-generating functions} *) + +(** Construct a {!aslp_ids} with the given {!Bincaml_util.ID.generator}s as + underlying generators. + + This will ensure that ASLp's local variable and block names do not clash + with existing names. *) +let aslp_ids_from_generators ~local_var ~global_var = { local_var; global_var } + +let scope st = function + | Local _ -> st.local_var + | BranchTaken | BTypeCompatible | BTypeNext -> st.local_var + | _ -> st.global_var + +let to_var st x = + let ty = typ x and name = name x and scope = scope st x in + scope.with_name name ty + +let global_vars gen = + predefined |> List.map (to_var gen) %> List.filter Var.is_global -let global_vars = - predefined |> Lazy.map (List.map to_var %> List.filter Var.is_global) +let pc_var st = to_var st PC +let branchtaken_var st = to_var st BranchTaken diff --git a/lib/transforms/aslp/aslp_state.ml b/lib/transforms/aslp/aslp_state.ml index 7701255c..f420d602 100644 --- a/lib/transforms/aslp/aslp_state.ml +++ b/lib/transforms/aslp/aslp_state.ml @@ -37,19 +37,13 @@ type aslp_diamond = aslp_block Diamond.diamond [@@deriving show] it is not the representation which is used {i during} lifting. For the "in-progress" representation, see {!diamond}. *) -type aslp_ids = { local_id : unit -> string } -(** Generators for unique IDs used by the offline lifter. - - The {!aslp_ids} is stateful and the same {!aslp_ids} should be used by all - opcodes within the same procedure, to ensure that IDs are unique.*) - type lifter_state = { address : Bitvec.t option; (** Byte address of the instruction currently being lifted. *) diamond : aslp_block Diamond_zipper.zipper; (** Lifter state representing a control flow diamond while it is being built. *) - generator : aslp_ids; [@opaque] (** Generators for ID names. *) + generator : Aslp_lexpr.aslp_ids; [@opaque] (** Generators for ID names. *) names : (string, string) Hashtbl.t; (** Map of ASLp local variable names to the "ID-ified" names produced for Bincaml. @@ -86,25 +80,6 @@ let empty_lifter_state ~generator () = generator; } -(** Construct a new {!aslp_ids} with no pre-existing IDs. - - Be careful! You should use {!aslp_ids_from_generators} if you will use the - lifted statements within an existing Bincaml IR. *) -let empty_aslp_ids () = - let local_id = Fix.Gensym.make () %> Printf.sprintf "var_%d" in - { local_id } - -(** {2 ID-generating functions} *) - -(** Construct a {!aslp_ids} with the given {!Bincaml_util.ID.generator}s as - underlying generators. - - This will ensure that ASLp's local variable and block names do not clash - with existing names. *) -let aslp_ids_from_generators ~local_ids = - let local_id = ID.fresh ~name:"var" local_ids %> ID.name in - { local_id } - (** {1 State manipulation functions} *) (** Appends the given statement to the given block. @@ -113,11 +88,11 @@ let aslp_ids_from_generators ~local_ids = is assumed that [PC] is assigned at most once on any straight-line path. Raises an exception if the statement is an assignment to [PC] and {!pc_assign} is already set. *) -let add_stmt_to_block ?(allow_double_pc = false) ~stmt blk = +let add_stmt_to_block gen ?(allow_double_pc = false) ~stmt blk = let pc_assign = match stmt with | Stmt.Instr_Assign { al = assigns; _ } -> - assigns |> List.Assoc.get ~eq:Var.equal Aslp_lexpr.pc_var + assigns |> List.Assoc.get ~eq:Var.equal (Aslp_lexpr.pc_var gen) | _ -> None in match (pc_assign, blk.pc_assign) with @@ -131,24 +106,28 @@ let add_stmt_to_block ?(allow_double_pc = false) ~stmt blk = let add_stmt_to_active stmt (lifter_state : lifter_state) = let diamond = lifter_state.diamond in - let diamond = diamond |> Diamond_zipper.modify (add_stmt_to_block ~stmt) in + let diamond = + diamond + |> Diamond_zipper.modify (add_stmt_to_block lifter_state.generator ~stmt) + in { lifter_state with diamond } (** {1 Program counter and guard functions} *) (** Ensures that the focused block has a PC assignment. If it already has {!pc_assign}, no changes are made. *) -let ensure_pc_assigned ~address = +let ensure_pc_assigned gen ~address = Diamond_zipper.modify (function | { pc_assign = None } as block -> let incremented = Expr.BasilExpr.bvconst Bitvec.(add address (of_int ~size:64 4)) and ff = Expr.BasilExpr.boolconst false in - let bt = Aslp_lexpr.branchtaken_var and pc = Aslp_lexpr.pc_var in + let bt = Aslp_lexpr.branchtaken_var gen + and pc = Aslp_lexpr.pc_var gen in let al = [ (bt, ff); (pc, incremented) ] in block - |> add_stmt_to_block + |> add_stmt_to_block gen ~stmt:(Stmt.Instr_Assign { attrib = Attrib.empty; al }) | block -> block) @@ -170,15 +149,15 @@ let ensure_pc_assigned ~address = This is used to maintain the invariant that at every control flow point, the [PC] variable is either assigned on all paths or assigned on no paths (from the beginning of the instruction). *) -let ensure_pc_consistency ~address state = +let ensure_pc_consistency gen ~address state = let left = state |> Diamond_zipper.move_in_to `L |> Result.get_ok and right = state |> Diamond_zipper.move_in_to `R |> Result.get_ok in (* Make PCs of left and right agree. Resulting state is at left or right. *) let state = match Diamond_zipper.((focus left).pc_assign, (focus right).pc_assign) with - | Some _, None -> right |> ensure_pc_assigned ~address - | None, Some _ -> left |> ensure_pc_assigned ~address + | Some _, None -> right |> ensure_pc_assigned gen ~address + | None, Some _ -> left |> ensure_pc_assigned gen ~address | None, None | Some _, Some _ -> left (* arbitrary *) in @@ -204,7 +183,7 @@ let ensure_pc_consistency ~address state = If the PC was assigned earlier, inserts a new assignment in the last block. This is semantically redundant, but is meant to simplify guard cleanup. *) -let ensure_forwarded_pc state = +let ensure_forwarded_pc gen state = match Diamond_zipper.(move_in_to `L state, move_in_to `R state) with | Error _, _ | _, Error _ -> state (* focus is not a branch *) | Ok l, Ok r -> ( @@ -215,11 +194,11 @@ let ensure_forwarded_pc state = Option.get_exn_or "invariant violation: pc should be propagated" (Diamond_zipper.focus state).pc_assign in - let al = [ (Aslp_lexpr.pc_var, pc_assign) ] in + let al = [ (Aslp_lexpr.pc_var gen, pc_assign) ] in let stmt = Stmt.Instr_Assign { attrib = Attrib.empty; al } in state |> Diamond_zipper.modify - (add_stmt_to_block ~stmt ~allow_double_pc:true) + (add_stmt_to_block gen ~stmt ~allow_double_pc:true) | Some _, None | None, Some _ -> failwith "pcs should already agree") (** Returns an {!Lang.Stmt.Instr_Assume} statement for the given block's guard, diff --git a/lib/transforms/aslp/bincaml_ibi.ml b/lib/transforms/aslp/bincaml_ibi.ml index d18180ab..f70b802a 100644 --- a/lib/transforms/aslp/bincaml_ibi.ml +++ b/lib/transforms/aslp/bincaml_ibi.ml @@ -30,6 +30,8 @@ let from_generator ?(memory = fun () -> failwith "bincaml_memory_var undefined") (** Builds a new {!IBI} where the ID generators are derived from the given procedure. *) -let from_bincaml_procedure ?memory proc : (module IBI) = - let local_ids = Procedure.local_ids proc in - from_generator ?memory (Aslp_state.aslp_ids_from_generators ~local_ids) +let from_bincaml_procedure prog ?memory proc : (module IBI) = + let local_var = Procedure.var_generator proc in + let global_var = Program.var_generator prog in + from_generator ?memory + (Aslp_lexpr.aslp_ids_from_generators ~local_var ~global_var) diff --git a/lib/transforms/aslp/bincaml_ibi_make.ml b/lib/transforms/aslp/bincaml_ibi_make.ml index 5291cafc..763d3c32 100644 --- a/lib/transforms/aslp/bincaml_ibi_make.ml +++ b/lib/transforms/aslp/bincaml_ibi_make.ml @@ -37,7 +37,10 @@ struct let id_name = match Hashtbl.find_opt !bincaml_lifter_state.names name with | None -> - let id_name = !bincaml_lifter_state.generator.local_id () in + let id_name = + ID.name @@ Var.id + @@ !bincaml_lifter_state.generator.local_var.fresh ty + in Hashtbl.replace !bincaml_lifter_state.names name id_name; id_name | Some x -> x @@ -77,7 +80,11 @@ struct | `M -> let address = bincaml_get_address () and diamond = !bincaml_lifter_state.diamond in - let diamond = diamond |> Aslp_state.ensure_pc_consistency ~address in + let diamond = + diamond + |> Aslp_state.ensure_pc_consistency !bincaml_lifter_state.generator + ~address + in bincaml_lifter_state := { !bincaml_lifter_state with diamond } (** {2 IR extraction} *) @@ -94,8 +101,10 @@ struct failwith "invariant violation: context switches did not return to merge" | [] -> diamond - |> Aslp_state.ensure_pc_assigned ~address - |> Aslp_state.ensure_forwarded_pc |> Diamond_zipper.to_diamond + |> Aslp_state.ensure_pc_assigned !bincaml_lifter_state.generator + ~address + |> Aslp_state.ensure_forwarded_pc !bincaml_lifter_state.generator + |> Diamond_zipper.to_diamond (** {2 Instruction building interface implementation} *) @@ -254,12 +263,12 @@ struct let f_gen_bool_lit : bool -> expr = Expr.BasilExpr.boolconst let f_gen_int_lit : bigint -> expr = Expr.BasilExpr.intconst + let to_var v = Aslp_lexpr.to_var !bincaml_lifter_state.generator v let f_gen_store : lexpr -> expr -> unit = fun lhs rhs -> bincaml_internal_emit - (Stmt.Instr_Assign - { attrib = Attrib.empty; al = [ (Aslp_lexpr.to_var lhs, rhs) ] }) + (Stmt.Instr_Assign { attrib = Attrib.empty; al = [ (to_var lhs, rhs) ] }) let f_decl_bv : string -> bigint -> lexpr = fun name size -> @@ -273,8 +282,7 @@ struct f_gen_store v (f_gen_bool_lit false); v - let f_gen_load : lexpr -> expr = - fun lhs -> Expr.BasilExpr.rvar (Aslp_lexpr.to_var lhs) + let f_gen_load : lexpr -> expr = fun lhs -> Expr.BasilExpr.rvar (to_var lhs) let f_gen_array_load : lexpr -> bigint -> expr = fun array idx -> @@ -311,8 +319,9 @@ struct fun size addr _ _acctype -> let addr = Stmt.Addr { addr; size = Z.to_int size; endian = `Little } and mem = S.bincaml_memory_var () in - let name = !bincaml_lifter_state.generator.local_id () in - let rhs = Var.create name (Types.bv (Z.to_int size)) in + let rhs = + !bincaml_lifter_state.generator.local_var.fresh (Types.bv (Z.to_int size)) + in bincaml_internal_emit (Stmt.Instr_Load { attrib = Attrib.empty; lhs = mem; rhs; addr }); Expr.BasilExpr.rvar rhs diff --git a/lib/transforms/boogie_prepass.ml b/lib/transforms/boogie_prepass.ml index 7752d7e9..d89e3735 100644 --- a/lib/transforms/boogie_prepass.ml +++ b/lib/transforms/boogie_prepass.ml @@ -63,8 +63,8 @@ module Builtins = struct | `BVNEG -> "bvneg" | `ZeroExtend sz -> Printf.sprintf "zero_extend %d" sz | `SignExtend sz -> Printf.sprintf "sign_extend %d" sz - | `Load (`Big, i) -> Printf.sprintf "load%d_be" i - | `Load (`Little, i) -> Printf.sprintf "load%d_le" i + | `Load (`Big, i) -> Printf.sprintf "$load%d_be" i + | `Load (`Little, i) -> Printf.sprintf "$load%d_le" i (** Returns the monomorphized builtin name *) let monomorphize_builtin (op : builtin) targs = @@ -151,14 +151,15 @@ module Builtins = struct s.rely |> List.iter (iexpr f); s.guarantee |> List.iter (iexpr f) - let function_for_op op args ret = - Var.create ~scope:Var.GlobalConst - (match name op (args @ [ ret ]) with + let function_for_op (pid : Var.generator) op args ret = + let name = + match name op (args @ [ ret ]) with | Function s -> s - | _ -> failwith "unexpected") - (Types.curry args ret) + | _ -> failwith "unexpected" + in + pid.with_name name ~access:Var.Const (Types.curry args ret) - let transform_op_to_decl op args ret = + let transform_op_to_decl pid op args ret = let boogie_attribs = StringMap.of_list [ @@ -170,8 +171,9 @@ module Builtins = struct Some (Function { + var_gen = Var.mk_gen ~scope:`Local (); attrib = attribs; - binding = function_for_op op args ret; + binding = function_for_op pid op args ret; definition = Uninterpreted; } : Program.declaration) @@ -179,29 +181,81 @@ module Builtins = struct let used_ops (p : Program.t) = Iter.from_iter (fun f -> iprog f p) |> Iter.sort_uniq + let expr_ops vargen (e : Types.t Expr.BasilExpr.abstract_expr) = + let open Expr.AbstractExpr in + let open Ops.AllOps in + let get_ty (op : [ unary | binary | intrin ]) o = + match o with + | Fun { ret; args } -> ( + try Some (function_for_op vargen op args ret) with Failure _ -> None) + | _ -> None + in + match e with + | UnaryExpr { op = #unary as op; arg; _ } -> + ret_type_unary op arg |> get_ty op + | BinaryExpr { op = #binary as op; arg1 = l; arg2 = r; _ } -> + ret_type_bin op l r |> get_ty op + | ApplyIntrin { op = #intrin as op; args; _ } -> + ret_type_intrin op args |> get_ty op + | _ -> None + + let transform_builtin_decls (p : Program.t) : Program.t = + let v = Program.var_generator p in + let bvop_alg : + (Program.e * Types.t) Expr.BasilExpr.abstract_expr -> Program.e option = + fun e -> + let open Expr.AbstractExpr in + let types = map snd e in + let ex = map fst e in + match ex with + | ApplyIntrin { op = `BVConcat | `AND | `OR | `Cases | `MapUpdate } -> + None + | BinaryExpr { op; arg1; arg2 } -> ( + match expr_ops v types with + | Some func -> + Some + (Expr.BasilExpr.apply_fun ~func:(Expr.BasilExpr.rvar func) + [ arg1; arg2 ]) + | None -> None) + | ApplyIntrin { op; args } -> ( + match expr_ops v types with + | Some func -> + Some + (Expr.BasilExpr.apply_fun ~func:(Expr.BasilExpr.rvar func) args) + | None -> None) + | _ -> None + in + let rw_expr ?visit (e : Expr.BasilExpr.t) = + Expr.BasilExpr.rewrite_typed bvop_alg e + in + Cf_tx.simplify_all rw_expr p + let transform_add_builtin_decls (p : Program.t) : Program.t = used_ops p |> Iter.filter_map (function op, args, ret -> (match op with | `Load _ -> None - | #builtin as op -> transform_op_to_decl op args ret + | #builtin as op -> + transform_op_to_decl (Program.var_generator p) op args ret | _ -> None)) |> Iter.to_list - |> List.fold_left Program.add_decl p + |> List.fold_left (fun p v -> Program.add_decl p v) p end module Instructions = struct let unique_stores_loads (prog : Program.t) = let visit_procs proc = Procedure.iter_stmt_topo_fwd proc in + (* we only care about the type of these vars to generate placeholder memory ops *) + let g = Var.mk_gen () in let load_exprs : (Var.t, Var.t, Program.e) Stmt.t Iter.t = Builtins.used_ops prog |> Iter.filter_map (function op, args, ret -> (match op with | `Load (endian, size) -> - let lhs = Var.create "" ret in - let rhs = Var.create "" (List.hd args) in + let lhs = g.fresh ret in + let rhs = g.fresh (List.hd args) in let addr = - Expr.BasilExpr.rvar @@ Var.create "" (List.hd @@ List.tl args) + Expr.BasilExpr.rvar @@ g.fresh (List.hd @@ List.tl args) in Some (Stmt.Instr_Load @@ -226,13 +280,10 @@ module Instructions = struct |> Iter.sort_uniq let store_body ?(be = false) mem_typ val_size addr_size = - let memory = Var.create ~scope:Var.LocalVar "#memory" mem_typ in - let value = - Var.create ~scope:Var.LocalVar "#value" (Types.Bitvector val_size) - in - let index = - Var.create ~scope:Var.LocalVar "#index" (Types.Bitvector addr_size) - in + let v = Var.mk_gen ~scope:`Local () in + let memory = v.with_name "#memory" mem_typ in + let value = v.with_name "#value" (Types.Bitvector val_size) in + let index = v.with_name "#index" (Types.Bitvector addr_size) in (* TODO: maybe generalize to non 8 bit stores, based on mem typ value? *) let steps = val_size / 8 in let body = @@ -255,13 +306,12 @@ module Instructions = struct ]) (Expr.BasilExpr.rvar memory) in - Expr.BasilExpr.lambda ~bound:[ memory; index; value ] body + (v, Expr.BasilExpr.lambda ~bound:[ memory; index; value ] body) let load_body ?(be = false) mem_typ val_size addr_size = - let memory = Var.create ~scope:Var.LocalVar "#memory" mem_typ in - let index = - Var.create ~scope:Var.LocalVar "#index" (Types.Bitvector addr_size) - in + let v = Var.mk_gen ~scope:`Local () in + let memory = v.with_name "#memory" mem_typ in + let index = v.with_name "#index" (Types.Bitvector addr_size) in let steps = val_size / 8 in let body = (if be then List.range 0 (steps - 1) else List.range (steps - 1) 0) @@ -285,9 +335,9 @@ module Instructions = struct (Bitvec.of_int ~size:addr_size (if be then 0 else steps - 1))))) in - Expr.BasilExpr.lambda ~bound:[ memory; index ] body + (v, Expr.BasilExpr.lambda ~bound:[ memory; index ] body) - let store_load_decl (s : Program.stmt) = + let store_load_decl (global_vargen : Var.generator) (s : Program.stmt) = match s with | Stmt.Instr_Store { lhs; rhs; value; addr = Addr { addr; size; endian } } -> @@ -295,7 +345,7 @@ module Instructions = struct StringMap.of_list [ (".extern", `List []); (".define", `List []) ] in let attribs = StringMap.singleton ".boogie" (`Assoc boogie_attribs) in - let body = + let var_gen, body = store_body (Var.typ rhs) (match Expr.BasilExpr.type_of value with | Types.Bitvector s -> s @@ -308,9 +358,10 @@ module Instructions = struct (Function { attrib = attribs; + var_gen; binding = - Var.create ~scope:Var.GlobalConst - (Printf.sprintf "store%d_%s" size + global_vargen.with_name ~access:Var.Const + (Printf.sprintf "$store%d_%s" size (Lang.Stmt.show_endian endian)) (Lang.Expr.BasilExpr.type_of value); definition = Lang.Program.Function body; @@ -321,7 +372,7 @@ module Instructions = struct let attribs = StringMap.of_list [ (".boogie", `Assoc boogie_attribs) ] in - let body = + let var_gen, body = load_body (Var.typ rhs) (match Var.typ lhs with | Types.Bitvector s -> s @@ -334,9 +385,10 @@ module Instructions = struct (Function { attrib = attribs; + var_gen; binding = - Var.create ~scope:Var.GlobalConst - (Printf.sprintf "load%d_%s" size (Stmt.show_endian endian)) + global_vargen.with_name ~access:Var.Const + (Printf.sprintf "$load%d_%s" size (Stmt.show_endian endian)) (Var.typ lhs); definition = Function body; } @@ -345,7 +397,7 @@ module Instructions = struct let transform_add_store_load_decls (prog : Program.t) = unique_stores_loads prog - |> Iter.filter_map store_load_decl + |> Iter.filter_map (store_load_decl (Program.var_generator prog)) |> Iter.fold Program.add_decl prog end @@ -373,11 +425,11 @@ module Normalise = struct (* function application in boogie becomes a map access when on lambdas (identified by local vars) *) | ApplyFun { func; args } -> ( match unfix func with + (*| RVar { attrib; id } when Var.is_local id -> failwith ( "is local var: " ^ Var.show id)*) | RVar { attrib; id } when Var.is_global id -> replace [%here] (BasilExpr.apply_fun ~attrib - ~func: - (BasilExpr.rvar ~attrib (Var.copy ~name:(Var.name id) id)) + ~func:(BasilExpr.rvar ~attrib id) args) | _ -> replace [%here] (apply_fun_to_map func args)) | ApplyIntrin { op = `AND; args } -> @@ -400,7 +452,7 @@ module Normalise = struct open Stmt - let replace_stmt (s : Program.stmt) = + let replace_stmt ~(global_vars : Var.generator) (s : Program.stmt) = match s with | Instr_IndirectCall { attrib } -> Instr_Assert @@ -414,7 +466,7 @@ module Normalise = struct Instr_Assign { al = [ (lhs, value) ]; attrib } | Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } -> let fn_name = - Printf.sprintf "load%d_%s" size (Stmt.show_endian endian) + Printf.sprintf "$load%d_%s" size (Stmt.show_endian endian) in Instr_Assign { @@ -423,7 +475,8 @@ module Normalise = struct ( lhs, Expr.BasilExpr.fapply (Expr.BasilExpr.rvar - (Var.create ~scope:Var.GlobalConst fn_name (Var.typ lhs))) + (global_vars.with_name ~access:Var.Const fn_name + (Var.typ lhs))) [ Expr.BasilExpr.rvar rhs; addr ] ); ]; attrib; @@ -431,7 +484,7 @@ module Normalise = struct | Instr_Store { lhs; rhs; value; addr = Addr { addr; size; endian }; attrib } -> let fn_name = - Printf.sprintf "store%d_%s" size (Stmt.show_endian endian) + Printf.sprintf "$store%d_%s" size (Stmt.show_endian endian) in Stmt.Instr_Assign { @@ -440,7 +493,8 @@ module Normalise = struct ( lhs, Expr.BasilExpr.fapply (Expr.BasilExpr.rvar - (Var.create ~scope:Var.GlobalConst fn_name (Var.typ lhs))) + (global_vars.with_name ~access:Var.Const fn_name + (Var.typ lhs))) [ Expr.BasilExpr.rvar rhs; addr; value ] ); ]; attrib; @@ -458,28 +512,35 @@ module Normalise = struct let replace_functions (p : Program.t) = let open Program in + let vg = Program.var_generator p in let prog = Program.flat_map_decls (fun k -> function - | Function { binding; attrib; definition } -> ( + | Function { binding; attrib; definition; var_gen } -> ( let keep = - Iter.singleton (Function { binding; attrib; definition }) + Iter.singleton + (Function { binding; attrib; definition; var_gen }) in match definition with | Function b -> ( match BasilExpr.unfix b with | Lambda { bound_vars; in_body } -> keep | body -> - let axiom_name = - Program.declare_name_exn (ID.name k ^ "_funvalue") p - in + let axiom_name = ID.name k ^ "_funvalue" in Iter.doubleton (Function - { binding; definition = Uninterpreted; attrib }) + { + binding; + definition = Uninterpreted; + attrib; + var_gen; + }) (Function { binding = - Var.copy ~name:(ID.name axiom_name) binding; + vg.with_name axiom_name + ~access:(Var.access binding) (Var.typ binding); + var_gen; definition = Axiom (BasilExpr.binexp ~op:`EQ @@ -494,10 +555,12 @@ module Normalise = struct prog let replace_stmts (p : Program.t) = + let gids = Program.var_generator p in Program.map_procedures (fun _ p -> Procedure.map_blocks_nondet - (fun (id, b) -> Block.map ~phi:Fun.id replace_stmt b) + (fun (id, b) -> + Block.map ~phi:Fun.id (replace_stmt ~global_vars:gids) b) p) p end @@ -505,4 +568,4 @@ end let transform (p : Program.t) = p |> Normalise.replace_functions |> Normalise.replace_exprs |> Instructions.transform_add_store_load_decls |> Normalise.replace_stmts - |> Builtins.transform_add_builtin_decls + |> Builtins.transform_add_builtin_decls |> Builtins.transform_builtin_decls diff --git a/lib/transforms/cf_tx.ml b/lib/transforms/cf_tx.ml index fed14ffe..7827bf67 100644 --- a/lib/transforms/cf_tx.ml +++ b/lib/transforms/cf_tx.ml @@ -49,7 +49,7 @@ let simplify_prog_exprs rewriter ?visit (p : Program.t) = Program.( fun id -> (function - | Function { binding; attrib; definition } -> + | Function { binding; attrib; definition; var_gen } -> let definition = match definition with | Axiom b -> @@ -58,14 +58,19 @@ let simplify_prog_exprs rewriter ?visit (p : Program.t) = | Function b -> Function (rewriter ?visit b) | Uninterpreted -> Uninterpreted in - Function { binding; attrib; definition } + Function { binding; attrib; definition; var_gen } | o -> o)) p +let simplify_all ?visit rewriter prog = + prog + |> simplify_prog_exprs ?visit rewriter + |> simplify_prog_spec_exprs ?visit rewriter + let to_smt (r : Expr.BasilExpr.rwinfo) = let open Lang.Expr_smt in let cexpr = Expr.BasilExpr.binexp ~op:`NEQ r.from r.into in - let smt = snd @@ SMTLib2.assert_bexpr cexpr SMTLib2.empty in + let smt = snd @@ SMTLib2.assert_bexpr cexpr (SMTLib2.empty ()) in smt |> SMTLib2.to_sexp ~set_logic:false let online_check visit (solver : Bincaml_util.Smt.Solver.t) diff --git a/lib/transforms/chc_infer.ml b/lib/transforms/chc_infer.ml index 6628516c..342692d5 100644 --- a/lib/transforms/chc_infer.ml +++ b/lib/transforms/chc_infer.ml @@ -126,15 +126,19 @@ module Encoder = struct mutable premises : Sexp.t list; mutable vars : VarSet.t; (** the clause binders for the eventual [forall] *) - mutable counter : int; + vargen : Var.generator; } let create ~initial_vars = + let vargen = Var.mk_gen () in + List.iter + (fun i -> ignore @@ vargen.with_name (Var.name i) (Var.typ i)) + initial_vars; { delta = VarMap.empty; premises = []; vars = VarSet.of_list initial_vars; - counter = 0; + vargen; } let lookup t v = @@ -153,8 +157,7 @@ module Encoder = struct v let fresh t v = - t.counter <- t.counter + 1; - let nv = Var.copy ~name:(Var.name v ^ "!" ^ string_of_int t.counter) v in + let nv = t.vargen.fresh ~name:(Var.name v) (Var.typ v) in t.delta <- VarMap.add v nv t.delta; t.vars <- VarSet.add nv t.vars; nv diff --git a/lib/transforms/function_summaries.ml b/lib/transforms/function_summaries.ml index 9649af41..2141af47 100644 --- a/lib/transforms/function_summaries.ml +++ b/lib/transforms/function_summaries.ml @@ -22,11 +22,11 @@ module type FunctionSummaryAnnotation = sig end (** Replace gamma expressions with gamma variables for an smt query *) -let normalise_gamma = +let normalise_gamma p = let open Expr.AbstractExpr in let open Expr.BasilExpr in let make_gamma_var v = - rvar (Var.create ("Gamma_" ^ Var.name v) ~scope:(Var.scope v) Boolean) + rvar (Procedure.get_local p ("Gamma_" ^ Var.name v) Boolean) in Expr.BasilExpr.rewrite ~rw_fun:(function | UnaryExpr { op = `Gamma; arg } -> ( @@ -41,7 +41,7 @@ let normalise_gamma = (** `redundant p ps` returns true if the conjunction of `p :: ps` is equivalent to that of `ps`. *) -let redundant (solver : Bincaml_util.Smt.Solver.t) p ps = +let redundant proc (solver : Bincaml_util.Smt.Solver.t) p ps = if Expr.BasilExpr.equal p (Expr.BasilExpr.boolconst true) then Bincaml_util.Smt.Solver.Unsat else if List.is_empty ps then Bincaml_util.Smt.Solver.Sat @@ -49,12 +49,12 @@ let redundant (solver : Bincaml_util.Smt.Solver.t) p ps = try let conj = Expr.BasilExpr.applyintrin ~op:`AND ps in let q = - normalise_gamma @@ Expr.BasilExpr.boolnot + normalise_gamma proc @@ Expr.BasilExpr.boolnot @@ Expr.BasilExpr.binexp ~op:`IMPLIES conj p in let open Expr_smt in let s = - SMTLib2.assert_bexpr q SMTLib2.empty + SMTLib2.assert_bexpr q (SMTLib2.empty ()) |> snd |> SMTLib2.to_sexp ~set_logic:false in @@ -102,7 +102,7 @@ let extra_summary (solver : Bincaml_util.Smt.Solver.t) wp_dual_requires (module S) proc |> List.fold_left (fun rs r -> - match redundant solver r (List.append rs cur_req) with + match redundant proc solver r (List.append rs cur_req) with | Unsat -> rs | Sat -> r :: rs | Unknown -> @@ -114,7 +114,7 @@ let extra_summary (solver : Bincaml_util.Smt.Solver.t) sp_ensures (module S) proc |> List.fold_left (fun rs r -> - match redundant solver r (List.append rs cur_ens) with + match redundant proc solver r (List.append rs cur_ens) with | Unsat -> rs | Sat -> r :: rs | Unknown -> @@ -143,18 +143,32 @@ let add_summary summary (proc : Program.proc) = Procedure.set_specification proc spec let add_decls solver prog = - Program.declarations prog |> Iter.from_iter |> Iter.map snd - |> Iter.filter - Program.( - function - | Type { binding } -> true - | Variable { binding } -> Var.is_constant binding - | Function { binding } -> Var.is_constant binding - | Procedure { definition } -> false) - |> Iter.map (fun d -> Expr_smt.SMTLib2.trans_decl d Expr_smt.SMTLib2.empty) - |> Iter.map fst - |> fun i -> - Iter.for_each i (fun s -> Bincaml_util.Smt.Solver.add_command solver s) + let decls = + Program.declarations prog |> Iter.from_iter |> Iter.map snd + |> Iter.filter + Program.( + function + | Type { binding } -> true + | Variable { binding } -> Var.is_const binding + | Function { binding } -> Var.is_const binding + | Procedure { definition } -> false) + |> Iter.persistent + in + + let add_decls ds = + ds + |> Iter.map (fun d -> + Expr_smt.SMTLib2.trans_decl d (Expr_smt.SMTLib2.empty ())) + |> Iter.map fst + |> fun i -> + Iter.for_each i (fun s -> Bincaml_util.Smt.Solver.add_command solver s) + in + decls + |> Iter.filter Program.(function Type _ -> true | _ -> false) + |> add_decls; + decls + |> Iter.filter Program.(function Type _ -> false | _ -> true) + |> add_decls let intraproc_transform_proc (prog : Program.t) (proc : Program.proc) = let solver = @@ -280,6 +294,12 @@ let solve_component (solver : Bincaml_util.Smt.Solver.t) g (prog : Program.t) IDMap.add pid (append_summary (IDMap.find pid res) (sol pid)) res) component res +let progs_decls_global p = + assert ( + Program.declarations p + |> Iter.for_all (fun (k, v) -> + Program.decl_bound_var v |> Option.for_all Var.is_global)) + let interproc_transform (prog : Program.t) = let call_graph = Program.CallGraph.make_call_graph prog in let sccs = Program.CallGraph.Scc.scc_list call_graph in @@ -290,6 +310,7 @@ let interproc_transform (prog : Program.t) = log = Bincaml_util.Smt.Config.quiet_log; } in + progs_decls_global prog; add_decls solver prog; let summaries = Program.procs prog diff --git a/lib/transforms/gamma_vars.ml b/lib/transforms/gamma_vars.ml index 5aa04aff..82388c2a 100644 --- a/lib/transforms/gamma_vars.ml +++ b/lib/transforms/gamma_vars.ml @@ -18,162 +18,36 @@ open Common variables with gammas are tained by i/o variables, and not actual gamma uses. *) -let check_var v = - assert (not @@ String.starts_with ~prefix:"Gamma_" @@ Var.name v) - -let gamma_of v = - let args, r = Types.uncurry (Var.typ v) in - let typ = Types.curry args Boolean in - Var.copy ~name:("Gamma_" ^ Var.name v) ~typ v - -let add_decl proc gv = - if Var.is_local gv then - Hashtbl.replace (Procedure.local_decls proc) (Var.name gv) gv +let transform_proc ?(check_names = false) (add : ID.t -> Var.t -> bool) prog + (proc : Program.proc) = + let check_var v = + assert (not @@ String.starts_with ~prefix:"Gamma_" @@ Var.name v) + in -let add_globals ?(check_names = false) (add : Var.t -> bool) (p : Program.t) = - Program.declarations p - |> Iter.fold - (fun p (s, decl) -> - match decl with - | Program.Variable { binding; attrib } when add binding -> - if check_names then check_var binding; - Program.decl_global ~attrib p (gamma_of binding) - | _ -> p) - p + (* keep track of introduced vars *) + let added = ref VarSet.empty in -let gamma_expr ?(check_names = false) (add : Var.t -> bool) - (e : Expr.BasilExpr.t) = - (* TODO handle maps ? *) - let vars = - Expr.BasilExpr.free_vars_iter e - |> Iter.map (fun v -> - if check_names then check_var v; + let gamma_of v = + let args, r = Types.uncurry (Var.typ v) in + let name = "Gamma_" ^ Var.name v in + let typ = Types.curry args Boolean in + let v = + if Var.is_global v then ( + let v = + (Program.var_generator prog).with_name ~access:(Var.access v) name typ + in + added := VarSet.add v !added; v) - |> Iter.map gamma_of - |> Iter.map Expr.BasilExpr.rvar - |> List.of_iter + else Procedure.get_local proc name typ + in + v + in + + let add_decl proc gv = + if Var.is_local gv then + Hashtbl.replace (Procedure.local_decls proc) (Var.name gv) gv in - match vars with - | [] -> Expr.BasilExpr.boolconst true - | [ v ] -> v - | l -> Expr.BasilExpr.applyintrin ~op:`AND l - -let update_expr ?(check_names = false) (add : Var.t -> bool) = - (* TODO handle maps ? *) - let open Expr.AbstractExpr in - let open Expr.BasilExpr in - Expr.BasilExpr.rewrite ~rw_fun:(function - | UnaryExpr { attrib; op = `Gamma; arg } -> - replace [%here] (gamma_expr ~check_names add arg) - | _ -> Keep) - -let update_lhs ?(check_names = false) add_cur add_target proc m = - StringMap.fold - (fun s v m -> - if add_cur v && add_target s then ( - if check_names then check_var v; - let gv = gamma_of v in - add_decl proc gv; - StringMap.add ("Gamma_" ^ s) gv m) - else m) - m m - -let update_args ?(check_names = false) add_cur add_target m = - StringMap.fold - (fun s e m -> - let m = StringMap.add s (update_expr ~check_names add_cur e) m in - if add_target s then - StringMap.add ("Gamma_" ^ s) (gamma_expr ~check_names add_cur e) m - else m) - m StringMap.empty - -let update_stmts ?(check_names = false) (add : ID.t -> Var.t -> bool) pid - (prog : Program.t) (b : (Var.t, Expr.BasilExpr.t) Block.t) = - let open Stmt in - let update_expr = update_expr ~check_names (add pid) in - let proc = Program.proc prog pid in - Block.map - ~phi:(fun a -> - List.flat_map - (fun (p : Var.t Block.phi) -> - if add pid p.lhs then ( - if check_names then check_var p.lhs; - let (g : Var.t Block.phi) = - { - lhs = gamma_of p.lhs; - rhs = List.map (fun (id, v) -> (id, gamma_of v)) p.rhs; - } - in - [ p; g ]) - else [ p ]) - a) - (function - | Instr_Assign { al; attrib } -> - let al = - al - |> List.flat_map (fun (l, e) -> - if add pid l then ( - if check_names then check_var l; - let gl = gamma_of l in - let ge = gamma_expr ~check_names (add pid) e in - add_decl proc gl; - [ (gl, ge); (l, e) ]) - else [ (l, e) ]) - in - Instr_Assign { attrib; al } - | Instr_Assert { body; attrib } -> - Instr_Assert { body = update_expr body; attrib } - | Instr_Assume { body; branch; attrib } -> - Instr_Assume { body = update_expr body; branch; attrib } - (* TODO Need atomic statement blocks to capture a "simultaneous op" from normal and gamma mem *) - | Instr_Load _ as s -> s - | Instr_Store _ as s -> s - | Instr_IntrinCall { lhs; name; args; attrib } -> - (* cursed *) - let to_sm lhs = - List.mapi (fun i v -> (Int.to_string i, v)) lhs |> StringMap.of_list - in - let of_sm lhs k = - List.mapi (fun i _ -> StringMap.find (Int.to_string i) k) lhs - in - Instr_IntrinCall - { - lhs = - update_lhs ~check_names (add pid) - (fun _ -> true) - proc (to_sm lhs) - |> of_sm lhs; - name; - attrib; - args = - update_args ~check_names (add pid) (fun _ -> true) (to_sm args) - |> of_sm args; - } - | Instr_Call { lhs; procid; args; attrib } -> - let callee = Program.proc prog procid in - Instr_Call - { - lhs = - update_lhs ~check_names (add pid) - (fun s -> - add procid - (StringMap.find s (Procedure.formal_out_params callee))) - proc lhs; - procid; - attrib; - args = - update_args ~check_names (add pid) - (fun s -> - add procid - (StringMap.find s (Procedure.formal_in_params callee))) - args; - } - | Instr_IndirectCall { target; attrib } -> - Instr_IndirectCall { target = update_expr target; attrib }) - b -let transform_proc ?(check_names = false) (add : ID.t -> Var.t -> bool) prog - (proc : Program.proc) = (* Add gamma in/out vars *) let add_param s v m = if add (Procedure.id proc) v then ( @@ -187,6 +61,146 @@ let transform_proc ?(check_names = false) (add : ID.t -> Var.t -> bool) prog |> Procedure.map_formal_in_params (fun s -> StringMap.fold add_param s s) |> Procedure.map_formal_out_params (fun s -> StringMap.fold add_param s s) in + + let gamma_expr ?(check_names = false) (add : Var.t -> bool) + (e : Expr.BasilExpr.t) = + (* TODO handle maps ? *) + let vars = + Expr.BasilExpr.free_vars_iter e + |> Iter.map (fun v -> + if check_names then check_var v; + v) + |> Iter.map gamma_of + |> Iter.map Expr.BasilExpr.rvar + |> List.of_iter + in + match vars with + | [] -> Expr.BasilExpr.boolconst true + | [ v ] -> v + | l -> Expr.BasilExpr.applyintrin ~op:`AND l + in + + let update_expr ?(check_names = false) (add : Var.t -> bool) = + (* TODO handle maps ? *) + let open Expr.AbstractExpr in + let open Expr.BasilExpr in + Expr.BasilExpr.rewrite ~rw_fun:(function + | UnaryExpr { attrib; op = `Gamma; arg } -> + replace [%here] (gamma_expr ~check_names add arg) + | _ -> Keep) + in + + let update_lhs ?(check_names = false) add_cur add_target proc m = + StringMap.fold + (fun s v m -> + if add_cur v && add_target s then ( + if check_names then check_var v; + let gv = gamma_of v in + add_decl proc gv; + StringMap.add ("Gamma_" ^ s) gv m) + else m) + m m + in + + let update_args ?(check_names = false) add_cur add_target m = + StringMap.fold + (fun s e m -> + let m = StringMap.add s (update_expr ~check_names add_cur e) m in + if add_target s then + StringMap.add ("Gamma_" ^ s) (gamma_expr ~check_names add_cur e) m + else m) + m StringMap.empty + in + + let update_stmts ?(check_names = false) (add : ID.t -> Var.t -> bool) pid + (prog : Program.t) (b : (Var.t, Expr.BasilExpr.t) Block.t) = + let open Stmt in + let update_expr = update_expr ~check_names (add pid) in + let proc = Program.proc prog pid in + Block.map + ~phi:(fun a -> + List.flat_map + (fun (p : Var.t Block.phi) -> + if add pid p.lhs then ( + if check_names then check_var p.lhs; + let (g : Var.t Block.phi) = + { + lhs = gamma_of p.lhs; + rhs = List.map (fun (id, v) -> (id, gamma_of v)) p.rhs; + } + in + [ p; g ]) + else [ p ]) + a) + (function + | Instr_Assign { al; attrib } -> + let al = + al + |> List.flat_map (fun (l, e) -> + if add pid l then ( + if check_names then check_var l; + let gl = gamma_of l in + let ge = gamma_expr ~check_names (add pid) e in + add_decl proc gl; + [ (gl, ge); (l, e) ]) + else [ (l, e) ]) + in + Instr_Assign { attrib; al } + | Instr_Assert { body; attrib } -> + Instr_Assert { body = update_expr body; attrib } + | Instr_Assume { body; branch; attrib } -> + Instr_Assume { body = update_expr body; branch; attrib } + (* TODO Need atomic statement blocks to capture a "simultaneous op" from normal and gamma mem *) + | Instr_Load _ as s -> s + | Instr_Store _ as s -> s + | Instr_IntrinCall { lhs; name; args; attrib } -> + (* cursed *) + let to_sm lhs = + List.mapi (fun i v -> (Int.to_string i, v)) lhs + |> StringMap.of_list + in + let of_sm lhs k = + List.mapi (fun i _ -> StringMap.find (Int.to_string i) k) lhs + in + Instr_IntrinCall + { + lhs = + update_lhs ~check_names (add pid) + (fun _ -> true) + proc (to_sm lhs) + |> of_sm lhs; + name; + attrib; + args = + update_args ~check_names (add pid) + (fun _ -> true) + (to_sm args) + |> of_sm args; + } + | Instr_Call { lhs; procid; args; attrib } -> + let callee = Program.proc prog procid in + Instr_Call + { + lhs = + update_lhs ~check_names (add pid) + (fun s -> + add procid + (StringMap.find s (Procedure.formal_out_params callee))) + proc lhs; + procid; + attrib; + args = + update_args ~check_names (add pid) + (fun s -> + add procid + (StringMap.find s (Procedure.formal_in_params callee))) + args; + } + | Instr_IndirectCall { target; attrib } -> + Instr_IndirectCall { target = update_expr target; attrib }) + b + in + (* Update specs *) let update_expr = update_expr ~check_names (add (Procedure.id proc)) in let and_gamma v = [ gamma_of v; v ] in @@ -202,19 +216,31 @@ let transform_proc ?(check_names = false) (add : ID.t -> Var.t -> bool) prog in let proc = Procedure.set_specification proc spec in + let add_globals (p : Program.t) = + VarSet.to_iter !added |> Iter.fold (fun p v -> Program.add_var_decl p v) p + in + (* Update statements *) let blocks = Procedure.blocks_to_list proc in - List.fold_left - (fun proc b -> - match b with - | Procedure.Vert.Begin id, (b : (Var.t, Expr.BasilExpr.t) Block.t) -> - update_stmts ~check_names add (Procedure.id proc) prog b - |> Procedure.update_block proc id - | _ -> proc) - proc blocks + let proc = + List.fold_left + (fun proc b -> + match b with + | Procedure.Vert.Begin id, (b : (Var.t, Expr.BasilExpr.t) Block.t) -> + update_stmts ~check_names add (Procedure.id proc) prog b + |> Procedure.update_block proc id + | _ -> proc) + proc blocks + in + (add_globals prog, proc) let transform ?(check_names = false) (p : Program.t) = - let p = add_globals ~check_names (fun v -> true) p in - Program.map_procedures - (fun i proc -> transform_proc ~check_names (fun pid v -> true) p proc) - p + Program.procs p + |> Iter.fold + (fun prog (pid, proc) -> + let prog, proc = + transform_proc ~check_names (fun pid v -> true) p proc + in + let prog = Program.update_proc pid (fun _ -> Some proc) prog in + prog) + p diff --git a/lib/transforms/livevars.ml b/lib/transforms/livevars.ml index f5115c8e..7acaf93d 100644 --- a/lib/transforms/livevars.ml +++ b/lib/transforms/livevars.ml @@ -69,9 +69,10 @@ let print_live_vars_dot fmt p = let%expect_test _ = let open BasilExpr in - let v1 = Var.create "v1" (Types.bv 0x1) in - let v2 = Var.create "v2" (Types.bv 0x1) in - let v3 = Var.create "v3" (Types.bv 0x1) in + let g = Var.mk_gen () in + let v1 = g.with_name "v1" (Types.bv 0x1) in + let v2 = g.with_name "v2" (Types.bv 0x1) in + let v3 = g.with_name "v3" (Types.bv 0x1) in let e1 = BasilExpr.forall ~bound:[ v2 ] diff --git a/lib/transforms/may_read_uninit.ml b/lib/transforms/may_read_uninit.ml index 4363ed79..b8d49e1c 100644 --- a/lib/transforms/may_read_uninit.ml +++ b/lib/transforms/may_read_uninit.ml @@ -157,12 +157,10 @@ let%expect_test "fold_block" = in [%expect {| - Warn: global undeclared $stack assuming mutable unshared - Warn: global undeclared $mem assuming mutable unshared - ($stack->RU, R31_in->RU, R0_in->RU, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, R0_10->W, _->⊥) + (R31_in->RU, R0_in->RU, _->⊥) + (R31_in->RU, R0_in->RU, load45_1->W, _->⊥) + (R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥) + (R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥) + (R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, load46_1->W, _->⊥) + (R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, load46_1->W, R0_10->W, _->⊥) |}] diff --git a/lib/transforms/memory_encoding.ml b/lib/transforms/memory_encoding.ml index f3604956..518f41e6 100644 --- a/lib/transforms/memory_encoding.ml +++ b/lib/transforms/memory_encoding.ml @@ -6,24 +6,39 @@ let fresh = Bitvec.of_int 0 ~size:2 let live = Bitvec.of_int 1 ~size:2 let dead = Bitvec.of_int 2 ~size:2 -module Globals = struct +type function_body = Var.generator * Expr.BasilExpr.t + +module GlobalsF (N : sig + val global_ids : Var.generator +end) = +struct + open Var + let mem_encoding_typ_name = "memory_encoding" let mem_encoding_typ = Types.Variable mem_encoding_typ_name let mem_encoding = - Var.create "$mem_encoding" ~scope:Var.GlobalVar mem_encoding_typ + N.global_ids.with_name "mem_encoding" ~access:None mem_encoding_typ end -module Calls = struct +module Calls (N : sig + val global_ids : Var.generator +end) = +struct + open Var open BasilExpr + (* instantiating this first should put the ids in the right order *) + module Globals = GlobalsF (N) + (** [addr_is_heap args] checks if an address belongs to the heap. args(0) is the memory encoding object. args(1) is the address to check. *) let addr_is_heap ?attrib args = apply_fun ?attrib ~func: (rvar - (Var.create "$me_addr_is_heap" ~scope:Var.GlobalConst Types.Boolean)) + (N.global_ids.with_name "me_addr_is_heap" ~access:Var.Const + Types.Boolean)) args (** [alloc_base args] returns the base address of a supplied allocation id. @@ -32,7 +47,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_alloc_base" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_alloc_base" ~access:Var.Const (Types.Bitvector 64))) args @@ -43,7 +58,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_alloc_live" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_alloc_live" ~access:Var.Const (Types.Bitvector 2))) args @@ -53,7 +68,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_alloc_size" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_alloc_size" ~access:Var.Const (Types.Bitvector 64))) args @@ -63,7 +78,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_addr_alloc" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_addr_alloc" ~access:Var.Const (Types.Bitvector 64))) args @@ -73,7 +88,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_addr_offset" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_addr_offset" ~access:Var.Const (Types.Bitvector 64))) args @@ -84,7 +99,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_alloc_size_update" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_alloc_size_update" ~access:Var.Const Globals.mem_encoding_typ)) args @@ -95,7 +110,7 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_alloc_live_update" ~scope:Var.GlobalConst + (N.global_ids.with_name "me_alloc_live_update" ~access:Var.Const Globals.mem_encoding_typ)) args @@ -105,7 +120,8 @@ module Calls = struct let allocate ?attrib args = apply_fun ?attrib ~func: - (rvar (Var.create "$me_allocate" ~scope:Var.GlobalConst Types.Boolean)) + (rvar + (N.global_ids.with_name "me_allocate" ~access:Var.Const Types.Boolean)) args (** [can_alloc args] Returns whether an alloc, performed by [allocate], is @@ -115,7 +131,8 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_can_allocate" ~scope:Var.GlobalConst Types.Boolean)) + (N.global_ids.with_name "me_can_allocate" ~access:Var.Const + Types.Boolean)) args (** [init_encoding args] Returns if a memory encoding is initialized. args(0) @@ -124,7 +141,8 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_init_encoding" ~scope:Var.GlobalConst Types.Boolean)) + (N.global_ids.with_name "me_init_encoding" ~access:Var.Const + Types.Boolean)) args (** [valid_access args] Checks if an access is valid. args(0) is the memory @@ -134,57 +152,73 @@ module Calls = struct apply_fun ?attrib ~func: (rvar - (Var.create "$me_valid_access" ~scope:Var.GlobalConst Types.Boolean)) + (N.global_ids.with_name "me_valid_access" ~access:Var.Const + Types.Boolean)) args end module type MemoryEncoding = sig - module Locals : sig + val global_ids : Var.generator + + module Globals : sig + val mem_encoding_typ_name : string + val mem_encoding_typ : Types.t val mem_encoding : Var.t - val mem_encoding_out : Var.t - val alloc : Var.t - val addr : Var.t - val size : Var.t - val live : Var.t + end + + module Locals : sig + val mem_encoding : Var.generator -> Var.t + val mem_encoding_out : Var.generator -> Var.t + val alloc : Var.generator -> Var.t + val addr : Var.generator -> Var.t + val size : Var.generator -> Var.t + val live : Var.generator -> Var.t end val mem_encoding_type : Types.t - val can_allocate_body : Lang.Program.e - val alloc_size_body : Lang.Program.e - val alloc_base_body : Lang.Program.e - val addr_alloc_body : Lang.Program.e - val alloc_live_body : Lang.Program.e - val addr_offset_body : Lang.Program.e - val addr_is_heap_body : Lang.Program.e - val alloc_size_update_body : Lang.Program.e - val alloc_live_update_body : Lang.Program.e - val allocate_body : Lang.Program.e - val init_encoding_body : Lang.Program.e - val valid_access_body : Lang.Program.e + val can_allocate_body : function_body + val alloc_size_body : function_body + val alloc_base_body : function_body + val addr_alloc_body : function_body + val alloc_live_body : function_body + val addr_offset_body : function_body + val addr_is_heap_body : function_body + val alloc_size_update_body : function_body + val alloc_live_update_body : function_body + val allocate_body : function_body + val init_encoding_body : function_body + val valid_access_body : function_body end module MemoryEncoder (Encoding : MemoryEncoding) = struct - let add_decl ?(attrib = Attrib.empty) (p : Program.t) (name : string) - (bindings : Var.t list) (body : BasilExpr.t) = - let name = "$" ^ name in - Lang.Program.add_decl ~attrib p - (Lang.Program.Function - { - binding = - Bincaml_util.Common.Var.create name ~scope:GlobalConst - (Types.curry (List.map Var.typ bindings) - @@ Lang.Expr.BasilExpr.type_of body); - attrib; - definition : Lang.Program.func_type = - Function (Lang.Expr.BasilExpr.lambda ~bound:bindings body); - }) + module Globals = Encoding.Globals + + let decl_global ?(attrib = Attrib.empty) (p : Program.t) (name : string) + (bindings : (Var.generator -> Var.t) list) (body : function_body) = + let local_var_gen, body = body in + let bindings = List.map (fun f -> f local_var_gen) bindings in + let decl = + Lang.Program.Function + { + var_gen = local_var_gen; + binding = + (Program.var_generator p).with_name name ~access:Const + (Types.curry (List.map Var.typ bindings) + @@ Lang.Expr.BasilExpr.type_of body); + attrib; + definition : Lang.Program.func_type = + Function (Lang.Expr.BasilExpr.lambda ~bound:bindings body); + } + in + Lang.Program.add_decl p decl let add_mem_encoding p = + let gids : ID.generator = Program.global_ids p in let p = Lang.Program.add_decl p (Lang.Program.Type { - binding = Globals.mem_encoding_typ_name; + binding = gids.decl_or_get Globals.mem_encoding_typ_name; typ = Encoding.mem_encoding_type; }) in @@ -213,14 +247,14 @@ module MemoryEncoder (Encoding : MemoryEncoding) = struct ] let add_can_allocate p = - add_decl ~attrib p "me_can_allocate" + decl_global ~attrib p "me_can_allocate" [ Encoding.Locals.mem_encoding; Encoding.Locals.addr; Encoding.Locals.size; ] Encoding.can_allocate_body let add_allocate p = - add_decl ~attrib p "me_allocate" + decl_global ~attrib p "me_allocate" [ Encoding.Locals.mem_encoding; Encoding.Locals.mem_encoding_out; @@ -230,37 +264,37 @@ module MemoryEncoder (Encoding : MemoryEncoding) = struct Encoding.allocate_body let add_alloc_size p = - add_decl ~attrib p "me_alloc_size" + decl_global ~attrib p "me_alloc_size" [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc ] Encoding.alloc_size_body let add_addr_alloc p = - add_decl ~attrib p "me_addr_alloc" + decl_global ~attrib p "me_addr_alloc" [ Encoding.Locals.mem_encoding; Encoding.Locals.addr ] Encoding.addr_alloc_body let add_alloc_live p = - add_decl ~attrib p "me_alloc_live" + decl_global ~attrib p "me_alloc_live" [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc ] Encoding.alloc_live_body let add_addr_offset p = - add_decl ~attrib p "me_addr_offset" + decl_global ~attrib p "me_addr_offset" [ Encoding.Locals.mem_encoding; Encoding.Locals.addr ] Encoding.addr_offset_body let add_alloc_base p = - add_decl ~attrib p "me_alloc_base" + decl_global ~attrib p "me_alloc_base" [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc ] Encoding.alloc_base_body let add_addr_is_heap p = - add_decl ~attrib p "me_addr_is_heap" + decl_global ~attrib p "me_addr_is_heap" [ Encoding.Locals.mem_encoding; Encoding.Locals.addr ] Encoding.addr_is_heap_body let add_alloc_size_update p = - add_decl ~attrib p "me_alloc_size_update" + decl_global ~attrib p "me_alloc_size_update" [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc; @@ -269,7 +303,7 @@ module MemoryEncoder (Encoding : MemoryEncoding) = struct Encoding.alloc_size_update_body let add_alloc_live_update p = - add_decl ~attrib p "me_alloc_live_update" + decl_global ~attrib p "me_alloc_live_update" [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc; @@ -278,18 +312,18 @@ module MemoryEncoder (Encoding : MemoryEncoding) = struct Encoding.alloc_live_update_body let add_init_encoding p = - add_decl ~attrib p "me_init_encoding" + decl_global ~attrib p "me_init_encoding" [ Encoding.Locals.mem_encoding ] Encoding.init_encoding_body let add_valid_access_body p = - add_decl ~attrib p "me_valid_access" + decl_global ~attrib p "me_valid_access" [ Encoding.Locals.mem_encoding; Encoding.Locals.addr; Encoding.Locals.size; ] Encoding.valid_access_body - let add_decls (p : Lang.Program.t) = + let decl_globals (p : Lang.Program.t) = List.fold_left (fun acc f -> f acc) p @@ -309,11 +343,21 @@ module MemoryEncoder (Encoding : MemoryEncoding) = struct add_valid_access_body; ] - let transform (p : Lang.Program.t) = add_decls p + let transform (p : Lang.Program.t) = decl_globals p +end + +(** Access to variable allocation functions for getting the handle for global + functions and local variables for the procedure we are encoding *) +module type IDAllocs = sig + val global_ids : Var.generator end -module FlatMemory : MemoryEncoding = struct +module FlatMemory (M : IDAllocs) : MemoryEncoding = struct open BasilExpr + module Calls = Calls (M) + module Globals = Calls.Globals + + let global_ids = M.global_ids let mem_encoding_type : Types.t = Types.Sort @@ -345,210 +389,284 @@ module FlatMemory : MemoryEncoding = struct ] ) module Locals = struct - let mem_encoding : Var.t = - Var.create "mem_encoding" ~scope:Var.LocalVar mem_encoding_type + open Var + + let mem_encoding l : Var.t = l.with_name "mem_encoding" mem_encoding_type - let mem_encoding_out : Var.t = - Var.create "mem_encoding_out" ~scope:Var.LocalVar mem_encoding_type + let mem_encoding_out l : Var.t = + l.with_name "mem_encoding_out" mem_encoding_type - let alloc = Var.create "alloc" ~scope:Var.LocalVar Types.Integer - let addr = Var.create "addr" ~scope:Var.LocalVar (Types.Bitvector 64) - let size = Var.create "size" ~scope:Var.LocalVar (Types.Bitvector 64) - let live = Var.create "live" ~scope:Var.LocalVar (Types.Bitvector 2) + let alloc l = l.with_name "alloc" Types.Integer + let addr l = l.with_name "addr" (Types.Bitvector 64) + let size l = l.with_name "size" (Types.Bitvector 64) + let live l = l.with_name "live" (Types.Bitvector 2) let alloc_live_access_h me = unexp ~op:(`ReadField "alloc_live") (rvar me) - let alloc_live_access = alloc_live_access_h mem_encoding + let alloc_live_access l = alloc_live_access_h (mem_encoding l) let alloc_size_access_h me = unexp ~op:(`ReadField "alloc_size") (rvar me) - let alloc_size_access = alloc_size_access_h mem_encoding + let alloc_size_access l = alloc_size_access_h (mem_encoding l) - let alloc_base_access = - unexp ~op:(`ReadField "alloc_base") (rvar mem_encoding) + let alloc_base_access l = + unexp ~op:(`ReadField "alloc_base") (rvar @@ mem_encoding l) - let addr_is_heap_access = - unexp ~op:(`ReadField "addr_is_heap") (rvar mem_encoding) + let addr_is_heap_access l = + unexp ~op:(`ReadField "addr_is_heap") (rvar @@ mem_encoding l) - let addr_alloc_access = - unexp ~op:(`ReadField "addr_alloc") (rvar mem_encoding) + let addr_alloc_access l = + unexp ~op:(`ReadField "addr_alloc") (rvar @@ mem_encoding l) - let addr_offset_access = - unexp ~op:(`ReadField "addr_offset") (rvar mem_encoding) + let addr_offset_access l = + unexp ~op:(`ReadField "addr_offset") (rvar @@ mem_encoding l) end let trigger e = [ [ e ] ] - let can_allocate_body : Lang.Program.e = boolconst true - - let alloc_size_body : Lang.Program.e = - binexp ~op:`MapAccess Locals.alloc_size_access (rvar Locals.alloc) - - let alloc_base_body : Lang.Program.e = - binexp ~op:`MapAccess Locals.alloc_base_access (rvar Locals.alloc) - - let addr_alloc_body : Lang.Program.e = - binexp ~op:`MapAccess Locals.addr_alloc_access (rvar Locals.addr) - - let alloc_live_body : Lang.Program.e = - binexp ~op:`MapAccess Locals.alloc_live_access (rvar Locals.alloc) - - let addr_offset_body : Lang.Program.e = - binexp ~op:`MapAccess Locals.addr_offset_access (rvar Locals.addr) + let can_allocate_body : function_body = (Var.mk_gen (), boolconst true) + + let alloc_size_body : function_body = + let l = Var.mk_gen () in + ( l, + binexp ~op:`MapAccess (Locals.alloc_size_access l) (rvar @@ Locals.alloc l) + ) + + let alloc_base_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:`MapAccess (Locals.alloc_base_access l) (rvar @@ Locals.alloc l) + in + (l, b) - let addr_is_heap_body : Lang.Program.e = - binexp ~op:`MapAccess Locals.addr_is_heap_access (rvar Locals.addr) + let addr_alloc_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:`MapAccess (Locals.addr_alloc_access l) (rvar @@ Locals.addr l) + in + (l, b) - let alloc_size_update_body : Lang.Program.e = - binexp ~op:(`WriteField "alloc_size") (rvar Locals.mem_encoding) - (applyintrin ~op:`MapUpdate - [ Locals.alloc_size_access; rvar Locals.alloc; rvar Locals.size ]) + let alloc_live_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:`MapAccess (Locals.alloc_live_access l) (rvar @@ Locals.alloc l) + in + (l, b) - let alloc_live_update_body : Lang.Program.e = - binexp ~op:(`WriteField "alloc_live") (rvar Locals.mem_encoding) - (applyintrin ~op:`MapUpdate - [ Locals.alloc_live_access; rvar Locals.alloc; rvar Locals.live ]) + let addr_offset_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:`MapAccess (Locals.addr_offset_access l) (rvar @@ Locals.addr l) + in + (l, b) + + let addr_is_heap_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:`MapAccess + (Locals.addr_is_heap_access l) + (rvar @@ Locals.addr l) + in + (l, b) + + let alloc_size_update_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:(`WriteField "alloc_size") + (rvar @@ Locals.mem_encoding l) + (applyintrin ~op:`MapUpdate + [ + Locals.alloc_size_access l; + rvar @@ Locals.alloc l; + rvar @@ Locals.size l; + ]) + in + (l, b) + + let alloc_live_update_body : function_body = + let l = Var.mk_gen () in + let b = + binexp ~op:(`WriteField "alloc_live") + (rvar @@ Locals.mem_encoding l) + (applyintrin ~op:`MapUpdate + [ + Locals.alloc_live_access l; + rvar @@ Locals.alloc l; + rvar @@ Locals.live l; + ]) + in + (l, b) - let allocate_body : Lang.Program.e = - let i = Var.create "i" ~scope:Var.LocalVar (Types.Bitvector 64) in + let allocate_body : function_body = + let l = Var.mk_gen () in + let i = l.with_name "i" (Types.Bitvector 64) in let in_bounds = applyintrin ~op:`AND [ - binexp ~op:`BVULE (rvar Locals.addr) (rvar i); + binexp ~op:`BVULE (rvar @@ Locals.addr l) (rvar i); binexp ~op:`BVULT (rvar i) - (binexp ~op:`BVADD (rvar Locals.addr) (rvar Locals.size)); + (binexp ~op:`BVADD (rvar @@ Locals.addr l) (rvar @@ Locals.size l)); ] in (* alloc for i and addr are the same *) - let same_alloc = + let same_alloc l = binexp ~op:`EQ - (Calls.addr_alloc [ rvar Locals.mem_encoding_out; rvar i ]) - (Calls.addr_alloc [ rvar Locals.mem_encoding_out; rvar Locals.addr ]) + (Calls.addr_alloc [ rvar @@ Locals.mem_encoding_out l; rvar i ]) + (Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar @@ Locals.addr l ]) in - applyintrin ~op:`AND - [ - (* update addr_alloc for all pointers in the range [addr, addr+size) + let b = + applyintrin ~op:`AND + [ + (* update addr_alloc for all pointers in the range [addr, addr+size) to point to the old allocation counter. *) - forall ~bound:[ i ] - ~triggers: - (trigger - (Calls.addr_alloc [ rvar Locals.mem_encoding_out; rvar i ])) - (binexp ~op:`IMPLIES in_bounds - (binexp ~op:`EQ - (Calls.addr_alloc [ rvar Locals.mem_encoding_out; rvar i ]) - (unexp ~op:(`ReadField "alloc_counter") - (rvar Locals.mem_encoding)))); - (* Preserve all other addr_alloc entries. *) - forall ~bound:[ i ] - ~triggers: - (trigger - (Calls.addr_alloc [ rvar Locals.mem_encoding_out; rvar i ])) - (binexp ~op:`IMPLIES - (unexp ~op:`BoolNOT in_bounds) - (binexp ~op:`EQ - (Calls.addr_alloc [ rvar Locals.mem_encoding_out; rvar i ]) - (Calls.addr_alloc [ rvar Locals.mem_encoding; rvar i ]))); - (* Update offsets for all pointers in allocation. *) - forall ~bound:[ i ] - ~triggers: - (trigger - (Calls.addr_offset [ rvar Locals.mem_encoding_out; rvar i ])) - (binexp ~op:`IMPLIES same_alloc - (binexp ~op:`EQ - (Calls.addr_offset [ rvar Locals.mem_encoding_out; rvar i ]) - (binexp ~op:`BVSUB (rvar i) (rvar Locals.addr)))); - (* Preserve all other addr offsets. *) - forall ~bound:[ i ] - ~triggers: - (trigger - (Calls.addr_offset [ rvar Locals.mem_encoding_out; rvar i ])) - (binexp ~op:`IMPLIES - (unexp ~op:`BoolNOT same_alloc) - (binexp ~op:`EQ - (Calls.addr_offset [ rvar Locals.mem_encoding_out; rvar i ]) - (Calls.addr_offset [ rvar Locals.mem_encoding; rvar i ]))); - (* Update the size of the allocation. *) - binexp ~op:`EQ - (Locals.alloc_size_access_h Locals.mem_encoding_out) - (applyintrin ~op:`MapUpdate - [ - Locals.alloc_size_access; - Calls.addr_alloc - [ rvar Locals.mem_encoding_out; rvar Locals.addr ]; - rvar Locals.size; - ]); - (* Update the liveness of the allocation. *) - binexp ~op:`EQ - (Locals.alloc_live_access_h Locals.mem_encoding_out) - (applyintrin ~op:`MapUpdate - [ - Locals.alloc_live_access; - Calls.addr_alloc - [ rvar Locals.mem_encoding_out; rvar Locals.addr ]; - bvconst live; - ]); - (* The allocation at addr was fresh. *) - binexp ~op:`EQ - (Calls.alloc_live - [ - rvar Locals.mem_encoding; - Calls.addr_alloc - [ rvar Locals.mem_encoding_out; rvar Locals.addr ]; - ]) - (bvconst fresh); - (* The allocation at addr was/is on the heap. *) - Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar Locals.addr ]; - (* addr_is_heap is unchanged. *) - binexp ~op:`EQ - (unexp ~op:(`ReadField "addr_is_heap") (rvar Locals.mem_encoding)) - (unexp ~op:(`ReadField "addr_is_heap") (rvar Locals.mem_encoding_out)); - ] - - let init_encoding_body : Lang.Program.e = - let o = Var.create "o" ~scope:Var.LocalVar Types.Integer in - let i = Var.create "i" ~scope:Var.LocalVar (Types.Bitvector 64) in - applyintrin ~op:`AND - [ - (* allocation counter starts at 0 *) - binexp ~op:`EQ - (unexp ~op:(`ReadField "alloc_counter") (rvar Locals.mem_encoding)) - (intconst @@ Z.of_int 0); - (* all objects are initially fresh *) - forall ~bound:[ o ] - ~triggers: - (trigger (Calls.alloc_live [ rvar Locals.mem_encoding; rvar o ])) - (binexp ~op:`EQ - (Calls.alloc_live [ rvar Locals.mem_encoding; rvar o ]) - (bvconst fresh)); - (* stack/heap separation, TODO: compute this smartly *) - forall ~bound:[ i ] - ~triggers: - (trigger (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])) - (binexp ~op:`EQ - (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ]) - (unexp ~op:`BoolNOT - @@ binexp ~op:`BVULE (rvar i) (bv_of_int ~size:64 100000000))); - ] - - let valid_access_body : Lang.Program.e = - let alloc = - Calls.addr_alloc [ rvar Locals.mem_encoding; rvar Locals.addr ] + forall ~bound:[ i ] + ~triggers: + (trigger + (Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar i ])) + (binexp ~op:`IMPLIES in_bounds + (binexp ~op:`EQ + (Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar i ]) + (unexp ~op:(`ReadField "alloc_counter") + (rvar @@ Locals.mem_encoding l)))); + (* Preserve all other addr_alloc entries. *) + forall ~bound:[ i ] + ~triggers: + (trigger + (Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar i ])) + (binexp ~op:`IMPLIES + (unexp ~op:`BoolNOT in_bounds) + (binexp ~op:`EQ + (Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar i ]) + (Calls.addr_alloc [ rvar @@ Locals.mem_encoding l; rvar i ]))); + (* Update offsets for all pointers in allocation. *) + forall ~bound:[ i ] + ~triggers: + (trigger + (Calls.addr_offset + [ rvar @@ Locals.mem_encoding_out l; rvar i ])) + (binexp ~op:`IMPLIES (same_alloc l) + (binexp ~op:`EQ + (Calls.addr_offset + [ rvar @@ Locals.mem_encoding_out l; rvar i ]) + (binexp ~op:`BVSUB (rvar i) (rvar @@ Locals.addr l)))); + (* Preserve all other addr offsets. *) + forall ~bound:[ i ] + ~triggers: + (trigger + (Calls.addr_offset + [ rvar @@ Locals.mem_encoding_out l; rvar i ])) + (binexp ~op:`IMPLIES + (unexp ~op:`BoolNOT (same_alloc l)) + (binexp ~op:`EQ + (Calls.addr_offset + [ rvar @@ Locals.mem_encoding_out l; rvar i ]) + (Calls.addr_offset [ rvar @@ Locals.mem_encoding l; rvar i ]))); + (* Update the size of the allocation. *) + binexp ~op:`EQ + (Locals.alloc_size_access_h (Locals.mem_encoding_out l)) + (applyintrin ~op:`MapUpdate + [ + Locals.alloc_size_access l; + Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar @@ Locals.addr l ]; + rvar (Locals.size l); + ]); + (* Update the liveness of the allocation. *) + binexp ~op:`EQ + (Locals.alloc_live_access_h @@ Locals.mem_encoding_out l) + (applyintrin ~op:`MapUpdate + [ + Locals.alloc_live_access l; + Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar @@ Locals.addr l ]; + bvconst live; + ]); + (* The allocation at addr was fresh. *) + binexp ~op:`EQ + (Calls.alloc_live + [ + rvar @@ Locals.mem_encoding l; + Calls.addr_alloc + [ rvar @@ Locals.mem_encoding_out l; rvar @@ Locals.addr l ]; + ]) + (bvconst fresh); + (* The allocation at addr was/is on the heap. *) + Calls.addr_is_heap + [ rvar @@ Locals.mem_encoding l; rvar @@ Locals.addr l ]; + (* addr_is_heap is unchanged. *) + binexp ~op:`EQ + (unexp ~op:(`ReadField "addr_is_heap") + (rvar @@ Locals.mem_encoding l)) + (unexp ~op:(`ReadField "addr_is_heap") + (rvar @@ Locals.mem_encoding_out l)); + ] + in + (l, b) + + let init_encoding_body : function_body = + let l = Var.mk_gen () in + let o = l.with_name "o" Types.Integer in + let i = l.with_name "i" (Types.Bitvector 64) in + let b = + begin + applyintrin ~op:`AND + [ + (* allocation counter starts at 0 *) + binexp ~op:`EQ + (unexp ~op:(`ReadField "alloc_counter") + (rvar @@ Locals.mem_encoding l)) + (intconst @@ Z.of_int 0); + (* all objects are initially fresh *) + forall ~bound:[ o ] + ~triggers: + (trigger + (Calls.alloc_live [ rvar @@ Locals.mem_encoding l; rvar o ])) + (binexp ~op:`EQ + (Calls.alloc_live [ rvar @@ Locals.mem_encoding l; rvar o ]) + (bvconst fresh)); + (* stack/heap separation, TODO: compute this smartly *) + forall ~bound:[ i ] + ~triggers: + (trigger + (Calls.addr_is_heap + [ rvar @@ Locals.mem_encoding l; rvar i ])) + (binexp ~op:`EQ + (Calls.addr_is_heap [ rvar @@ Locals.mem_encoding l; rvar i ]) + (unexp ~op:`BoolNOT + @@ binexp ~op:`BVULE (rvar i) (bv_of_int ~size:64 100000000))); + ] + end in - let offset = - Calls.addr_offset [ rvar Locals.mem_encoding; rvar Locals.addr ] + (l, b) + + let valid_access_body : function_body = + let l = Var.mk_gen () in + let me = rvar (Locals.mem_encoding l) in + let addr = rvar (Locals.addr l) in + let alloc = Calls.addr_alloc [ me; addr ] in + let offset = Calls.addr_offset [ me; addr ] in + let b = + binexp ~op:`IMPLIES + (Calls.addr_is_heap [ me; addr ]) + (applyintrin ~op:`AND + [ + binexp ~op:`EQ (Calls.alloc_live [ me; alloc ]) (bvconst live); + binexp ~op:`BVULE (bv_of_int 0 ~size:64) offset; + binexp ~op:`BVULE + (binexp ~op:`BVADD (rvar @@ Locals.size l) offset) + (Calls.alloc_size [ me; alloc ]); + ]) in - binexp ~op:`IMPLIES - (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar Locals.addr ]) - (applyintrin ~op:`AND - [ - binexp ~op:`EQ - (Calls.alloc_live [ rvar Locals.mem_encoding; alloc ]) - (bvconst live); - binexp ~op:`BVULE (bv_of_int 0 ~size:64) offset; - binexp ~op:`BVULE - (binexp ~op:`BVADD (rvar Locals.size) offset) - (Calls.alloc_size [ rvar Locals.mem_encoding; alloc ]); - ]) + (l, b) end -module SplitMemory : MemoryEncoding = struct +module SplitMemory (M : IDAllocs) : MemoryEncoding = struct open BasilExpr + module Calls = Calls (M) + module Globals = Calls.Globals + let v = M.global_ids + let global_ids = v let offset_size = 32 let addr_size = 64 - offset_size @@ -568,174 +686,223 @@ module SplitMemory : MemoryEncoding = struct ] ) module Locals = struct - let mem_encoding = - Var.create "mem_encoding" ~scope:Var.LocalVar mem_encoding_type + open Var - let mem_encoding_out : Var.t = - Var.create "mem_encoding_out" ~scope:Var.LocalVar mem_encoding_type + let mem_encoding l = l.with_name "mem_encoding" mem_encoding_type - let alloc = Var.create "alloc" ~scope:Var.LocalVar (Types.Bitvector 64) - let addr = Var.create "addr" ~scope:Var.LocalVar (Types.Bitvector 64) - let size = Var.create "size" ~scope:Var.LocalVar (Types.Bitvector 64) - let live = Var.create "live" ~scope:Var.LocalVar (Types.Bitvector 2) + let mem_encoding_out l : Var.t = + l.with_name "mem_encoding_out" mem_encoding_type - let alloc_live_access = - unexp ~op:(`ReadField "alloc_live") (rvar mem_encoding) + let alloc l = l.with_name "alloc" (Types.Bitvector 64) + let addr l = l.with_name "addr" (Types.Bitvector 64) + let size l = l.with_name "size" (Types.Bitvector 64) + let live l = l.with_name "live" (Types.Bitvector 2) - let alloc_size_access = - unexp ~op:(`ReadField "alloc_size") (rvar mem_encoding) + let alloc_live_access l = + unexp ~op:(`ReadField "alloc_live") (rvar @@ mem_encoding l) - let addr_is_heap_access = - unexp ~op:(`ReadField "addr_is_heap") (rvar mem_encoding) - end - - let can_allocate_body = - applyintrin ~op:`AND - [ - (* Addr must be on the heap: *) - Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar Locals.addr ]; - (* Address is a base address *) - binexp ~op:`EQ - (Calls.alloc_base [ rvar Locals.mem_encoding; rvar Locals.addr ]) - (rvar Locals.addr); - (* Adddress is fresh *) - binexp ~op:`EQ - (Calls.alloc_live - [ - rvar Locals.mem_encoding; - Calls.addr_alloc [ rvar Locals.mem_encoding; rvar Locals.addr ]; - ]) - (bvconst fresh); - (* Size is within bounds *) - binexp ~op:`BVULE (rvar Locals.size) - (bv_of_int ~size:64 (Int.pow 2 offset_size - 1)); - binexp ~op:`BVULT (bv_of_int ~size:64 0) (rvar Locals.size); - ] + let alloc_size_access l = + unexp ~op:(`ReadField "alloc_size") (rvar @@ mem_encoding l) - let alloc_size_body = - binexp ~op:`MapAccess Locals.alloc_size_access (rvar Locals.alloc) - - let alloc_base_body = - binexp ~op:`BVAND (rvar Locals.alloc) - (bv_of_int ~size:64 (Int.lnot (Int.pow 2 addr_size - 1))) + let addr_is_heap_access l = + unexp ~op:(`ReadField "addr_is_heap") (rvar @@ mem_encoding l) + end - let addr_alloc_body = rvar Locals.addr + let can_allocate_body : function_body = + let v = Var.mk_gen () in + ( v, + applyintrin ~op:`AND + [ + (* Addr must be on the heap: *) + Calls.addr_is_heap + [ rvar @@ Locals.mem_encoding v; rvar @@ Locals.addr v ]; + (* Address is a base address *) + binexp ~op:`EQ + (Calls.alloc_base + [ rvar @@ Locals.mem_encoding v; rvar @@ Locals.addr v ]) + (rvar @@ Locals.addr v); + (* Adddress is fresh *) + binexp ~op:`EQ + (Calls.alloc_live + [ + rvar @@ Locals.mem_encoding v; + Calls.addr_alloc + [ rvar @@ Locals.mem_encoding v; rvar @@ Locals.addr v ]; + ]) + (bvconst fresh); + (* Size is within bounds *) + binexp ~op:`BVULE + (rvar @@ Locals.size v) + (bv_of_int ~size:64 (Int.pow 2 offset_size - 1)); + binexp ~op:`BVULT (bv_of_int ~size:64 0) (rvar @@ Locals.size v); + ] ) - let alloc_live_body = - binexp ~op:`MapAccess Locals.alloc_live_access (rvar Locals.alloc) + let alloc_size_body : function_body = + let v = Var.mk_gen () in + ( v, + binexp ~op:`MapAccess (Locals.alloc_size_access v) (rvar @@ Locals.alloc v) + ) + + let alloc_base_body : function_body = + let v = Var.mk_gen () in + ( v, + binexp ~op:`BVAND + (rvar (Locals.alloc v)) + (bv_of_int ~size:64 (Int.lnot (Int.pow 2 addr_size - 1))) ) + + let addr_alloc_body : function_body = + let v = Var.mk_gen () in + (v, rvar (Locals.addr v)) + + let alloc_live_body : function_body = + let v = Var.mk_gen () in + ( v, + binexp ~op:`MapAccess (Locals.alloc_live_access v) (rvar @@ Locals.alloc v) + ) let addr_offset_body = - binexp ~op:`BVAND (rvar Locals.addr) - (bv_of_int ~size:64 (Int.pow 2 offset_size - 1)) + let l = Var.mk_gen () in + let b = + binexp ~op:`BVAND + (rvar @@ Locals.addr l) + (bv_of_int ~size:64 (Int.pow 2 offset_size - 1)) + in + (l, b) let addr_is_heap_body = - binexp ~op:`MapAccess Locals.addr_is_heap_access (rvar Locals.addr) + let l = Var.mk_gen () in + ( l, + binexp ~op:`MapAccess + (Locals.addr_is_heap_access l) + (rvar @@ Locals.addr l) ) let alloc_size_update_body = - binexp ~op:(`WriteField "alloc_size") (rvar Locals.mem_encoding) - (applyintrin ~op:`MapUpdate - [ Locals.alloc_size_access; rvar Locals.alloc; rvar Locals.size ]) + let l = Var.mk_gen () in + let b = + binexp ~op:(`WriteField "alloc_size") + (rvar @@ Locals.mem_encoding l) + (applyintrin ~op:`MapUpdate + [ + Locals.alloc_size_access l; + rvar @@ Locals.alloc l; + rvar @@ Locals.size l; + ]) + in + (l, b) let alloc_live_update_body = - binexp ~op:(`WriteField "alloc_live") (rvar Locals.mem_encoding) - (applyintrin ~op:`MapUpdate - [ Locals.alloc_live_access; rvar Locals.alloc; rvar Locals.live ]) + let l = Var.mk_gen () in + let b = + binexp ~op:(`WriteField "alloc_live") + (rvar @@ Locals.mem_encoding l) + (applyintrin ~op:`MapUpdate + [ + Locals.alloc_live_access l; + rvar (Locals.alloc l); + rvar (Locals.live l); + ]) + in + (l, b) let allocate_body = + let l = Var.mk_gen () in let alloc = - Calls.addr_alloc [ rvar Locals.mem_encoding; rvar Locals.addr ] + Calls.addr_alloc [ rvar (Locals.mem_encoding l); rvar (Locals.addr l) ] in - let updated = Calls.alloc_size_update [ Calls.alloc_live_update - [ rvar Locals.mem_encoding; alloc; bvconst live ]; + [ rvar (Locals.mem_encoding l); alloc; bvconst live ]; alloc; - rvar Locals.size; + rvar (Locals.size l); ] in - - binexp ~op:`EQ updated (rvar Locals.mem_encoding_out) + (l, binexp ~op:`EQ updated (rvar @@ Locals.mem_encoding_out l)) let init_encoding_body = - let i = Var.create "i" ~scope:Var.LocalVar (Types.Bitvector 64) in + let l = Var.mk_gen () in + let i = l.with_name "i" (Types.Bitvector 64) in + let mem_enc = rvar (Locals.mem_encoding l) in let trigger e = [ [ e ] ] in - applyintrin ~op:`AND - [ - (* Ensure that all heap addresses are bigger than the largest global address *) - forall - ~triggers: - (trigger (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])) - ~bound:[ i ] - (binexp ~op:`EQ - (binexp ~op:`BVULT - (* TODO compute this value somehow *) - (bv_of_int 100000000 ~size:64) - (rvar i)) - (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])); - (* Heap addresses are initially fresh *) - forall - ~triggers: - (trigger (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ])) - ~bound:[ i ] - (binexp ~op:`IMPLIES - (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ]) - (binexp ~op:`EQ - (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ]) - (bvconst fresh))); - (* Non heap addresses are dead *) - forall - ~triggers: - (trigger (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ])) - ~bound:[ i ] - (binexp ~op:`IMPLIES - (boolnot (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])) - (binexp ~op:`EQ - (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ]) - (bvconst dead))); - ] + let b = + applyintrin ~op:`AND + [ + (* Ensure that all heap addresses are bigger than the largest global address *) + forall + ~triggers:(trigger (Calls.addr_is_heap [ mem_enc; rvar i ])) + ~bound:[ i ] + (binexp ~op:`EQ + (binexp ~op:`BVULT + (* TODO compute this value somehow *) + (bv_of_int 100000000 ~size:64) + (rvar i)) + (Calls.addr_is_heap [ mem_enc; rvar i ])); + (* Heap addresses are initially fresh *) + forall + ~triggers:(trigger (Calls.alloc_live [ mem_enc; rvar i ])) + ~bound:[ i ] + (binexp ~op:`IMPLIES + (Calls.addr_is_heap [ mem_enc; rvar i ]) + (binexp ~op:`EQ + (Calls.alloc_live [ mem_enc; rvar i ]) + (bvconst fresh))); + (* Non heap addresses are dead *) + forall + ~triggers:(trigger (Calls.alloc_live [ mem_enc; rvar i ])) + ~bound:[ i ] + (binexp ~op:`IMPLIES + (boolnot (Calls.addr_is_heap [ mem_enc; rvar i ])) + (binexp ~op:`EQ + (Calls.alloc_live [ mem_enc; rvar i ]) + (bvconst dead))); + ] + in + (l, b) let valid_access_body = - binexp ~op:`IMPLIES - (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar Locals.addr ]) - (applyintrin ~op:`AND - [ - binexp ~op:`EQ - (Calls.alloc_live - [ - rvar Locals.mem_encoding; - Calls.alloc_base - [ - rvar Locals.mem_encoding; - Calls.addr_alloc - [ rvar Locals.mem_encoding; rvar Locals.addr ]; - ]; - ]) - (bvconst live); - binexp ~op:`BVULE - (Calls.addr_offset - [ - rvar Locals.mem_encoding; - binexp ~op:`BVADD (rvar Locals.addr) (rvar Locals.size); - ]) - (Calls.alloc_size - [ - rvar Locals.mem_encoding; - Calls.alloc_base - [ - rvar Locals.mem_encoding; - Calls.addr_alloc - [ rvar Locals.mem_encoding; rvar Locals.addr ]; - ]; - ]); - ]) + let l = Var.mk_gen () in + let mem_enc = rvar (Locals.mem_encoding l) in + let addr = rvar (Locals.addr l) in + let b = + binexp ~op:`IMPLIES + (Calls.addr_is_heap [ mem_enc; addr ]) + (applyintrin ~op:`AND + [ + binexp ~op:`EQ + (Calls.alloc_live + [ + mem_enc; + Calls.alloc_base + [ mem_enc; Calls.addr_alloc [ mem_enc; addr ] ]; + ]) + (bvconst live); + binexp ~op:`BVULE + (Calls.addr_offset + [ mem_enc; binexp ~op:`BVADD addr (rvar @@ Locals.size l) ]) + (Calls.alloc_size + [ + mem_enc; + Calls.alloc_base + [ mem_enc; Calls.addr_alloc [ mem_enc; addr ] ]; + ]); + ]) + in + (l, b) end let split_transform (p : Program.t) = - let module E = MemoryEncoder (SplitMemory) in - E.transform p + let module I : IDAllocs = struct + let global_ids = Program.var_generator p + end + in + let module E = MemoryEncoder (SplitMemory (I)) in + E.transform p |> fun prog -> Spec_modifies.set_modsets prog let flat_transform (p : Program.t) = - let module E = MemoryEncoder (FlatMemory) in - E.transform p + let module I : IDAllocs = struct + let global_ids = Program.var_generator p + end + in + let module E = MemoryEncoder (FlatMemory (I)) in + E.transform p |> fun prog -> Spec_modifies.set_modsets prog diff --git a/lib/transforms/memory_specification.ml b/lib/transforms/memory_specification.ml index 42c84ebd..aef2c7a4 100644 --- a/lib/transforms/memory_specification.ml +++ b/lib/transforms/memory_specification.ml @@ -3,178 +3,181 @@ open Lang.Common open Lang.Expr open Memory_encoding -let make_msg_attrib msg = - StringMap.of_list - [ (".boogie", `Assoc (StringMap.of_list [ (".msg", `String msg) ])) ] +module T (I : sig + val global_ids : Var.generator +end) = +struct + module Calls = Calls (I) + module Globals = Calls.Globals -let old e = BasilExpr.unexp ~op:`Old e -let i = Var.create ~scope:Var.LocalConst "i" (Types.Bitvector 64) + let make_msg_attrib msg = + StringMap.of_list + [ (".boogie", `Assoc (StringMap.of_list [ (".msg", `String msg) ])) ] -let r n = - BasilExpr.rvar - (Var.create ~scope:Var.GlobalVar (Printf.sprintf "$R%d" n) - (Types.Bitvector 64)) + let old e = BasilExpr.unexp ~op:`Old e -let r_in n = - BasilExpr.rvar - (Var.create ~scope:Var.LocalVar - (Printf.sprintf "R%d_in" n) - (Types.Bitvector 64)) + open Var -let r_out n = - BasilExpr.rvar - (Var.create ~scope:Var.LocalVar - (Printf.sprintf "R%d_out" n) - (Types.Bitvector 64)) + let r p n = + BasilExpr.rvar (p.with_name (Printf.sprintf "$R%d" n) (Types.Bitvector 64)) -let transform_main p = - (* TODO: Specify Gammas Oneday *) - let spec = Procedure.specification p in - Procedure.set_specification p - { - spec with - requires = - spec.requires - (* Require memory is initialized. *) - @ [ Calls.init_encoding [ BasilExpr.rvar Globals.mem_encoding ] ]; - (* Ensure there are no memory leaks. *) - ensures = - spec.ensures - @ [ - BasilExpr.forall - ~attrib:(make_msg_attrib "Memory Error: Memory Leak") - ~bound:[ i ] - @@ BasilExpr.binexp ~op:`IMPLIES - (Calls.addr_is_heap - [ BasilExpr.rvar Globals.mem_encoding; BasilExpr.rvar i ]) - (BasilExpr.binexp ~op:`NEQ - (Calls.alloc_live - [ - BasilExpr.rvar Globals.mem_encoding; - Calls.addr_alloc - [ - BasilExpr.rvar Globals.mem_encoding; - BasilExpr.rvar i; - ]; - ]) - (BasilExpr.bvconst live)); - ]; - modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; - captures_globs = spec.captures_globs @ [ Globals.mem_encoding ]; - } + let r_in p n = + BasilExpr.rvar + (p.with_name (Printf.sprintf "R%d_in" n) (Types.Bitvector 64)) -let transform_malloc p = - (* TODO: Specify Gammas Oneday *) - let spec = Procedure.specification p in - let open BasilExpr in - Procedure.set_specification p - { - spec with - ensures = - spec.ensures - @ [ - (* Can allocate at new r0 with size old r0 *) - Calls.can_alloc - [ old @@ rvar Globals.mem_encoding; r_out 0; r_in 0 ]; - (* Offset of return address r0 is 0 *) - binexp ~op:`EQ - (Calls.addr_offset [ rvar Globals.mem_encoding; r_out 0 ]) - (bv_of_int ~size:64 0); - (* Base of associated allocation is r(0) *) - binexp ~op:`EQ - (Calls.alloc_base - [ - rvar Globals.mem_encoding; - Calls.addr_alloc [ rvar Globals.mem_encoding; r_out 0 ]; - ]) - (r_out 0); - (* Update the memory encoding: *) - Calls.allocate - [ - old @@ rvar Globals.mem_encoding; - rvar Globals.mem_encoding; - r_out 0; - r_in 0; - ]; - ]; - modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; - captures_globs = spec.captures_globs @ [ Globals.mem_encoding ]; - } + let r_out p n = + BasilExpr.rvar + (p.with_name (Printf.sprintf "R%d_out" n) (Types.Bitvector 64)) -let transform_free p = - (* TODO: Specify Gammas Oneday *) - let spec = Procedure.specification p in - let open BasilExpr in - Procedure.set_specification p - { - spec with - requires = - spec.requires - @ [ - (* Only free heap values *) - Calls.addr_is_heap - ~attrib: - (make_msg_attrib "Memory Error: Invalid Free (non heap object)") - [ rvar Globals.mem_encoding; r_in 0 ]; - (* Only free if offset is 0 *) - binexp - ~attrib: - (make_msg_attrib "Memory Error: Invalid Free (not base address)") - ~op:`EQ (bv_of_int ~size:64 0) - (Calls.addr_offset [ rvar Globals.mem_encoding; r_in 0 ]); - (* The object must be live to free *) - binexp - ~attrib: - (make_msg_attrib "Memory Error: Invalid Free (object not live)") - ~op:`EQ - (Calls.alloc_live - [ - rvar Globals.mem_encoding; - Calls.addr_alloc [ rvar Globals.mem_encoding; r_in 0 ]; - ]) - (bvconst live); - ]; - ensures = - spec.ensures - @ [ - binexp ~op:`EQ - ~attrib:(make_msg_attrib "Memory Error: Invalid Free") - (rvar Globals.mem_encoding) - (Calls.alloc_live_update - [ - old @@ rvar Globals.mem_encoding; - Calls.addr_alloc [ old @@ rvar Globals.mem_encoding; r_in 0 ]; - BasilExpr.bvconst dead; - ]); - ]; - modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; - captures_globs = spec.captures_globs @ [ Globals.mem_encoding ]; - } + let transform_main (p : Program.proc) = + (* TODO: Specify Gammas Oneday *) + let mem_encoding = BasilExpr.rvar @@ Globals.mem_encoding in + let spec = Procedure.specification p in + let i = Procedure.fresh_var p ~name:"i" ~pure:true (Types.Bitvector 64) in + Procedure.set_specification p + { + spec with + requires = + spec.requires + (* Require memory is initialized. *) + @ [ Calls.init_encoding [ mem_encoding ] ]; + (* Ensure there are no memory leaks. *) + ensures = + spec.ensures + @ [ + BasilExpr.forall + ~attrib:(make_msg_attrib "Memory Error: Memory Leak") + ~bound:[ i ] + @@ BasilExpr.binexp ~op:`IMPLIES + (Calls.addr_is_heap [ mem_encoding; BasilExpr.rvar i ]) + (BasilExpr.binexp ~op:`NEQ + (Calls.alloc_live + [ + mem_encoding; + Calls.addr_alloc [ mem_encoding; BasilExpr.rvar i ]; + ]) + (BasilExpr.bvconst live)); + ]; + modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; + captures_globs = spec.captures_globs @ [ Globals.mem_encoding ]; + } -let transform_stmt (s : Program.stmt) = - (match s with - | Stmt.Instr_Store { lhs; rhs; addr = Addr { addr; size; endian }; attrib } - | Stmt.Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } - -> ( - let valid_assert = - Stmt.Instr_Assert - { - attrib = make_msg_attrib "Memory Error: Invalid Access"; - body = - BasilExpr.( - Calls.valid_access - [ - rvar Globals.mem_encoding; - addr; - bv_of_int ~size:64 (size / 8); - ]); - } - in - match Var.name rhs with "$mem" -> [ valid_assert; s ] | _ -> [ s ]) - | _ -> [ s ]) - |> List.to_iter + let transform_malloc p = + (* TODO: Specify Gammas Oneday *) + let spec = Procedure.specification p in + let mem_encoding = BasilExpr.rvar @@ Globals.mem_encoding in + let pid = Var.mk_gen ~id_generator:(Procedure.local_ids p) () in + let r_in = r_in pid in + let r_out = r_out pid in + let open BasilExpr in + Procedure.set_specification p + { + spec with + ensures = + spec.ensures + @ [ + (* Can allocate at new r0 with size old r0 *) + Calls.can_alloc [ old @@ mem_encoding; r_out 0; r_in 0 ]; + (* Offset of return address r0 is 0 *) + binexp ~op:`EQ + (Calls.addr_offset [ mem_encoding; r_out 0 ]) + (bv_of_int ~size:64 0); + (* Base of associated allocation is r(0) *) + binexp ~op:`EQ + (Calls.alloc_base + [ mem_encoding; Calls.addr_alloc [ mem_encoding; r_out 0 ] ]) + (r_out 0); + (* Update the memory encoding: *) + Calls.allocate + [ old @@ mem_encoding; mem_encoding; r_out 0; r_in 0 ]; + ]; + modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; + captures_globs = spec.captures_globs @ [ Globals.mem_encoding ]; + } -let transform_proc entry _ (p : Program.proc) = + let transform_free p = + (* TODO: Specify Gammas Oneday *) + let spec = Procedure.specification p in + let open BasilExpr in + let mem_encoding = BasilExpr.rvar @@ Globals.mem_encoding in + let pid = Var.mk_gen ~id_generator:(Procedure.local_ids p) () in + let r_in = r_in pid in + Procedure.set_specification p + { + spec with + requires = + spec.requires + @ [ + (* Only free heap values *) + Calls.addr_is_heap + ~attrib: + (make_msg_attrib + "Memory Error: Invalid Free (non heap object)") + [ mem_encoding; r_in 0 ]; + (* Only free if offset is 0 *) + binexp + ~attrib: + (make_msg_attrib + "Memory Error: Invalid Free (not base address)") + ~op:`EQ (bv_of_int ~size:64 0) + (Calls.addr_offset [ mem_encoding; r_in 0 ]); + (* The object must be live to free *) + binexp + ~attrib: + (make_msg_attrib + "Memory Error: Invalid Free (object not live)") + ~op:`EQ + (Calls.alloc_live + [ mem_encoding; Calls.addr_alloc [ mem_encoding; r_in 0 ] ]) + (bvconst live); + ]; + ensures = + spec.ensures + @ [ + binexp ~op:`EQ + ~attrib:(make_msg_attrib "Memory Error: Invalid Free") + mem_encoding + (Calls.alloc_live_update + [ + old @@ mem_encoding; + Calls.addr_alloc [ old @@ mem_encoding; r_in 0 ]; + BasilExpr.bvconst dead; + ]); + ]; + modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; + captures_globs = spec.captures_globs @ [ Globals.mem_encoding ]; + } + + let transform_stmt (s : Program.stmt) = + (match s with + | Stmt.Instr_Store + { lhs; rhs; addr = Addr { addr; size; endian }; attrib } + | Stmt.Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } + -> ( + let valid_assert = + Stmt.Instr_Assert + { + attrib = make_msg_attrib "Memory Error: Invalid Access"; + body = + BasilExpr.( + Calls.valid_access + [ + rvar Globals.mem_encoding; + addr; + bv_of_int ~size:64 (size / 8); + ]); + } + in + match Var.name rhs with "$mem" -> [ valid_assert; s ] | _ -> [ s ]) + | _ -> [ s ]) + |> List.to_iter +end + +let transform_proc prog entry _ (p : Program.proc) = + let module TR = T (struct + let global_ids = Program.var_generator prog + end) in + let open TR in let p = Procedure.map_blocks_nondet (fun (i, b) -> Block.flat_map ~phi:Fun.id transform_stmt b) @@ -195,5 +198,5 @@ let transform_proc entry _ (p : Program.proc) = let transform (p : Program.t) = let entry = Program.entry_proc_exn p |> Procedure.id %> ID.name in - let p = Program.map_procedures (transform_proc entry) p in + let p = Program.map_procedures (transform_proc p entry) p in (fun prog -> Spec_modifies.set_modsets ~add_only:false prog) p diff --git a/lib/transforms/ssa.ml b/lib/transforms/ssa.ml index 8a775edd..dd283050 100644 --- a/lib/transforms/ssa.ml +++ b/lib/transforms/ssa.ml @@ -64,7 +64,7 @@ let drop_unused_var_declarations_proc p = |> Iter.fold (fun acc i -> VarSet.add i acc) acc) VarSet.empty p in - Var.Decls.filter_map_inplace + Hashtbl.filter_map_inplace (fun _ v -> if VarSet.mem v used then Some v else None) (Procedure.local_decls p); VarSet.filter Var.is_global used @@ -89,7 +89,7 @@ let should_lift ~skip_observable ~skip_maps v = let skip = (skip_observable && Var.is_shared v) || (skip_maps && Var.typ v |> function Map _ -> true | _ -> false) - || (Var.is_global v && Var.is_constant v) + || (Var.is_global v && Var.is_const v) in not skip @@ -254,7 +254,7 @@ let lift_procedure_params prog ~skip_observable ~skip_maps all_lifted procid let alg node = match node with | UnaryExpr { op = `Old; arg } -> replace [%here] arg - | RVar { id } when Var.is_constant id -> Keep + | RVar { id } when Var.is_const id -> Keep | RVar { id } -> ( match StringMap.find_opt (Var.name id) glob_to_inparam with | Some v -> replace [%here] (rvar v) @@ -284,8 +284,7 @@ let lift_procedure_params prog ~skip_observable ~skip_maps all_lifted procid let alg node = match node with | UnaryExpr { op = `Old; arg } -> replace [%here] (rewrite_old_expr arg) - | RVar { id } when Var.is_constant id || (not @@ VarSet.mem id fvs) -> - Keep + | RVar { id } when Var.is_const id || (not @@ VarSet.mem id fvs) -> Keep | RVar { id } -> ( match StringMap.find_opt (Var.name id) glob_to_outparam with | Some v -> replace [%here] (rvar v) diff --git a/lib/util/ID.ml b/lib/util/ID.ml index 118263cd..74b9e770 100644 --- a/lib/util/ID.ml +++ b/lib/util/ID.ml @@ -23,6 +23,7 @@ open struct type cache type generator = { + gen_id : string; (** unique id for this generator *) get_id : string -> t; (** return a previously declared unique integer identifier for a name *) @@ -38,7 +39,7 @@ open struct get_declared : unit -> M.t; } - val make_gen : unit -> generator + val make_gen : ?scope_name:string -> unit -> generator end end @@ -142,6 +143,7 @@ module ID : ID_Pub = struct (name, id) type generator = { + gen_id : string; get_id : string -> t; (** return a previously declared unique integer identifier for a name *) get_name : int -> t; (** get name for a given unique integer identifier *) @@ -155,9 +157,14 @@ module ID : ID_Pub = struct get_declared : unit -> M.t; } + let gen_ids = Fix.Gensym.make () + (** return a generator for unique hash-consed string identifiers. general implementation of a declaration *) - let make_gen () : generator = + let make_gen ?scope_name () : generator = + let gen_id = + Option.get_or ~default:(Int.to_string (gen_ids ())) scope_name + in let c = { names = ref M.empty; @@ -166,6 +173,7 @@ module ID : ID_Pub = struct } in { + gen_id; get_id = get_id c; get_name = get_name c; fresh = fresh c; @@ -176,8 +184,6 @@ module ID : ID_Pub = struct end include ID -module Map = Map.Make (ID) -module Set = Set.Make (ID) (** return a previously declared unique integer identifier for a name *) let get_id (g : generator) = g.get_id diff --git a/lib/util/var.ml b/lib/util/var.ml index 1ba6d057..a42cfb34 100644 --- a/lib/util/var.ml +++ b/lib/util/var.ml @@ -1,121 +1,126 @@ open Containers open Mtypes -type scope = LocalConst | LocalVar | GlobalVar | GlobalConst | GlobalVarShared -[@@deriving show, eq, ord] - -open struct - module V = struct - type t = { name : string; typ : Types.t; scope : scope } - [@@deriving eq, ord, show] - - let hash v = - Hash.(combine3 (Hash.string v.name) (Hash.poly v.scope) (Hash.poly v.typ)) - end -end - -(** variables are interned *) - -module H = Fix.HashCons.ForHashedTypeWeak (V) - -include ( - struct - type t = V.t Fix.HashCons.cell - - let create name ?(scope = LocalVar) typ = - (* disallow creating local const as its too hard to have declaration order *) - match scope with - | LocalConst -> H.make { name; typ; scope = LocalVar } - | _ -> H.make { name; typ; scope } - - let copy ?name ?scope ?typ (v : t) = - let v = Fix.HashCons.data v in - H.make - { - name = Option.get_or ~default:v.name name; - typ = Option.get_or ~default:v.typ typ; - scope = Option.get_or ~default:v.scope scope; - } - - let to_int (v : V.t Fix.HashCons.cell) = v.id - let show v = V.show (Fix.HashCons.data v) - let equal (a : t) (b : t) : bool = Fix.HashCons.equal a b - let compare (a : t) (b : t) : int = Fix.HashCons.compare a b - let name (e : t) = (Fix.HashCons.data e).name - let scope (e : t) = (Fix.HashCons.data e).scope - let typ (e : t) = (Fix.HashCons.data e).typ - let hash (a : t) = Fix.HashCons.hash a - let to_string v = name v ^ ":" ^ Types.to_string @@ typ v - let pp fmt v = Format.pp_print_string fmt (to_string v) - let pretty v = Containers_pp.text (to_string v) - end : - sig - type t - - val to_int : t -> int - - include HASH_TYPE with type t := t - include PRETTY with type t := t - - val create : string -> ?scope:scope -> Types.t -> t - val pp : Format.formatter -> t -> unit - val to_string : t -> string - val name : t -> string - val scope : t -> scope - val typ : t -> Types.t - val hash : t -> int - val copy : ?name:string -> ?scope:scope -> ?typ:Types.t -> t -> t - end) - -let is_local (v : t) = - match scope v with LocalVar -> true | LocalConst -> true | _ -> false - -let is_global (v : t) = - match scope v with - | GlobalVar -> true - | GlobalConst -> true - | GlobalVarShared -> true - | _ -> false - -let is_mutable (v : t) = - match scope v with GlobalVar -> true | LocalVar -> true | _ -> false - -let is_constant (v : t) = - match scope v with LocalConst -> true | GlobalConst -> true | _ -> false - -let is_pure (v : t) = is_constant v - -let is_shared (v : t) = - match scope v with GlobalVarShared -> true | _ -> false - +type access_tag = Const | Shared | None [@@deriving show, eq, ord] +type scope_tag = Global of string | Local of string [@@deriving show, eq, ord] + +type t = { name : ID.t; scope : scope_tag; typ : Types.t; tags : access_tag } +[@@deriving eq, ord, show] + +let hash v = + Hash.(combine3 (ID.hash v.name) (Hash.poly v.tags) (Hash.poly v.typ)) + +(* +let copy ?name ?scope ?typ (v : t) = + { + name = Option.get_or ~default:v.name name; + typ = Option.get_or ~default:v.typ typ; + scope = Option.get_or ~default:v.scope scope; + } *) + +let to_int (v : t) = ID.index v.name +let id v = v.name +let tags (e : t) = e.tags +let typ (e : t) = e.typ +let is_local (v : t) = match v.scope with Local _ -> true | Global _ -> false +let is_global (v : t) = match v.scope with Global _ -> true | Local _ -> false +let name (e : t) = if is_global e then "$" ^ ID.name e.name else ID.name e.name + +let name_scoped (e : t) = + let sn = e.scope |> function Local n -> n | Global n -> n in + name e ^ sn + +let to_string v = name v ^ ":" ^ Types.to_string @@ typ v +let pp fmt v = Format.pp_print_string fmt (to_string v) +let pretty v = Containers_pp.text (to_string v) +let is_const (v : t) = match v.tags with Const -> true | _ -> false +let access (v : t) = v.tags +let is_shared (v : t) = match v.tags with Shared -> true | _ -> false let to_string_il_rvar v = to_string v let to_string_il_lvar v = - match scope v with - | LocalVar -> "var " ^ to_string v - | LocalConst -> "let " ^ to_string v - | GlobalVar -> to_string v - | GlobalVarShared -> to_string v - | GlobalConst -> "let " ^ to_string v + match (v.scope, v.tags) with + | _, Const -> "let " ^ to_string v + | Local _, _ -> "var " ^ to_string v + | Global _, None -> to_string v + | Global _, Shared -> to_string v let to_decl_string_il v = let modifiers = if is_shared v then "observable " else "" in "var " ^ modifiers ^ to_string v -module Decls = struct - include Hashtbl - - type 'v t = (string, 'v) Hashtbl.t - - let find_opt m name = Hashtbl.find_opt m name - let empty () : 'v t = Hashtbl.create 30 +(** Variable Generators *) + +type generator = { + scope : scope_tag; + fresh : ?name:string -> ?access:access_tag -> Types.t -> t; + (** generate a fresh unique name optional string prefix hint *) + with_name : string -> ?access:access_tag -> Types.t -> t; + of_var : t -> t; (** Create or return variable with name*) + create_exn : string -> ?access:access_tag -> Types.t -> t; + (** Create variable or throw exception if it was previously declared *) + generator : ID.generator; (** The internal ID generator this closes over *) +} + +type ('t, 'a, 'g) any_gen = { + call : 'a -> 't; + (** Create variable or throw exception if it was previously declared *) + inner : 'g; +} - (*let add m vn v = - let d = find_opt m (name vn) in - match d with - | Some e when equal e v -> () - | Some _ -> - failwith @@ "Already declared diff var with that name: " ^ name v - | None -> Hashtbl.add m (name vn) v - *) +open struct + let force_sigil sigil s : string = + match String.chop_prefix ~pre:sigil s with Some s -> s | None -> s + + let create name id_gen ?(access = None) typ = + (* disallow creating local const as its too hard to have declaration order *) + let tags = match (id_gen, access) with Local _, _ -> None | _, o -> o in + { name; scope = id_gen; typ; tags } + + let fresh gt (gen : ID.generator) sgl name ?access typ = + let name = force_sigil sgl name in + let name = gen.fresh ~name () in + create name gt ?access typ + + let with_name gt (id_gen : ID.generator) sgl name ?access typ = + let name = force_sigil sgl name in + let name = id_gen.decl_or_get name in + create name gt ?access typ + + let of_var gt (id_gen : ID.generator) sgl v = + with_name gt id_gen sgl (name v) ~access:(access v) (typ v) + + let create_exn gt (id_gen : ID.generator) sgl name ?access typ = + let name = force_sigil sgl name in + let name = id_gen.decl_exn name in + create name gt ?access typ end + +let mk_gen ?id_generator ?(req_sigil = Option.None) ?(scope = `Local) + ?(default_name = "v") () = + let id_gen = Option.get_or ~default:(ID.make_gen ()) id_generator in + let gt = + match scope with + | `Local -> Local id_gen.gen_id + | `Global -> Global id_gen.gen_id + in + let sgl = + match (req_sigil, scope) with + | Some s, _ -> s + | None, `Local -> "" + | None, `Global -> "$" + in + + let fresh ?name ?access typ = + let name = Option.get_or ~default:default_name name in + fresh gt id_gen sgl name ?access typ + in + + { + scope = gt; + fresh; + with_name = with_name gt id_gen sgl; + create_exn = create_exn gt id_gen sgl; + of_var = of_var gt id_gen sgl; + generator = id_gen; + } diff --git a/test/analysis/test_ide_live.ml b/test/analysis/test_ide_live.ml index 020bacb7..fb2c2ce5 100644 --- a/test/analysis/test_ide_live.ml +++ b/test/analysis/test_ide_live.ml @@ -12,6 +12,9 @@ let%expect_test "intra_checks" = Loader.Loadir.ast_of_string {| memory shared $mem : (bv64 -> bv8); +var $x: bv64; +var $y: bv64; +var $z: bv64; prog entry @main; @@ -44,17 +47,16 @@ proc @main (a:bv64, b:bv64, c:bv64, d:bv64, e:bv64) -> () print_lives results main; [%expect {| - Warn: global undeclared $x assuming mutable unshared - Warn: global undeclared $y assuming mutable unshared - Warn: global undeclared $z assuming mutable unshared @main $mem:(bv64->bv8) a:bv64 + $x:bv64 b:bv64 + $y:bv64 c:bv64 + $z:bv64 d:bv64 e:bv64 - $x:bv64 |}] let%expect_test "phi_loop" = @@ -189,13 +191,13 @@ proc @fun2 (f:bv64) -> (out2:bv64) [%expect {| @main + $global:bv64 b:bv64 y:bv64 - $global:bv64 @fun1 + $global:bv64 c:bv64 d:bv64 - $global:bv64 @fun2 $global:bv64 f:bv64 @@ -256,13 +258,13 @@ proc @fun2 (f:bv64) -> (out2:bv64) [%expect {| @main + $global:bv64 b:bv64 y:bv64 - $global:bv64 @fun1 + $global:bv64 c:bv64 d:bv64 - $global:bv64 @fun2 $global:bv64 f:bv64 diff --git a/test/cram/chc_mem_call.il b/test/cram/chc_mem_call.il index b7fbf2cd..bc0cacfa 100644 --- a/test/cram/chc_mem_call.il +++ b/test/cram/chc_mem_call.il @@ -29,7 +29,7 @@ proc @foo() -> () proc @main() -> () [ block %entry [ - $mem := store le $mem 0x100:bv64 secret:bv8 8; + $mem := store le $mem 0x100:bv64 $secret:bv8 8; call @foo (); var v:bv8 := load le $mem 0x100:bv64 8; assert eq(v:bv8, bvadd($secret, 5:bv8)); diff --git a/test/cram/concat.il b/test/cram/concat.il index 04217d06..78b757c1 100644 --- a/test/cram/concat.il +++ b/test/cram/concat.il @@ -2,6 +2,7 @@ var $R28:bv64; var $R0:bv64; var $R30:bv64; +var $__BranchTaken:bv1; prog entry @main_4204352; proc @main_4204352() -> () [ diff --git a/test/cram/expr_smt.t b/test/cram/expr_smt.t index ad6416f5..dd7506ef 100644 --- a/test/cram/expr_smt.t +++ b/test/cram/expr_smt.t @@ -6,7 +6,6 @@ Should output no errors (load-il ../../examples/cntlm-output.il) (run-transforms cf-expressions-smtcheck) (load-il concat.il) - Warn: global undeclared $__BranchTaken assuming mutable unshared (dump-il before.il) (run-transforms cf-expressions-smtcheck) (dump-il after.il) @@ -14,7 +13,7 @@ Should output no errors Check concat rewrites work $ diff before.il after.il - 16,82c16,18 + 17,83c17,19 < $R28:bv64 := bvor(bvand(bvconcat(extract(1,0, bvlshr(var1_4206396_bv64:bv64, < 0x1f:bv64)), extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), @@ -86,7 +85,7 @@ Check concat rewrites work > $R28:bv64 := bvor(bvand(sign_extend(63, > extract(32,31, var1_4206396_bv64:bv64)), 0xffffffff00000000:bv64), > bvand(var1_4206396_bv64:bv64, 0xffffffff:bv64, 0xffffffff:bv64)); - 87,88c23 + 88,89c24 < $R0:bv64 := bvor(var1_4206400_bv64:bv64, < bvshl(var2_4206400_bv64:bv64, 0x0:bv64)); --- diff --git a/test/cram/gammavars.t b/test/cram/gammavars.t index 3a7eb06b..d93d9717 100644 --- a/test/cram/gammavars.t +++ b/test/cram/gammavars.t @@ -3,65 +3,10 @@ (load-il ../../examples/gamma.il) (dump-il before.il) (run-transforms gamma-vars) - bincaml: [ERROR] global Gamma_$x:bool should have global sigil $ (dump-il after.il) $ diff before.il after.il - 2,6c2,6 - < proc @main() -> (out:bv64) { } - < modifies $x:bv64 - < captures $x:bv64 - < requires gamma($x) - < ensures gamma($x) - --- - > proc @main() -> (Gamma_out:bool, out:bv64) { } - > modifies Gamma_$x:bool, $x:bv64 - > captures Gamma_$x:bool, $x:bv64 - > requires Gamma_$x - > ensures Gamma_$x - 9,10c9,16 - < block %main_entry [ ($x:bv64=out) := call @f(z=$x); goto (%main_return); ]; - < block %main_return [ var out:bv64 := $x; return; ] - --- - > block %main_entry [ - > (Gamma_$x:bool=Gamma_out, $x:bv64=out) := call @f(Gamma_z=Gamma_$x, z=$x); - > goto (%main_return); - > ]; - > block %main_return [ - > (var Gamma_out:bool := Gamma_$x, var out:bv64 := $x); - > return; - > ] - 12,14c18,20 - < proc @f(z:bv64) -> (out:bv64) { } - < requires gamma(z:bv64) - < ensures eq(gamma(out:bv64), old(gamma(z:bv64))) - --- - > proc @f(Gamma_z:bool, z:bv64) -> (Gamma_out:bool, out:bv64) { } - > requires Gamma_z:bool - > ensures eq(Gamma_out:bool, old(Gamma_z:bool)) - 18,19c24,26 - < (var out:bv64=out) := call @h(a=z:bv64, b=bvmul(z:bv64, z:bv64)); - < var out:bv64 := out:bv64; - --- - > (var Gamma_out:bool=Gamma_out, var out:bv64=out) := call @h(Gamma_a=Gamma_z:bool, - > Gamma_b=Gamma_z:bool, a=z:bv64, b=bvmul(z:bv64, z:bv64)); - > (var Gamma_out:bool := Gamma_out:bool, var out:bv64 := out:bv64); - 23,25c30,32 - < proc @g(a:bv64) -> (out:bv64) { } - < requires gamma(a:bv64) - < ensures eq(gamma(out:bv64), old(gamma(a:bv64))) - --- - > proc @g(Gamma_a:bool, a:bv64) -> (Gamma_out:bool, out:bv64) { } - > requires Gamma_a:bool - > ensures eq(Gamma_out:bool, old(Gamma_a:bool)) - 29,30c36,38 - < (var out:bv64=out) := call @h(a=a:bv64, b=bvsub(a:bv64, 0x1:bv64)); - < var out:bv64 := out:bv64; - --- - > (var Gamma_out:bool=Gamma_out, var out:bv64=out) := call @h(Gamma_a=Gamma_a:bool, - > Gamma_b=Gamma_a:bool, a=a:bv64, b=bvsub(a:bv64, 0x1:bv64)); - > (var Gamma_out:bool := Gamma_out:bool, var out:bv64 := out:bv64); - 34,37c42,45 + 34,37c34,37 < proc @h(a:bv64, b:bv64) -> (out:bv64) { } < requires booland(gamma(a:bv64), gamma(b:bv64)) < ensures boolor(boolnot(booland(old(gamma(a:bv64)), old(gamma(b:bv64)))), @@ -71,30 +16,28 @@ > requires booland(Gamma_a:bool, Gamma_b:bool) > ensures boolor(boolnot(booland(old(Gamma_a:bool), old(Gamma_b:bool))), > Gamma_out:bool) - 42c50 + 42c42 < assert gamma(a:bv64); --- > assert Gamma_a:bool; - 44c52 + 44c44 < var c:bv64 := b:bv64; --- > (var Gamma_c:bool := Gamma_b:bool, var c:bv64 := b:bv64); - 48c56 + 48c48 < assert gamma(a:bv64); --- > assert Gamma_a:bool; - 50c58,59 + 50c50,51 < (var c:bv64=out) := call @g(a=bvadd(a:bv64, b:bv64)); --- > (var Gamma_c:bool=Gamma_out, var c:bv64=out) := call @g(Gamma_a=booland(Gamma_a:bool, > Gamma_b:bool), a=bvadd(a:bv64, b:bv64)); - 53c62,65 + 53c54,57 < block %h_return [ var out:bv64 := bvadd(c:bv64, 0x1:bv64); return; ] --- > block %h_return [ > (var Gamma_out:bool := Gamma_c:bool, var out:bv64 := bvadd(c:bv64, 0x1:bv64)); > return; > ] - 54a67 - > var Gamma_$x:bool; [1] diff --git a/test/cram/malloc_free.t b/test/cram/malloc_free.t index e89c58a2..b6851167 100644 --- a/test/cram/malloc_free.t +++ b/test/cram/malloc_free.t @@ -11,26 +11,32 @@ $ cat ./good.bpl var $mem: [bv64]bv8; var $stack: [bv64]bv8; - datatype memory_encoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} var $mem_encoding: memory_encoding; - function {:extern } {:inline } $me_addr_offset(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { - bvand_bv64(addr, 4294967295bv64) - } - function {:extern } {:inline } $me_alloc_base(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { - bvand_bv64(alloc, 18446744069414584320bv64) + function {:extern } {:inline } $me_addr_alloc(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { + addr } function {:extern } {:inline } $me_alloc_live(mem_encoding: memory_encoding, alloc: bv64) returns (bv2) { mem_encoding->alloc_live[alloc] } - function {:extern } {:inline } $me_alloc_size(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { - mem_encoding->alloc_size[alloc] - } - function {:extern } {:inline } $me_addr_alloc(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { - addr + function {:extern } {:inline } $me_alloc_base(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { + $bvand_bv64(alloc, 18446744069414584320bv64) } function {:extern } {:inline } $me_addr_is_heap(mem_encoding: memory_encoding, addr: bv64) returns (bool) { mem_encoding->addr_is_heap[addr] } + function {:extern } {:inline } $me_alloc_live_update(mem_encoding: memory_encoding, alloc: bv64, live: bv2) returns (memory_encoding) { + mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) + } + function {:extern } {:inline } $me_alloc_size_update(mem_encoding: memory_encoding, alloc: bv64, size: bv64) returns (memory_encoding) { + mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) + } + function {:extern } {:inline } $me_alloc_size(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { + mem_encoding->alloc_size[alloc] + } + function {:extern } {:inline } $me_addr_offset(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { + $bvand_bv64(addr, 4294967295bv64) + } + datatype memory_encoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} function {:extern } {:inline } $me_can_allocate(mem_encoding: memory_encoding, addr: bv64, size: bv64) returns (bool) { (((($me_addr_is_heap(mem_encoding, addr) && @@ -38,15 +44,9 @@ && ($me_alloc_live(mem_encoding, $me_addr_alloc(mem_encoding, addr)) == 0bv2)) && - bvule_bv64_bv64_bool(size, 4294967295bv64)) + $bvule_bv64_bv64_bool(size, 4294967295bv64)) && - bvult_bv64_bv64_bool(0bv64, size)) - } - function {:extern } {:inline } $me_alloc_size_update(mem_encoding: memory_encoding, alloc: bv64, size: bv64) returns (memory_encoding) { - mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) - } - function {:extern } {:inline } $me_alloc_live_update(mem_encoding: memory_encoding, alloc: bv64, live: bv2) returns (memory_encoding) { - mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) + $bvult_bv64_bv64_bool(0bv64, size)) } function {:extern } {:inline } $me_allocate(mem_encoding: memory_encoding, mem_encoding_out: memory_encoding, addr: bv64, size: bv64) returns (bool) { ($me_alloc_size_update( @@ -63,7 +63,7 @@ (((forall i: bv64 :: {$me_addr_is_heap(mem_encoding, i)} - (bvult_bv64_bv64_bool(100000000bv64, i) == $me_addr_is_heap( + ($bvult_bv64_bv64_bool(100000000bv64, i) == $me_addr_is_heap( mem_encoding, i ))) @@ -84,55 +84,55 @@ $me_alloc_base(mem_encoding, $me_addr_alloc(mem_encoding, addr)) ) == 1bv2) && - bvule_bv64_bv64_bool( - $me_addr_offset(mem_encoding, bvadd_bv64(addr, size)), + $bvule_bv64_bv64_bool( + $me_addr_offset(mem_encoding, $bvadd_bv64(addr, size)), $me_alloc_size( mem_encoding, $me_alloc_base(mem_encoding, $me_addr_alloc(mem_encoding, addr)) ) ))) } - function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { - (((((((#memory[bvadd_bv64(#index, 7bv64)] + function {:extern } $load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { + (((((((#memory[$bvadd_bv64(#index, 7bv64)] ++ - #memory[bvadd_bv64(#index, 6bv64)]): bv16 + #memory[$bvadd_bv64(#index, 6bv64)]): bv16 ++ - #memory[bvadd_bv64(#index, 5bv64)]): bv24 + #memory[$bvadd_bv64(#index, 5bv64)]): bv24 ++ - #memory[bvadd_bv64(#index, 4bv64)]): bv32 + #memory[$bvadd_bv64(#index, 4bv64)]): bv32 ++ - #memory[bvadd_bv64(#index, 3bv64)]): bv40 + #memory[$bvadd_bv64(#index, 3bv64)]): bv40 ++ - #memory[bvadd_bv64(#index, 2bv64)]): bv48 + #memory[$bvadd_bv64(#index, 2bv64)]): bv48 ++ - #memory[bvadd_bv64(#index, 1bv64)]): bv56 + #memory[$bvadd_bv64(#index, 1bv64)]): bv56 ++ - #memory[bvadd_bv64(#index, 0bv64)]): bv64 + #memory[$bvadd_bv64(#index, 0bv64)]): bv64 } - function {:define } {:extern } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { - #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64( + function {:define } {:extern } $store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { + #memory[#index := #value[8:0]][$bvadd_bv64(#index, 1bv64) := #value[16:8]][$bvadd_bv64( #index, 2bv64 - ) := #value[24:16]][bvadd_bv64(#index, 3bv64) := #value[32:24]][bvadd_bv64( + ) := #value[24:16]][$bvadd_bv64(#index, 3bv64) := #value[32:24]][$bvadd_bv64( #index, 4bv64 - ) := #value[40:32]][bvadd_bv64(#index, 5bv64) := #value[48:40]][bvadd_bv64( + ) := #value[40:32]][$bvadd_bv64(#index, 5bv64) := #value[48:40]][$bvadd_bv64( #index, 6bv64 - ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]] + ) := #value[56:48]][$bvadd_bv64(#index, 7bv64) := #value[64:56]] } - function {:define } {:extern } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { + function {:define } {:extern } $store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { #memory[#index := #value[8:0]] } - function {:bvbuiltin "bvadd"} {:extern } bvadd_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvand"} {:extern } bvand_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvule"} {:extern } bvule_bv64_bv64_bool(bv64, bv64) returns (bool); - function {:bvbuiltin "bvult"} {:extern } bvult_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:bvbuiltin "bvadd"} {:extern } $bvadd_bv64(bv64, bv64) returns (bv64); + function {:bvbuiltin "bvand"} {:extern } $bvand_bv64(bv64, bv64) returns (bv64); + function {:bvbuiltin "bvule"} {:extern } $bvule_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:bvbuiltin "bvult"} {:extern } $bvult_bv64_bv64_bool(bv64, bv64) returns (bool); procedure p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64, R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64, R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $stack, $mem_encoding; ensures {:msg "Memory Error: Memory Leak"} (forall i: bv64 :: @@ -144,22 +144,23 @@ implementation p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64, R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64, R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64) { + var Exp14__5_2_2: bv64; + var i: bv64; + var Exp14__5_1_2: bv64; var Exp18__5_25_2: bv64; var Exp14__5_21_2: bv64; var Exp14__5_22_2: bv64; var R0_4: bv64; var Exp16__5_24_2: bv64; - var Exp14__5_2_2: bv64; - var Exp14__5_1_2: bv64; b#main_entry: - $stack := store64_le( + $stack := $store64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551584bv64), + $bvadd_bv64(R31_in, 18446744073709551584bv64), R29_in ); - $stack := store64_le( + $stack := $store64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551592bv64), + $bvadd_bv64(R31_in, 18446744073709551592bv64), R30_in ); assert{:msg "Memory Error: Invalid Access"} $me_valid_access( @@ -167,47 +168,47 @@ 131088bv64, 8bv64 ); - Exp14__5_2_2 := load64_le($mem, 131088bv64); + Exp14__5_2_2 := $load64_le($mem, 131088bv64); assert true; call R0_4 := p$malloc(1bv64); goto b#phi_5; b#phi_5: - $stack := store64_le( + $stack := $store64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551608bv64), + $bvadd_bv64(R31_in, 18446744073709551608bv64), R0_4 ); - Exp14__5_21_2 := load64_le( + Exp14__5_21_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551608bv64) + $bvadd_bv64(R31_in, 18446744073709551608bv64) ); assert{:msg "Memory Error: Invalid Access"} $me_valid_access( $mem_encoding, Exp14__5_21_2, 1bv64 ); - $mem := store8_le($mem, Exp14__5_21_2, 121bv8); - Exp14__5_22_2 := load64_le( + $mem := $store8_le($mem, Exp14__5_21_2, 121bv8); + Exp14__5_22_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551608bv64) + $bvadd_bv64(R31_in, 18446744073709551608bv64) ); assert{:msg "Memory Error: Invalid Access"} $me_valid_access( $mem_encoding, 131112bv64, 8bv64 ); - Exp14__5_1_2 := load64_le($mem, 131112bv64); + Exp14__5_1_2 := $load64_le($mem, 131112bv64); assert true; call p$#free(Exp14__5_22_2); goto b#phi_6; b#phi_6: - Exp16__5_24_2 := load64_le( + Exp16__5_24_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551584bv64) + $bvadd_bv64(R31_in, 18446744073709551584bv64) ); - Exp18__5_25_2 := load64_le( + Exp18__5_25_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551592bv64) + $bvadd_bv64(R31_in, 18446744073709551592bv64) ); goto b#main_return; b#main_return: @@ -216,13 +217,13 @@ return; } procedure p$malloc(R0_in: bv64) returns (R0_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $stack, $mem_encoding; ensures $me_can_allocate(old($mem_encoding), R0_out, R0_in); ensures ($me_addr_offset($mem_encoding, R0_out) == 0bv64); ensures ($me_alloc_base($mem_encoding, $me_addr_alloc($mem_encoding, R0_out)) == R0_out); ensures $me_allocate(old($mem_encoding), $mem_encoding, R0_out, R0_in); procedure p$#free(R0_in: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $stack, $mem_encoding; ensures {:msg "Memory Error: Invalid Free"} ($mem_encoding == $me_alloc_live_update( old($mem_encoding), $me_addr_alloc(old($mem_encoding), R0_in), @@ -248,26 +249,32 @@ $ cat ./bad.bpl var $mem: [bv64]bv8; var $stack: [bv64]bv8; - datatype memory_encoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} var $mem_encoding: memory_encoding; - function {:extern } {:inline } $me_addr_offset(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { - bvand_bv64(addr, 4294967295bv64) - } - function {:extern } {:inline } $me_alloc_base(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { - bvand_bv64(alloc, 18446744069414584320bv64) + function {:extern } {:inline } $me_addr_alloc(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { + addr } function {:extern } {:inline } $me_alloc_live(mem_encoding: memory_encoding, alloc: bv64) returns (bv2) { mem_encoding->alloc_live[alloc] } - function {:extern } {:inline } $me_alloc_size(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { - mem_encoding->alloc_size[alloc] - } - function {:extern } {:inline } $me_addr_alloc(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { - addr + function {:extern } {:inline } $me_alloc_base(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { + $bvand_bv64(alloc, 18446744069414584320bv64) } function {:extern } {:inline } $me_addr_is_heap(mem_encoding: memory_encoding, addr: bv64) returns (bool) { mem_encoding->addr_is_heap[addr] } + function {:extern } {:inline } $me_alloc_live_update(mem_encoding: memory_encoding, alloc: bv64, live: bv2) returns (memory_encoding) { + mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) + } + function {:extern } {:inline } $me_alloc_size_update(mem_encoding: memory_encoding, alloc: bv64, size: bv64) returns (memory_encoding) { + mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) + } + function {:extern } {:inline } $me_alloc_size(mem_encoding: memory_encoding, alloc: bv64) returns (bv64) { + mem_encoding->alloc_size[alloc] + } + function {:extern } {:inline } $me_addr_offset(mem_encoding: memory_encoding, addr: bv64) returns (bv64) { + $bvand_bv64(addr, 4294967295bv64) + } + datatype memory_encoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} function {:extern } {:inline } $me_can_allocate(mem_encoding: memory_encoding, addr: bv64, size: bv64) returns (bool) { (((($me_addr_is_heap(mem_encoding, addr) && @@ -275,15 +282,9 @@ && ($me_alloc_live(mem_encoding, $me_addr_alloc(mem_encoding, addr)) == 0bv2)) && - bvule_bv64_bv64_bool(size, 4294967295bv64)) + $bvule_bv64_bv64_bool(size, 4294967295bv64)) && - bvult_bv64_bv64_bool(0bv64, size)) - } - function {:extern } {:inline } $me_alloc_size_update(mem_encoding: memory_encoding, alloc: bv64, size: bv64) returns (memory_encoding) { - mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) - } - function {:extern } {:inline } $me_alloc_live_update(mem_encoding: memory_encoding, alloc: bv64, live: bv2) returns (memory_encoding) { - mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) + $bvult_bv64_bv64_bool(0bv64, size)) } function {:extern } {:inline } $me_allocate(mem_encoding: memory_encoding, mem_encoding_out: memory_encoding, addr: bv64, size: bv64) returns (bool) { ($me_alloc_size_update( @@ -300,7 +301,7 @@ (((forall i: bv64 :: {$me_addr_is_heap(mem_encoding, i)} - (bvult_bv64_bv64_bool(100000000bv64, i) == $me_addr_is_heap( + ($bvult_bv64_bv64_bool(100000000bv64, i) == $me_addr_is_heap( mem_encoding, i ))) @@ -321,55 +322,55 @@ $me_alloc_base(mem_encoding, $me_addr_alloc(mem_encoding, addr)) ) == 1bv2) && - bvule_bv64_bv64_bool( - $me_addr_offset(mem_encoding, bvadd_bv64(addr, size)), + $bvule_bv64_bv64_bool( + $me_addr_offset(mem_encoding, $bvadd_bv64(addr, size)), $me_alloc_size( mem_encoding, $me_alloc_base(mem_encoding, $me_addr_alloc(mem_encoding, addr)) ) ))) } - function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { - (((((((#memory[bvadd_bv64(#index, 7bv64)] + function {:extern } $load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { + (((((((#memory[$bvadd_bv64(#index, 7bv64)] ++ - #memory[bvadd_bv64(#index, 6bv64)]): bv16 + #memory[$bvadd_bv64(#index, 6bv64)]): bv16 ++ - #memory[bvadd_bv64(#index, 5bv64)]): bv24 + #memory[$bvadd_bv64(#index, 5bv64)]): bv24 ++ - #memory[bvadd_bv64(#index, 4bv64)]): bv32 + #memory[$bvadd_bv64(#index, 4bv64)]): bv32 ++ - #memory[bvadd_bv64(#index, 3bv64)]): bv40 + #memory[$bvadd_bv64(#index, 3bv64)]): bv40 ++ - #memory[bvadd_bv64(#index, 2bv64)]): bv48 + #memory[$bvadd_bv64(#index, 2bv64)]): bv48 ++ - #memory[bvadd_bv64(#index, 1bv64)]): bv56 + #memory[$bvadd_bv64(#index, 1bv64)]): bv56 ++ - #memory[bvadd_bv64(#index, 0bv64)]): bv64 + #memory[$bvadd_bv64(#index, 0bv64)]): bv64 } - function {:define } {:extern } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { - #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64( + function {:define } {:extern } $store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { + #memory[#index := #value[8:0]][$bvadd_bv64(#index, 1bv64) := #value[16:8]][$bvadd_bv64( #index, 2bv64 - ) := #value[24:16]][bvadd_bv64(#index, 3bv64) := #value[32:24]][bvadd_bv64( + ) := #value[24:16]][$bvadd_bv64(#index, 3bv64) := #value[32:24]][$bvadd_bv64( #index, 4bv64 - ) := #value[40:32]][bvadd_bv64(#index, 5bv64) := #value[48:40]][bvadd_bv64( + ) := #value[40:32]][$bvadd_bv64(#index, 5bv64) := #value[48:40]][$bvadd_bv64( #index, 6bv64 - ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]] + ) := #value[56:48]][$bvadd_bv64(#index, 7bv64) := #value[64:56]] } - function {:define } {:extern } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { + function {:define } {:extern } $store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { #memory[#index := #value[8:0]] } - function {:bvbuiltin "bvadd"} {:extern } bvadd_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvand"} {:extern } bvand_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvule"} {:extern } bvule_bv64_bv64_bool(bv64, bv64) returns (bool); - function {:bvbuiltin "bvult"} {:extern } bvult_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:bvbuiltin "bvadd"} {:extern } $bvadd_bv64(bv64, bv64) returns (bv64); + function {:bvbuiltin "bvand"} {:extern } $bvand_bv64(bv64, bv64) returns (bv64); + function {:bvbuiltin "bvule"} {:extern } $bvule_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:bvbuiltin "bvult"} {:extern } $bvult_bv64_bv64_bool(bv64, bv64) returns (bool); procedure p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64, R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64, R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $stack, $mem_encoding; ensures {:msg "Memory Error: Memory Leak"} (forall i: bv64 :: @@ -381,22 +382,23 @@ implementation p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64, R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64, R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64) { + var Exp14__5_2_2: bv64; + var i: bv64; + var Exp14__5_1_2: bv64; var Exp18__5_25_2: bv64; var Exp14__5_21_2: bv64; var Exp14__5_22_2: bv64; var R0_4: bv64; var Exp16__5_24_2: bv64; - var Exp14__5_2_2: bv64; - var Exp14__5_1_2: bv64; b#main_entry: - $stack := store64_le( + $stack := $store64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551584bv64), + $bvadd_bv64(R31_in, 18446744073709551584bv64), R29_in ); - $stack := store64_le( + $stack := $store64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551592bv64), + $bvadd_bv64(R31_in, 18446744073709551592bv64), R30_in ); assert{:msg "Memory Error: Invalid Access"} $me_valid_access( @@ -404,47 +406,47 @@ 131088bv64, 8bv64 ); - Exp14__5_2_2 := load64_le($mem, 131088bv64); + Exp14__5_2_2 := $load64_le($mem, 131088bv64); assert true; call R0_4 := p$malloc(1bv64); goto b#phi_5; b#phi_5: - $stack := store64_le( + $stack := $store64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551608bv64), + $bvadd_bv64(R31_in, 18446744073709551608bv64), R0_4 ); - Exp14__5_21_2 := load64_le( + Exp14__5_21_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551608bv64) + $bvadd_bv64(R31_in, 18446744073709551608bv64) ); assert{:msg "Memory Error: Invalid Access"} $me_valid_access( $mem_encoding, - bvadd_bv64(Exp14__5_21_2, 7bv64), + $bvadd_bv64(Exp14__5_21_2, 7bv64), 1bv64 ); - $mem := store8_le($mem, bvadd_bv64(Exp14__5_21_2, 7bv64), 121bv8); - Exp14__5_22_2 := load64_le( + $mem := $store8_le($mem, $bvadd_bv64(Exp14__5_21_2, 7bv64), 121bv8); + Exp14__5_22_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551608bv64) + $bvadd_bv64(R31_in, 18446744073709551608bv64) ); assert{:msg "Memory Error: Invalid Access"} $me_valid_access( $mem_encoding, 131112bv64, 8bv64 ); - Exp14__5_1_2 := load64_le($mem, 131112bv64); + Exp14__5_1_2 := $load64_le($mem, 131112bv64); assert true; call p$#free(Exp14__5_22_2); goto b#phi_6; b#phi_6: - Exp16__5_24_2 := load64_le( + Exp16__5_24_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551584bv64) + $bvadd_bv64(R31_in, 18446744073709551584bv64) ); - Exp18__5_25_2 := load64_le( + Exp18__5_25_2 := $load64_le( $stack, - bvadd_bv64(R31_in, 18446744073709551592bv64) + $bvadd_bv64(R31_in, 18446744073709551592bv64) ); goto b#main_return; b#main_return: @@ -453,13 +455,13 @@ return; } procedure p$malloc(R0_in: bv64) returns (R0_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $stack, $mem_encoding; ensures $me_can_allocate(old($mem_encoding), R0_out, R0_in); ensures ($me_addr_offset($mem_encoding, R0_out) == 0bv64); ensures ($me_alloc_base($mem_encoding, $me_addr_alloc($mem_encoding, R0_out)) == R0_out); ensures $me_allocate(old($mem_encoding), $mem_encoding, R0_out, R0_in); procedure p$#free(R0_in: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $stack, $mem_encoding; ensures {:msg "Memory Error: Invalid Free"} ($mem_encoding == $me_alloc_live_update( old($mem_encoding), $me_addr_alloc(old($mem_encoding), R0_in), @@ -476,14 +478,11 @@ ) == 1bv2); -<<<<<<< HEAD -======= ->>>>>>> origin/main $ boogie ./bad.bpl Memory Error: Invalid Access Execution trace: - ./bad.bpl(143,3): b#main_entry + ./bad.bpl(144,3): b#main_entry Boogie program verifier finished with 0 verified, 1 error diff --git a/test/cram/memassign.il b/test/cram/memassign.il index cdf0bef6..1b4bf67d 100644 --- a/test/cram/memassign.il +++ b/test/cram/memassign.il @@ -11,10 +11,10 @@ type record = Record of {a : bv64; b: bv32; c:bv64}; type ilist = Cons of {head:bv64; tail:ilist} | Nil ; -let $a = UninterpSort; +let $a = $UninterpSort; -let $b = Record {a=1:bv64; b=2:bv64; c=3:bv64}; +let $b = $Record (1:bv64, 2:bv64, 3:bv64); let $mul_2 (a:bv64), (b:bv64) : bv64 = bvadd(b, bvmul(a, 2:bv64)); let $three = let func (a:bv64) : bv64 = bvadd(a, 1:bv64) in func($mul_2(2:bv64, 1:bv64)); diff --git a/test/cram/roundtrip.t b/test/cram/roundtrip.t index 45ec3210..97da1c57 100644 --- a/test/cram/roundtrip.t +++ b/test/cram/roundtrip.t @@ -55,8 +55,8 @@ Memassign repr return; ] ]; - let $a : uninterpSort = UninterpSort; - let $b : record = (Record)(0x1:bv64, 0x2:bv64, 0x3:bv64); + let $a : uninterpSort = $UninterpSort; + let $b : record = ($Record)(0x1:bv64, 0x2:bv64, 0x3:bv64); let $three : bv64 = let func (a:bv64) : bv64 = (bvadd(a:bv64, 0x1:bv64)) in ((func:(bv64->bv64))(($mul_2)(0x2:bv64, 0x1:bv64))); prog entry @main_4196164; diff --git a/test/cram/sva.t b/test/cram/sva.t index 1a7167f1..a1f1830b 100644 --- a/test/cram/sva.t +++ b/test/cram/sva.t @@ -1,5 +1,74 @@ $ bincaml script ./sva.sexp (load-il ../../examples/irreducible_loop_1.il) (run-transforms ssa sva) - (CF_in->(Par(@puts_1584_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@puts_1584_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@puts_1584_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@puts_1584_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@puts_1584_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@puts_1584_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@puts_1584)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@puts_1584_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@puts_1584_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), _->⊥) - (CF_in->(Par(@main_1876_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@main_1876_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@main_1876_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@main_1876_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@main_1876_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@main_1876_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@main_1876_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_out->(Ret(@puts_1584_{ Var.V.name = "CF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_out->(Ret(@puts_1584_{ Var.V.name = "NF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_out->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_out->(Ret(@puts_1584_{ Var.V.name = "R1_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_out->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_out->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_out->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), VF_out->(Ret(@puts_1584_{ Var.V.name = "VF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_out->(Ret(@puts_1584_{ Var.V.name = "ZF_12"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_1->(Par(@main_1876_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_1->(Par(@main_1876_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_1->(Par(@main_1876_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_1->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_1->(Par(@main_1876_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_1->(Par(@main_1876_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_1->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_1->(Par(@main_1876_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_1->(Par(@main_1876_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), #4_1->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R31_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R29_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R0_2->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_3->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), R0_4->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_5->(Constant->⟦0x20040:bv64, 0x20040:bv64⟧, _->⊥), load18_1->(Loaded(load18_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_6->(Loaded(load18_1)->⊤, _->⊥), R0_7->(Loaded(load18_1)->⊤, _->⊥), #5_1->(Loaded(load18_1)->⊤, _->⊥), VF_2->(Loaded(load18_1)->⊤, _->⊥), CF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_2->(Loaded(load18_1)->⊤, _->⊥), NF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_3->(Loaded(load18_1)->⊤, _->⊥), ZF_4->(Loaded(load18_1)->⊤, _->⊥), ZF_5->(Ret(@puts_1584_{ Var.V.name = "ZF_10"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), VF_3->(Ret(@puts_1584_{ Var.V.name = "VF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), R31_3->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R31_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_3->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R29_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_2->(Loaded(load19_1)->⊤, Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_3->(Ret(@puts_1584_{ Var.V.name = "NF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), CF_3->(Ret(@puts_1584_{ Var.V.name = "CF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), R0_8->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_9->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_2->(Constant->⟦0x7d0:bv64, 0x7d0:bv64⟧, _->⊥), CF_4->(Ret(@puts_1584_{ Var.V.name = "CF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_4->(Ret(@puts_1584_{ Var.V.name = "NF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_10->(Ret(@puts_1584_{ Var.V.name = "R0_10"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_3->(Ret(@puts_1584_{ Var.V.name = "R1_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_4->(Ret(@puts_1584_{ Var.V.name = "R29_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_3->(Ret(@puts_1584_{ Var.V.name = "R30_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_4->(Ret(@puts_1584_{ Var.V.name = "R31_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_4->(Ret(@puts_1584_{ Var.V.name = "VF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_6->(Ret(@puts_1584_{ Var.V.name = "ZF_6"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_11->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_12->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load20_1->(Loaded(load20_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_13->(Loaded(load20_1)->⊤, _->⊥), #6_1->(Loaded(load20_1)->⊤, _->⊥), VF_5->(Loaded(load20_1)->⊤, _->⊥), CF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_7->(Loaded(load20_1)->⊤, _->⊥), NF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_8->(Loaded(load20_1)->⊤, _->⊥), ZF_9->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), VF_6->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), R31_5->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R31_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_5->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R29_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_4->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R1_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_6->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), CF_6->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), R0_14->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_15->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_4->(Constant->⟦0x7a0:bv64, 0x7a0:bv64⟧, _->⊥), CF_7->(Ret(@puts_1584_{ Var.V.name = "CF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_7->(Ret(@puts_1584_{ Var.V.name = "NF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_16->(Ret(@puts_1584_{ Var.V.name = "R0_16"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_5->(Ret(@puts_1584_{ Var.V.name = "R1_5"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_6->(Ret(@puts_1584_{ Var.V.name = "R29_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_5->(Ret(@puts_1584_{ Var.V.name = "R30_5"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_6->(Ret(@puts_1584_{ Var.V.name = "R31_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_7->(Ret(@puts_1584_{ Var.V.name = "VF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_10->(Ret(@puts_1584_{ Var.V.name = "ZF_10"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_17->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_18->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load19_1->(Loaded(load19_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_19->(Loaded(load19_1)->⊤, _->⊥), R1_6->(Loaded(load19_1)->⊤, _->⊥), R0_20->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_21->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), ZF_11->(Loaded(load20_1)->⊤, _->⊥), R0_22->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_23->(Constant->⟦0x828:bv64, 0x828:bv64⟧, _->⊥), R30_6->(Constant->⟦0x7f4:bv64, 0x7f4:bv64⟧, _->⊥), CF_8->(Ret(@puts_1584_{ Var.V.name = "CF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_8->(Ret(@puts_1584_{ Var.V.name = "NF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_24->(Ret(@puts_1584_{ Var.V.name = "R0_24"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_7->(Ret(@puts_1584_{ Var.V.name = "R1_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_7->(Ret(@puts_1584_{ Var.V.name = "R29_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_7->(Ret(@puts_1584_{ Var.V.name = "R30_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_7->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_8->(Ret(@puts_1584_{ Var.V.name = "VF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_12->(Ret(@puts_1584_{ Var.V.name = "ZF_12"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_25->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load21_1->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_8->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load22_1->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_8->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_8->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), _->⊥) + (CF_in->(Par(@puts_1584_{ Var.name = ("CF_in", 0); scope = (Var.Local "@puts_1584"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@puts_1584_{ Var.name = ("NF_in", 1); scope = (Var.Local "@puts_1584"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@puts_1584_{ Var.name = ("R0_in", 2); scope = (Var.Local "@puts_1584"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@puts_1584_{ Var.name = ("R1_in", 3); scope = (Var.Local "@puts_1584"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@puts_1584_{ Var.name = ("R29_in", 4); scope = (Var.Local "@puts_1584"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@puts_1584_{ Var.name = ("R30_in", 5); scope = (Var.Local "@puts_1584"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@puts_1584)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@puts_1584_{ Var.name = ("VF_in", 7); scope = (Var.Local "@puts_1584"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@puts_1584_{ Var.name = ("ZF_in", 8); scope = (Var.Local "@puts_1584"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), _->⊥) + (CF_in->(Par(@main_1876_{ Var.name = ("CF_in", 8); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@main_1876_{ Var.name = ("NF_in", 9); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@main_1876_{ Var.name = ("R0_in", 10); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@main_1876_{ Var.name = ("R1_in", 11); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@main_1876_{ Var.name = ("R29_in", 12); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@main_1876_{ Var.name = ("R30_in", 13); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@main_1876_{ Var.name = ("VF_in", 15); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@main_1876_{ Var.name = ("ZF_in", 16); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_out->(Ret(@puts_1584_{ Var.name = ("CF_8", 120); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_out->(Ret(@puts_1584_{ Var.name = ("NF_8", 121); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_out->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_out->(Ret(@puts_1584_{ Var.name = ("R1_7", 123); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_out->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_out->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_out->(Ret(@puts_1584_{ Var.name = ("R31_7", 126); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), VF_out->(Ret(@puts_1584_{ Var.name = ("VF_8", 127); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_out->(Ret(@puts_1584_{ Var.name = ("ZF_12", 128); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_1->(Par(@main_1876_{ Var.name = ("CF_in", 8); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_1->(Par(@main_1876_{ Var.name = ("NF_in", 9); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_1->(Par(@main_1876_{ Var.name = ("R0_in", 10); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_1->(Par(@main_1876_{ Var.name = ("R1_in", 11); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_1->(Par(@main_1876_{ Var.name = ("R29_in", 12); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_1->(Par(@main_1876_{ Var.name = ("R30_in", 13); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_1->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_1->(Par(@main_1876_{ Var.name = ("VF_in", 15); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_1->(Par(@main_1876_{ Var.name = ("ZF_in", 16); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), #4_1->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R31_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R29_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R0_2->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_3->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), R0_4->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_5->(Constant->⟦0x20040:bv64, 0x20040:bv64⟧, _->⊥), load18_1->(Loaded(load18_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_6->(Loaded(load18_1)->⊤, _->⊥), R0_7->(Loaded(load18_1)->⊤, _->⊥), #5_1->(Loaded(load18_1)->⊤, _->⊥), VF_2->(Loaded(load18_1)->⊤, _->⊥), CF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_2->(Loaded(load18_1)->⊤, _->⊥), NF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_3->(Loaded(load18_1)->⊤, _->⊥), ZF_4->(Loaded(load18_1)->⊤, _->⊥), ZF_5->(Ret(@puts_1584_{ Var.name = ("ZF_10", 108); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), VF_3->(Loaded(load18_1)->⊤, Ret(@puts_1584_{ Var.name = ("VF_7", 107); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R31_3->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.name = ("R31_6", 106); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_3->(Ret(@puts_1584_{ Var.name = ("R29_6", 104); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R1_2->(Loaded(load19_1)->⊤, Par(@main_1876_{ Var.name = ("R1_in", 11); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_3->(Ret(@puts_1584_{ Var.name = ("NF_7", 101); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), CF_3->(Loaded(load18_1)->⊤, Ret(@puts_1584_{ Var.name = ("CF_7", 100); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_8->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_9->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_2->(Constant->⟦0x7d0:bv64, 0x7d0:bv64⟧, _->⊥), CF_4->(Ret(@puts_1584_{ Var.name = ("CF_4", 71); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_4->(Ret(@puts_1584_{ Var.name = ("NF_4", 72); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_10->(Ret(@puts_1584_{ Var.name = ("R0_10", 73); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_3->(Ret(@puts_1584_{ Var.name = ("R1_3", 74); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_4->(Ret(@puts_1584_{ Var.name = ("R29_4", 75); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_3->(Ret(@puts_1584_{ Var.name = ("R30_3", 76); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_4->(Ret(@puts_1584_{ Var.name = ("R31_4", 77); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_4->(Ret(@puts_1584_{ Var.name = ("VF_4", 78); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_6->(Ret(@puts_1584_{ Var.name = ("ZF_6", 79); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_11->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_12->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load20_1->(Loaded(load20_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_13->(Loaded(load20_1)->⊤, _->⊥), #6_1->(Loaded(load20_1)->⊤, _->⊥), VF_5->(Loaded(load20_1)->⊤, _->⊥), CF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_7->(Loaded(load20_1)->⊤, _->⊥), NF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_8->(Loaded(load20_1)->⊤, _->⊥), ZF_9->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), VF_6->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), R31_5->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.name = ("R31_4", 77); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_5->(Ret(@puts_1584_{ Var.name = ("R29_4", 75); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R1_4->(Ret(@puts_1584_{ Var.name = ("R1_3", 74); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, Par(@main_1876_{ Var.name = ("R1_in", 11); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_6->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), CF_6->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), R0_14->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_15->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_4->(Constant->⟦0x7a0:bv64, 0x7a0:bv64⟧, _->⊥), CF_7->(Ret(@puts_1584_{ Var.name = ("CF_7", 100); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_7->(Ret(@puts_1584_{ Var.name = ("NF_7", 101); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_16->(Ret(@puts_1584_{ Var.name = ("R0_16", 102); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_5->(Ret(@puts_1584_{ Var.name = ("R1_5", 103); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_6->(Ret(@puts_1584_{ Var.name = ("R29_6", 104); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_5->(Ret(@puts_1584_{ Var.name = ("R30_5", 105); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_6->(Ret(@puts_1584_{ Var.name = ("R31_6", 106); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_7->(Ret(@puts_1584_{ Var.name = ("VF_7", 107); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_10->(Ret(@puts_1584_{ Var.name = ("ZF_10", 108); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_17->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_18->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load19_1->(Loaded(load19_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_19->(Loaded(load19_1)->⊤, _->⊥), R1_6->(Loaded(load19_1)->⊤, _->⊥), R0_20->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_21->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), ZF_11->(Loaded(load20_1)->⊤, _->⊥), R0_22->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_23->(Constant->⟦0x828:bv64, 0x828:bv64⟧, _->⊥), R30_6->(Constant->⟦0x7f4:bv64, 0x7f4:bv64⟧, _->⊥), CF_8->(Ret(@puts_1584_{ Var.name = ("CF_8", 120); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_8->(Ret(@puts_1584_{ Var.name = ("NF_8", 121); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_24->(Ret(@puts_1584_{ Var.name = ("R0_24", 122); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_7->(Ret(@puts_1584_{ Var.name = ("R1_7", 123); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_7->(Ret(@puts_1584_{ Var.name = ("R29_7", 124); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_7->(Ret(@puts_1584_{ Var.name = ("R30_7", 125); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_7->(Ret(@puts_1584_{ Var.name = ("R31_7", 126); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_8->(Ret(@puts_1584_{ Var.name = ("VF_8", 127); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_12->(Ret(@puts_1584_{ Var.name = ("ZF_12", 128); scope = (Var.Local "@main_1876"); typ = bv1; + tags = Var.None })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_25->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load21_1->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_8->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load22_1->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_8->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_8->(Ret(@puts_1584_{ Var.name = ("R31_7", 126); scope = (Var.Local "@main_1876"); typ = bv64; + tags = Var.None })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), _->⊥) diff --git a/test/lang/test_expr_eval_qcheck.ml b/test/lang/test_expr_eval_qcheck.ml index df87dcf6..41e59a4d 100644 --- a/test/lang/test_expr_eval_qcheck.ml +++ b/test/lang/test_expr_eval_qcheck.ml @@ -159,7 +159,8 @@ let check_smt = let query = "(set-logic QF_BV)\n(set-option :print-success true)\n" ^ Sexp.to_string - (Expr_smt.SMTLib2.add_assert check_p Expr_smt.SMTLib2.empty |> fst) + (Expr_smt.SMTLib2.add_assert check_p (Expr_smt.SMTLib2.empty ()) + |> fst) ^ "\n(exit)" in check_success_smt query diff --git a/test/lang/test_interp.ml b/test/lang/test_interp.ml index 7db229b7..535857cc 100644 --- a/test/lang/test_interp.ml +++ b/test/lang/test_interp.ml @@ -22,7 +22,6 @@ let%expect_test "fold_block" = (); [%expect {| - Warn: global undeclared $mem assuming mutable unshared PC= test::Return Stack diff --git a/test/lang/test_stmt.ml b/test/lang/test_stmt.ml index 0c46d2e7..0b724e14 100644 --- a/test/lang/test_stmt.ml +++ b/test/lang/test_stmt.ml @@ -4,15 +4,16 @@ open Lang.Common open Expr let%expect_test "frees" = + let v = Var.mk_gen ~scope:`Local () in let s = Instr_Assign { al = [ - ( Var.create "v1" Types.Boolean, - BasilExpr.rvar @@ Var.create "v2" Types.Boolean ); - ( Var.create "v3" Types.Boolean, - BasilExpr.rvar @@ Var.create "v4" Types.Boolean ); + ( v.with_name "v1" Types.Boolean, + BasilExpr.rvar @@ v.with_name "v2" Types.Boolean ); + ( v.with_name "v3" Types.Boolean, + BasilExpr.rvar @@ v.with_name "v4" Types.Boolean ); ]; attrib = Attrib.empty; } @@ -54,8 +55,6 @@ let%expect_test "fold_block" = (); [%expect {| - Warn: global undeclared $stack assuming mutable unshared - Warn: global undeclared $mem assuming mutable unshared $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64, 0xfffffffffffffffc:bv64) extract(32,0, R0_in:bv64) 32 var load45_1:bv32 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64, diff --git a/test/transforms/test_aslp.ml b/test/transforms/test_aslp.ml index 2d288a32..fc026b78 100644 --- a/test/transforms/test_aslp.ml +++ b/test/transforms/test_aslp.ml @@ -3,7 +3,7 @@ open Common open Transforms.Aslp let%expect_test "lift empty" = - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in let x = lift_code_block (module I) ~address:(Bitvec.of_int ~size:64 0x2000) [] @@ -12,7 +12,7 @@ let%expect_test "lift empty" = [%expect {| |}] let%expect_test "lift: add x1, x2, x3, lsl #4" = - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in let x = lift_opcode @@ -26,15 +26,15 @@ let%expect_test "lift: add x1, x2, x3, lsl #4" = (Leaf { Aslp_state.assume = true; stmts = - [var var_0:bv64 := 0x0:bv64; var var_0:bv64 := $R2; - var var_1:bv64 := 0x0:bv64; var var_1:bv64 := $R3; - $R1:bv64 := bvadd(var_0:bv64, bvshl(var_1:bv64, 0x4:bv12)); + [var v:bv64 := 0x0:bv64; var v:bv64 := $R2; var v_1:bv64 := 0x0:bv64; + var v_1:bv64 := $R3; + $R1:bv64 := bvadd(v:bv64, bvshl(v_1:bv64, 0x4:bv12)); (var BranchTaken:bool := false, $PC:bv64 := 0x2004:bv64)]; pc_assign = (Some 0x2004:bv64) }) |}] let%expect_test "lift 2x: mov x1, #0xabcd" = - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in let x = lift_code_block @@ -60,7 +60,7 @@ let%expect_test "lift 2x: mov x1, #0xabcd" = |}] let%expect_test "lift: b.eq #1024" = - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in let x = lift_opcode @@ -92,7 +92,7 @@ let%expect_test "lift: b.eq #1024" = |}] let%expect_test "lift: b #16" = - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in let x = lift_opcode @@ -106,9 +106,9 @@ let%expect_test "lift: b #16" = (Leaf { Aslp_state.assume = true; stmts = - [var var_0:bv64 := 0x0:bv64; var var_0:bv64 := $R2; - var var_1:bv64 := 0x0:bv64; var var_1:bv64 := $R3; - $R1:bv64 := bvadd(var_0:bv64, bvshl(var_1:bv64, 0x4:bv12)); + [var v:bv64 := 0x0:bv64; var v:bv64 := $R2; var v_1:bv64 := 0x0:bv64; + var v_1:bv64 := $R3; + $R1:bv64 := bvadd(v:bv64, bvshl(v_1:bv64, 0x4:bv12)); (var BranchTaken:bool := false, $PC:bv64 := 0x2004:bv64)]; pc_assign = (Some 0x2004:bv64) }) |}] @@ -165,18 +165,18 @@ proc @main() -> () { } goto (%block); ]; block %block { .asm = "stp x29, x30, [sp, #-0x20]!" } [ - var var:bv64 := 0x0:bv64; - var var:bv64 := $SP; + var v:bv64 := 0x0:bv64; + var v:bv64 := $SP; $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0xffffffffffffffe0:bv64) $R29 8; $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, 0xffffffffffffffe0:bv64), 0x8:bv64) $R30 8; - $SP:bv64 := bvadd(var:bv64, 0xffffffffffffffe0:bv64); + $SP:bv64 := bvadd(v:bv64, 0xffffffffffffffe0:bv64); (var BranchTaken:bool := false, $PC:bv64 := 0x40080c:bv64); goto (%block_1); ]; block %block_1 { .asm = "mov x29, sp" } [ - var var_1:bv64 := 0x0:bv64; + var v_1:bv64 := 0x0:bv64; $R29:bv64 := bvadd($SP, 0x0:bv64); (var BranchTaken:bool := false, $PC:bv64 := 0x400810:bv64); goto (%block_2); @@ -192,10 +192,10 @@ proc @main() -> () { } goto (%block_4); ]; block %block_4 { .asm = "ldrsw x0, [sp, #0x1c]" } [ - var var_2:bv32 := 0x0:bv32; - $mem:(bv64->bv8) := load le var_3:bv4 bvadd($SP, 0x1c:bv64) 4; - var var_2:bv32 := var_3:bv4; - $R0:bv64 := zero_extend(0, sign_extend(32, var_2:bv32)); + var v_2:bv32 := 0x0:bv32; + $mem:(bv64->bv8) := load le v_3:bv4 bvadd($SP, 0x1c:bv64) 4; + var v_2:bv32 := v_3:bv4; + $R0:bv64 := zero_extend(0, sign_extend(32, v_2:bv32)); (var BranchTaken:bool := false, $PC:bv64 := 0x40081c:bv64); goto (%block_5); ]; @@ -209,10 +209,10 @@ proc @main() -> () { } block %ret_1 [ return; ] ]; var $SP:bv64; - var $R0:bv64; - var $R1:bv64; var $R29:bv64; var $R30:bv64; + var $R0:bv64; + var $R1:bv64; prog entry @main; |}] @@ -285,8 +285,8 @@ proc @Sqrt() -> () { } block %Sqrt_code_3 [ assume eq(0x4007fc:bv64, $PC); goto (%ret); ]; block %ret [ return; ] ]; - var $PSTATE_N:bv1; var $PSTATE_V:bv1; + var $PSTATE_N:bv1; prog entry @Sqrt; |}] @@ -339,8 +339,8 @@ proc @main() -> () { } goto (%block); ]; block %block { .asm = "mov xzr, xzr" } [ - var var:bv64 := 0x0:bv64; - var var_1:bv64 := 0x0:bv64; + var v:bv64 := 0x0:bv64; + var v_1:bv64 := 0x0:bv64; (var BranchTaken:bool := false, $PC:bv64 := 0x400810:bv64); goto (%ret_1); ]; diff --git a/test/transforms/test_aslp_ibi.ml b/test/transforms/test_aslp_ibi.ml index 0ef01457..985bb434 100644 --- a/test/transforms/test_aslp_ibi.ml +++ b/test/transforms/test_aslp_ibi.ml @@ -78,7 +78,7 @@ let%expect_test "diamond bfs" = let%expect_test "nested diamonds" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in I.bincaml_set_address (Bitvec.of_int ~size:64 0xfaf); let branch1 = I.f_gen_branch (I.f_gen_bool_lit true) in @@ -157,7 +157,7 @@ let%expect_test "nested diamonds" = let%expect_test "sequential diamonds" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in ( guard @@ fun () -> I.bincaml_set_address (Bitvec.of_int ~size:64 0xfaf); @@ -208,7 +208,7 @@ let%expect_test "sequential diamonds" = let%expect_test "pc before branch" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in guard (fun () -> I.bincaml_set_address (Bitvec.of_int ~size:64 0xbadbad); @@ -254,7 +254,7 @@ let%expect_test "pc before branch" = let%expect_test "skipped merge context when going to outer merge" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in I.bincaml_set_address (Bitvec.of_int ~size:64 0xfaf); let outer = I.f_gen_branch (I.f_gen_bool_lit true) in @@ -309,7 +309,7 @@ let%expect_test "skipped merge context when going to outer merge" = let%expect_test "skipped merge context when going to outer branch" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in I.bincaml_set_address (Bitvec.of_int ~size:64 0xfaf); let outer = I.f_gen_branch (I.f_gen_bool_lit true) in @@ -371,7 +371,7 @@ let%expect_test "skipped merge context when going to outer branch" = let%expect_test "pathological: referencing old branch with intervening gen_branch" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in guard (fun () -> I.bincaml_set_address (Bitvec.of_int ~size:64 0xfaf); @@ -401,7 +401,7 @@ let%expect_test let%expect_test "pathological: sequential diamonds, then going back into the first one" = let make_call = make_call () in - let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ())) + let module I = (val Bincaml_ibi.from_generator (Aslp_lexpr.empty_aslp_ids ())) in ( guard @@ fun () -> begin