Aslp transform + fixes

lib/gtirb/gfir_to_bincaml.ml

@@ -354,5 +354,6 @@ let module_to_ir_prog ir_cfg (m : Module.t) =
       (fun _ proc prog -> temp_proc_to_ir_proc all_blocks prog proc)
       procs prog
   in
+  let prog = Lang.Spec_modifies.set_modsets prog in
   let entry_proc = UUIDMap.find entry_proc procs in
   Lang.Program.set_entry_proc entry_proc.id prog

lib/invariants.ml

@@ -16,13 +16,15 @@ type t =
   | Params
   | LambdaLift
   | MemoryEncoding
+  | GTIRB_ARM
   | ReducibleLoops
       (** All loops are reducible. That is, there are no {i irreducible} loops.
       *)
 [@@deriving show { with_path = false }, eq, ord]
 
 let read s =
   match s with
+  | "GTIRB_ARM" -> GTIRB_ARM
   | "SSA" -> SSA
   | "DSA" -> DSA
   | "NoPhis" -> NoPhis

lib/lang/spec_modifies.ml

@@ -76,14 +76,17 @@ let set_modsets ?(add_only = false) prog =
         |> Iter.flat_map Expr.BasilExpr.free_vars_iter
         |> Iter.filter Var.is_global |> VarSet.of_iter
       in
+      let name_compare = fun a b -> String.compare (Var.name a) (Var.name b) in
       let captures_globs =
-        List.filter (not % Var.is_constant)
+        List.sort name_compare
+        @@ List.filter (not % Var.is_constant)
         @@ VarSet.elements @@ VarSet.union vs
         @@ VarSet.union exist_captures
         @@ VarSet.union read written
       in
       let modifies_globs =
-        VarSet.elements @@ VarSet.union exist_modifies written
+        List.sort name_compare @@ VarSet.elements
+        @@ VarSet.union exist_modifies written
       in
       let spec : (Var.t, Program.e) Procedure.proc_spec =
         Procedure.specification p

lib/loadir.ml

@@ -1523,7 +1523,7 @@ let concrete_prog_ast_of_channel ?input ?filename c =
   let lexbuf = Lexing.from_channel ~with_positions:true c in
   filename |> Option.iter (fun f -> Lexing.set_filename lexbuf f);
   try ParBasilIR.pModuleT LexBasilIR.token lexbuf
-  with ParBasilIR.Error -> raise (ILBParseError { input; lexbuf })
+  with _ -> raise (ILBParseError { input; lexbuf })
 
 let concrete_prog_ast_of_string ?input ?filename str =
   let open BasilIR in

lib/passes.ml

@@ -106,6 +106,15 @@ module PassManager = struct
       invariants = Invariants.presupposes [ SSA ];
     }
 
+  let aslp_semantics =
+    {
+      name = "aslp-semantics";
+      apply = Prog Transforms.Aslp.transform_program;
+      doc = "Add ASLP instsruction semantics after gtirb";
+      invariants =
+        Invariants.presupposes [ GTIRB_ARM ] ~invalidates:[ GTIRB_ARM ];
+    }
+
   let cse_elim =
     {
       name = "cse-elim";
@@ -442,6 +451,7 @@ module PassManager = struct
 
   let passes =
     [
+      aslp_semantics;
       lift_intrinsics_aarch64;
       hm_elaborate;
       chop_unreachable;

lib/script.ml

@@ -315,6 +315,7 @@ let load_gtirb st fname =
       let p =
         match p with
         | Ok e ->
+            let e = Program.set_attrib Invariants.(to_attrib [ GTIRB_ARM ]) e in
             Loader.Loadir.(
               Some
                 { prog = e; curr_proc = None; params_order = Hashtbl.create 0 })

lib/transforms/aslp/aslp.ml

@@ -73,11 +73,23 @@ let stmt_of_aarch64_intrin ?error :
   let args = Expr.BasilExpr.[ bvconst opcode; bvconst address ] in
   Stmt.Instr_IntrinCall { attrib; lhs = []; name = Aarch64Eval; args }
 
-(** Returns the Bincaml global variable representing heap memory. *)
+(** Returns the Bincaml global variable representing heap memory, declaring it
+    if it does not exist. *)
 let aarch64_mem_of_prog prog =
   Program.get_decl_by_name "$mem" prog |> function
-  | Some (Variable { binding }) -> binding
-  | _ -> failwith "aarch64_mem_of_prog: no $mem found"
+  | Some (Variable { binding }) -> (prog, binding)
+  | None ->
+      let mem =
+        Var.create "$mem" ~scope:Var.GlobalVarShared
+          Types.(Map (Bitvector 64, Bitvector 8))
+      in
+
+      let prog =
+        let attrib = Attrib.empty and classification = None in
+        Program.add_decl prog
+          (Program.Variable { binding = mem; attrib; classification })
+      in
+      (prog, mem)
 
 (** {1 Main Bincaml IR transformation functions} *)
 
@@ -170,13 +182,13 @@ let add_aarch64_global_declarations ?(add_all = false) prog =
     procedures within the given program.
 
     Also inserts global variable declarations for the architectural variables,
-    if not already present. *)
+    if not already present. Assumes it is running immediately after gtirb. *)
 let transform_program prog =
-  let memory = aarch64_mem_of_prog prog in
-
+  let prog, memory = aarch64_mem_of_prog prog in
   prog
   |> Program.map_procedures (fun _ -> transform_procedure ~memory)
   |> add_aarch64_global_declarations
+  |> Spec_modifies.set_modsets ~add_only:false
 
 (** {1 Supplementary transformation} *)
 

lib/transforms/aslp/aslp_state.ml

@@ -102,7 +102,7 @@ let empty_aslp_ids () =
     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
+  let local_id = ID.fresh ~name:"lv" local_ids %> ID.name in
   { local_id }
 
 (** {1 State manipulation functions} *)

lib/transforms/aslp/bincaml_ibi_make.ml

@@ -297,25 +297,31 @@ struct
       =
    fun _ -> failwith "f_gen_Elem_set"
 
-  (** [f_gen_Mem_set size address size acctype value] *)
+  (** [(f_gen_Mem_set size address size acctype value) : unit] emits an
+      instruction which stores value to memory. Value must have bit width equal
+      to size (bytes) in bits. *)
   let f_gen_Mem_set : bigint -> expr -> expr -> expr -> expr -> unit =
    fun size addr _ _acctype value ->
-    let addr = Stmt.Addr { addr; size = Z.to_int size; endian = `Little }
+    let size = 8 * Z.to_int size in
+    let addr = Stmt.Addr { addr; size; endian = `Little }
     and mem = S.bincaml_memory_var () in
     bincaml_internal_emit
       (Stmt.Instr_Store
          { attrib = Attrib.empty; lhs = mem; rhs = mem; value; addr })
 
-  (** [f_gen_Mem_read size address size acctype value] *)
+  (** [let lhs = f_gen_Mem_read size address size acctype value] emits a read
+      instruction reading a bitvector [size] (bytes) from the memory variable,
+      assigning it to variable [lhs]. Returns [lhs] as an expression). *)
   let f_gen_Mem_read : bigint -> expr -> expr -> expr -> expr =
    fun size addr _ _acctype ->
-    let addr = Stmt.Addr { addr; size = Z.to_int size; endian = `Little }
+    let size = 8 * Z.to_int size in
+    let addr = Stmt.Addr { addr; 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 lhs = Var.create name (Types.bv size) in
     bincaml_internal_emit
-      (Stmt.Instr_Load { attrib = Attrib.empty; lhs = mem; rhs; addr });
-    Expr.BasilExpr.rvar rhs
+      (Stmt.Instr_Load { attrib = Attrib.empty; lhs; rhs = mem; addr });
+    Expr.BasilExpr.rvar lhs
 
   let f_AtomicStart : unit -> unit = fun _ -> failwith "f_AtomicStart"
   let f_AtomicEnd : unit -> unit = fun _ -> failwith "f_AtomicEnd"
@@ -375,20 +381,30 @@ struct
   let f_gen_slt_bits : bigint -> expr -> expr -> expr =
    fun _ a b -> Expr.BasilExpr.binexp ~op:`BVSLT a b
 
+  let make_widths_equal a b =
+    let width a =
+      Expr.BasilExpr.type_of a |> Types.bit_width
+      |> Option.get_exn_or "expected bv argument to operator"
+    in
+    let wb = width b and wa = width a in
+    if wa = wb then b
+    else if wa > wb then Expr.BasilExpr.zero_extend ~n_prefix_bits:(wa - wb) b
+    else failwith "expected second shift argument to be equal or smaller"
+
   let f_gen_mul_bits : bigint -> expr -> expr -> expr =
    fun _ a b -> Expr.BasilExpr.applyintrin ~op:`BVMUL [ a; b ]
 
   let f_gen_append_bits : bigint -> bigint -> expr -> expr -> expr =
    fun _ _ a b -> Expr.BasilExpr.applyintrin ~op:`BVConcat [ a; b ]
 
   let f_gen_lsr_bits : bigint -> bigint -> expr -> expr -> expr =
-   fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVLSHR a b
+   fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVLSHR a (make_widths_equal a b)
 
   let f_gen_lsl_bits : bigint -> bigint -> expr -> expr -> expr =
-   fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVSHL a b
+   fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVSHL a (make_widths_equal a b)
 
   let f_gen_asr_bits : bigint -> bigint -> expr -> expr -> expr =
-   fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVASHR a b
+   fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVASHR a (make_widths_equal a b)
 
   (** [f_gen_replicate_bits operand_width num_replications operand
        num_replications] *)
@@ -408,7 +424,7 @@ struct
   (** [f_gen_slice x lo wd] *)
   let f_gen_slice : expr -> bigint -> bigint -> expr =
    fun x lo_incl wd ->
-    let hi_excl = Z.(to_int (lo_incl - wd)) and lo_incl = Z.to_int lo_incl in
+    let hi_excl = Z.(to_int (lo_incl + wd)) and lo_incl = Z.to_int lo_incl in
     Expr.BasilExpr.extract ~lo_incl ~hi_excl x
 
   (* {1 Floating point intrinsics} *)

test/cram/basicssa.t

@@ -52,10 +52,10 @@ Run on basic irreducible loop example
   var $ZF:bv1;
   proc @main_1876()  -> () { .address = 1876; .name = "main";
       .returnBlock = "main_basil_return_1" }
-    modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64,
-      $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1
-    captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64,
-      $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1
+    modifies $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64,
+      $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64,
+      $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8)
 
   [
      block %main_entry { .address = 1876 } [
@@ -158,10 +158,10 @@ Run on basic irreducible loop example
      block %main_basil_return_1 [ return; ]
   ];
   proc @puts_1584()  -> () { .address = 1584; .name = "puts" }
-    modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64,
-      $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1
-    captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64,
-      $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1
+    modifies $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64,
+      $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64,
+      $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8)
   ;
   prog entry @main_1876;