Memory allocation intrinsics

.gitignore

@@ -7,4 +7,5 @@ trace.json
 *.dot
 **/*.dot
 
-.vscode/
+.vscode/
+.helix/

lib/fe/BasilIR.cf

@@ -164,7 +164,7 @@ separator nonempty NamedCallArg "," ;
 CallParams_Exprs . CallParams ::= [Expr];
 CallParams_Named . CallParams ::= [NamedCallArg];
 
-Stmt_DirectCall . Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ;
+Stmt_DirectCall   . Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ;
 Stmt_IndirectCall . Stmt ::= "indirect" "call" Expr ;
 
 Stmt_Assume . Stmt ::= "assume" Expr ;

lib/lang/stmt.ml

@@ -23,19 +23,20 @@ module Intrinsic = struct
     | "@_malloc" -> Some Malloc
     | "@_calloc" -> Some Calloc
     | "@_free" -> Some Free
-    | "@_allcoa" -> Some AllocStack
+    | "@_alloca" -> Some AllocStack
     | "@_free_alloca" -> Some FreeStack
     | _ -> None
 
-  let pretty e =
-    (match e with
-      | Havoc -> "@_havoc"
-      | Malloc -> "@_malloc"
-      | Calloc -> "@_calloc"
-      | Free -> "@_free"
-      | AllocStack -> "@_allcoa"
-      | FreeStack -> "@_free_alloca")
-    |> Containers_pp.text
+  let to_string e =
+    match e with
+    | Havoc -> "@_havoc"
+    | Malloc -> "@_malloc"
+    | Calloc -> "@_calloc"
+    | Free -> "@_free"
+    | AllocStack -> "@_alloca"
+    | FreeStack -> "@_free_alloca"
+
+  let pretty = Containers_pp.text % to_string
 end
 
 let show_endian = function `Big -> "be" | `Little -> "le"

lib/passes.ml

@@ -290,6 +290,14 @@ module PassManager = struct
          cleaning stack address uses. Assumes SSA.";
     }
 
+  let intrin_call =
+    {
+      name = "intrin-call";
+      apply = Prog Transforms.Intrin_call.transform;
+      doc =
+        "Replaces special calls like malloc and free with intrin calls instead";
+    }
+
   let simp =
     {
       name = "simplify";
@@ -337,6 +345,7 @@ module PassManager = struct
       read_uninit false;
       read_uninit true;
       sssa;
+      intrin_call;
       sva;
       full_ssa;
       type_check;

lib/transforms/dune

@@ -14,6 +14,7 @@
   memory_specification
   function_summaries
   boogie_prepass
+  intrin_call
   gamma_vars
   const_prop
   linear_copy)

lib/transforms/intrin_call.ml

@@ -0,0 +1,97 @@
+open Bincaml_util.Common
+open Lang
+open Expr
+
+let string_to_intrin =
+  Stmt.Intrinsic.(
+    function
+    | "@malloc" | "@#malloc" | "@_malloc" -> Malloc
+    | "@calloc" | "@_calloc" | "@zmalloc" -> Calloc
+    | "@alloca" | "@_alloca" -> AllocStack
+    | "@free" | "@#free" | "@_free" -> Free
+    | _ -> failwith "Unreachable")
+
+let transform_proc proc prog =
+  let replace_call (stmt : Program.stmt) : Program.stmt Iter.t =
+    match stmt with
+    | Stmt.Instr_Call { procid; lhs; args; attrib } -> (
+        match ID.name procid with
+        | ( "@malloc" | "@#malloc" | "@calloc" | "@alloca" | "@_malloc"
+          | "@_calloc" | "@_alloca" ) as name ->
+            let modifies =
+              List.filter
+                (fun var ->
+                  not @@ String.starts_with (Var.name var) ~prefix:"R0")
+                (Procedure.specification (Program.proc prog procid))
+                  .modifies_globs
+            in
+            let lhs =
+              StringMap.filter
+                (fun name _ -> String.starts_with name ~prefix:"R0")
+                lhs
+              |> StringMap.values |> List.of_iter
+            in
+            let args =
+              StringMap.filter
+                (fun name _ -> String.starts_with name ~prefix:"R0")
+                args
+              |> StringMap.values |> List.of_iter
+            in
+            Iter.doubleton
+              (Stmt.Instr_IntrinCall
+                 { name = string_to_intrin name; lhs; args; attrib })
+              (Stmt.Instr_IntrinCall
+                 {
+                   name = Stmt.Intrinsic.Havoc;
+                   lhs = modifies;
+                   args = [];
+                   attrib = Attrib.empty;
+                 })
+        | ("@#free" | "@free" | "@_free") as name ->
+            let modifies =
+              (Procedure.specification (Program.proc prog procid))
+                .modifies_globs
+            in
+            let lhs = StringMap.values lhs |> List.of_iter in
+            let args =
+              StringMap.filter
+                (fun name _ -> String.starts_with name ~prefix:"R0")
+                args
+              |> StringMap.values |> List.of_iter
+            in
+            Iter.doubleton
+              (Stmt.Instr_IntrinCall
+                 { name = string_to_intrin name; lhs; args; attrib })
+              (Stmt.Instr_IntrinCall
+                 {
+                   name = Stmt.Intrinsic.Havoc;
+                   lhs = modifies;
+                   args = [];
+                   attrib = Attrib.empty;
+                 })
+        | ("@#havoc" | "@havoc" | "@_havoc") as name ->
+            let modifies =
+              (Procedure.specification (Program.proc prog procid))
+                .modifies_globs
+            in
+            let lhs = StringMap.values lhs |> List.of_iter in
+            Iter.doubleton
+              (Stmt.Instr_IntrinCall
+                 { name = string_to_intrin name; lhs; args = []; attrib })
+              (Stmt.Instr_IntrinCall
+                 {
+                   name = Stmt.Intrinsic.Havoc;
+                   lhs = modifies;
+                   args = [];
+                   attrib = Attrib.empty;
+                 })
+        | _ -> Iter.singleton stmt)
+    | _ -> Iter.singleton stmt
+  in
+  let open BasilExpr in
+  Procedure.map_blocks_topo_fwd
+    (fun _ b -> Block.flat_map ~phi:id replace_call b)
+    proc
+
+let transform (prog : Program.t) =
+  Program.map_procedures (fun pid proc -> transform_proc proc prog) prog

lib/transforms/memory_specification.ml

@@ -168,11 +168,8 @@ let transform_proc entry _ (p : Program.proc) =
     match name with
     | "@main" -> transform_main p
     | e when String.equal entry e -> transform_main p
-    | "@malloc" -> transform_malloc p
-    | "@free" -> transform_free p
-    | "@#malloc" -> transform_malloc p
-    | "@zmalloc" -> transform_malloc p
-    | "@#free" -> transform_free p
+    | "@malloc" | "@#malloc" | "@zmalloc" -> transform_malloc p
+    | "@free" | "@#free" -> transform_free p
     | _ -> p
 
 let transform (p : Program.t) =

lib/transforms/type_check.ml

@@ -263,6 +263,49 @@ let type_check stmt_id block_id expr =
   in
   BasilExpr.cata type_error_alg expr
 
+let check_intrin_call (intrin_call : Stmt.Intrinsic.t) args params =
+  Stmt.Intrinsic.(
+    match intrin_call with
+    | Havoc -> (
+        match params with
+        | [] -> []
+        | _ -> [ TypeError { text = "Havoc should not have args" } ])
+    | Malloc | AllocStack | Calloc -> (
+        match (args, params) with
+        | [ size ], [ ptr ] ->
+            let err =
+              if Types.leq (Bitvector 64) (BasilExpr.type_of ptr) then []
+              else
+                [
+                  TypeError
+                    { text = "Wrong type of arg in " ^ to_string intrin_call };
+                ]
+            in
+            if Types.equal (Bitvector 64) (Var.typ size) then err
+            else
+              TypeError
+                { text = "Wrong type of arg in " ^ to_string intrin_call }
+              :: err
+        | _ ->
+            [
+              TypeError
+                { text = "Wrong amount of args in " ^ to_string intrin_call };
+            ])
+    | Free | FreeStack -> (
+        match (args, params) with
+        | [ ptr ], [] ->
+            if Types.leq (Bitvector 64) (Var.typ ptr) then []
+            else
+              [
+                TypeError
+                  { text = "Wrong type of arg in " ^ to_string intrin_call };
+              ]
+        | _ ->
+            [
+              TypeError
+                { text = "Wrong amount of args in " ^ to_string intrin_call };
+            ]))
+
 let check_stmt_types (stmt : Program.stmt) (pt : Program.t) stmt_id block_id =
   let type_err fmt = type_err fmt stmt_id block_id in
   let expect_equal msg a b (s : type_error list) =
@@ -273,7 +316,6 @@ let check_stmt_types (stmt : Program.stmt) (pt : Program.t) stmt_id block_id =
   in
   let type_check = type_check stmt_id block_id in
   match stmt with
-  | Stmt.Instr_IntrinCall _ -> []
   | Stmt.Instr_Assign { al } ->
       al
       |> List.fold_left
@@ -386,6 +428,7 @@ let check_stmt_types (stmt : Program.stmt) (pt : Program.t) stmt_id block_id =
              output)
       in
       params_check
+  | Stmt.Instr_IntrinCall { name; lhs; args } -> check_intrin_call name lhs args
 
 let check_block prog (id, b) =
   Block.stmts_iter b

test/cram/dune

@@ -18,6 +18,7 @@
   ssa-multi-deps.il
   memassign.il
   ptrrec1.il
+  intrin_before.il
   ../../examples/sqrt.il
   ../../examples/irreducible_loop_1.il
   ../../examples/cat.il
@@ -47,6 +48,8 @@
   ll_spec.sexp
   repeated_ssa.il
   repeated_ssa.sexp
+  intrin_call.sexp
+  ../../examples/memory/malloc_free.il
   ../../bin/main.exe))
 
 (cram

test/cram/intrin_before.il

@@ -0,0 +1,25 @@
+proc @main_4196164(R0_in:bv64, R10_in:bv64, R11_in:bv64, R12_in:bv64, R13_in:bv64,
+   R14_in:bv64, R15_in:bv64, R16_in:bv64, R17_in:bv64, R18_in:bv64, R1_in:bv64,
+   R29_in:bv64, R2_in:bv64, R30_in:bv64, R31_in:bv64, R3_in:bv64, R4_in:bv64,
+   R5_in:bv64, R6_in:bv64, R7_in:bv64, R8_in:bv64, R9_in:bv64, _PC_in:bv64)
+   -> (R0_out:bv64, R1_out:bv64) { .address = 4196164; .name = "main";
+    .returnBlock = "main_return" }
+
+[
+   block %main_entry [
+     var as:bv64 := 0x32:bv64;
+     (var x_2:bv64, var x_3:bv64, var addr:bv64):= call @_havoc();
+     (var ptr0:bv64):= call @_malloc(as:bv64);
+     (var ptr1:bv64):= call @_calloc(as:bv64);
+     call @_free(ptr0:bv64);
+     call @_free(ptr1:bv64);
+     (var stack_ptr:bv64):= call @_alloca(as:bv64);
+     call @_free_alloca(stack_ptr:bv64);
+     goto (%main_return);
+   ];
+   block %main_return [
+     (var R0_out:bv64 := 0x0:bv64, var R1_out:bv64 := 0x2a:bv64);
+     return;
+   ]
+];
+prog entry @main_4196164;

test/cram/intrin_call.sexp

@@ -0,0 +1,3 @@
+(load-il "../../examples/memory/malloc_free.il")
+(run-transforms "intrin-call")
+(dump-il "after.il")

test/cram/intrin_call.t

@@ -0,0 +1,63 @@
+  $ bincaml script intrin_call.sexp
+  (load-il ../../examples/memory/malloc_free.il)
+  (run-transforms intrin-call)
+  (dump-il after.il)
+  $ cat after.il
+  var observable $mem:(bv64->bv8);
+  var $stack:(bv64->bv8);
+  proc @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)
+     -> (R0_out:bv64, R17_out:bv64, R1_out:bv64, R29_out:bv64, R30_out:bv64) { .address = 2276;
+      .name = "main"; .returnBlock = "main_return" }
+    modifies $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $mem:(bv64->bv8), $stack:(bv64->bv8)
+
+  [
+     block %main_entry [
+       $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe0:bv64) R29_in:bv64 64;
+       $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe8:bv64) R30_in:bv64 64;
+       var Exp14__5_2_1:bv64 := load le $mem:(bv64->bv8) 0x20010:bv64 64;
+       assert true;
+       (var R0_3:bv64):= call @_malloc(0x1:bv64);
+       ($mem:(bv64->bv8), $stack:(bv64->bv8)):= call @_havoc();
+       goto (%phi_5);
+     ];
+     block %phi_5 [
+       $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xfffffffffffffff8:bv64) R0_3:bv64 64;
+       var Exp14__5_21_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xfffffffffffffff8:bv64) 64;
+       $mem:(bv64->bv8) := store le $mem:(bv64->bv8) Exp14__5_21_1:bv64 0x79:bv8 8;
+       var Exp14__5_22_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xfffffffffffffff8:bv64) 64;
+       var Exp14__5_1_1:bv64 := load le $mem:(bv64->bv8) 0x20028:bv64 64;
+       assert true;
+       call @_free(Exp14__5_22_1:bv64);
+       ($mem:(bv64->bv8), $stack:(bv64->bv8)):= call @_havoc();
+       goto (%phi_6);
+     ];
+     block %phi_6 [
+       var Exp16__5_24_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe0:bv64) 64;
+       var Exp18__5_25_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe8:bv64) 64;
+       goto (%main_return);
+     ];
+     block %main_return [
+       (var R0_out:bv64 := 0x0:bv64, var R17_out:bv64 := Exp14__5_1_1:bv64,
+        var R1_out:bv64 := 0x79:bv64, var R29_out:bv64 := Exp16__5_24_1:bv64,
+        var R30_out:bv64 := Exp18__5_25_1:bv64);
+       return;
+     ]
+  ];
+  proc @malloc(R0_in:bv64)  -> (R0_out:bv64) { .name = "malloc" }
+    modifies $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $mem:(bv64->bv8), $stack:(bv64->bv8)
+  ;
+  proc @#free(R0_in:bv64)  -> () { .name = "#free" }
+    modifies $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $mem:(bv64->bv8), $stack:(bv64->bv8)
+  ;
+  prog entry @main_2276;

test/cram/roundtrip.sexp

@@ -16,3 +16,6 @@
 (dump-il "ptrrec2.il")
 (load-il "ptrrec2.il")
 (dump-il "ptrrec3.il")
+
+(load-il "intrin_before.il")
+(dump-il "intrin_after.il")

test/cram/roundtrip.t

@@ -16,6 +16,8 @@
   (dump-il ptrrec2.il)
   (load-il ptrrec2.il)
   (dump-il ptrrec3.il)
+  (load-il intrin_before.il)
+  (dump-il intrin_after.il)
 
 The serialise -> parse serialise loop should be idempotent
 
@@ -84,6 +86,12 @@ Record and Pointer
   [1]
   $ diff ptrrec2.il ptrrec3.il
 
+Intrin Calls
+
+  $ diff intrin_before.il intrin_after.il
+  6a7
+  >   
+  [1]
 
 Examples Directory