Require variables be scoped from program/procedure allocators

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
     |}]

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

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 |}]

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) =

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 }

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,21 +46,21 @@ 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
     Some guard
   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

lib/lang/algsimp.ml

@@ -331,20 +331,21 @@ 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);
   let e = normalise e in
   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))
     |}]