Phil/isel jmp3 (#162)

Initial pass at supporting jmps of various kinds in the minizinc instruction selector.

bap-vibes/src/arm_selector.ml

@@ -708,7 +708,7 @@ module ARM_ops = struct
 end
 
 (* We assume that a block is always created *)
-let ir (t : arm_eff) : Ir.t KB.t =
+let ir_of_arm_eff (t : arm_eff) : Ir.t KB.t =
   if not (List.is_empty t.current_data && List.is_empty t.current_ctrl)
   then Err.(fail @@ Other "Arm_selector.ir: expected empty data and ctrl")
   else KB.return @@ Ir.add_in_vars t.other_blks
@@ -1089,7 +1089,7 @@ struct
       ~(is_thumb : bool)
       ~(argument_tids : Tid.Set.t) : Ir.t KB.t =
     let* bs = select_blks bs ~patch ~is_thumb ~argument_tids in
-    ir bs
+    ir_of_arm_eff bs
 
 end
 
@@ -1099,8 +1099,10 @@ module Isel = struct
     String.Map.of_alist_exn [
     "add", binop PLUS (ARM_ops.Ops.add false);
     "mov", mov (ARM_ops.Ops.mov false);
-    "str", store;
-    "ld",  load
+    "str", store (Ir.Opcode.create "str");
+    "ld",  load (Ir.Opcode.create "ld");
+    "b",   goto (Ir.Opcode.create "b");
+    "null_jump", null_jump (Ir.Opcode.create "b")
   ]
 
 end

bap-vibes/src/arm_selector.mli

@@ -45,7 +45,7 @@ val is_arm_or_thumb : Theory.language -> bool KB.t
 
 (** Extracts the concrete [Ir.t] from the abstract [arm_eff]
     representation. *)
-val ir : arm_eff -> Ir.t KB.t
+val ir_of_arm_eff : arm_eff -> Ir.t KB.t
 
 (** Performs various ARM specific simplifications of a given [ir]
    program, aimed mostly to conserve space. *)

bap-vibes/src/bir_passes.ml

@@ -472,7 +472,7 @@ let to_linear_ssa
   let* sub = Helper.create_sub blks in
   sub |> Sub.ssa |> Linear_ssa.transform ~patch:(Some patch)
 
-let run (patch : Data.Patch.t) : t KB.t =
+let run (patch : Data.Patch.t) ~(merge_adjacent : bool) : t KB.t =
   let* code = Data.Patch.get_bir patch in
   let info_str = Format.asprintf "\nPatch: %a\n\n%!" KB.Value.pp code in
   Events.(send @@ Info info_str);
@@ -496,6 +496,6 @@ let run (patch : Data.Patch.t) : t KB.t =
   let ir = Opt.apply ir in
   let* ir = Subst.substitute tgt hvars ir in
   let* ir = Shape.reorder_blks ir in
-  let ir = Opt.merge_adjacent ir in
+  let ir = if merge_adjacent then Opt.merge_adjacent ir else ir in
   let+ ir = to_linear_ssa patch ir in
   {ir; exclude_regs; argument_tids}

bap-vibes/src/bir_passes.mli

@@ -61,4 +61,4 @@ end
 (** [run patch] creates the BIR from [patch], then applies a series of
     transformations to it. The resulting code is then ready to be handed
     off to the instruction selector. *)
-val run : Data.Patch.t -> t KB.t  
+val run : Data.Patch.t -> merge_adjacent:bool -> t KB.t

bap-vibes/src/compiler.ml

@@ -40,7 +40,7 @@ let create_assembly (solver : Ir.t -> (Ir.t * Minizinc.sol) KB.t)
 let create_vibes_ir
     (patch : Data.Patch.t)
     (isel_model_filepath : string option) : (Ir.t * String.Set.t) KB.t =
-  let* {ir; exclude_regs; argument_tids} = Bir_passes.run patch in
+  let* {ir; exclude_regs; argument_tids} = Bir_passes.run patch ~merge_adjacent:(Option.is_none isel_model_filepath) in
   Events.(send @@ Info "Transformed BIR\n");
   Events.(send @@ Info (
       List.map ir ~f:(fun blk -> Format.asprintf "    %a" Blk.pp blk) |>

bap-vibes/src/ir.ml

@@ -180,7 +180,7 @@ let empty_op () : operation =
   { id = create_id ();
     lhs = [];
     opcodes = [];
-    optional = true;
+    optional = false;
     operands = []
   }
 
@@ -540,47 +540,39 @@ end
 
 module OpSet = Set.Make(Operand)
 
-let is_defined (defs : OpSet.t) (v : operand) : bool =
-  let vars =
-    match v with
-    | Var v | Void v -> v.temps
-    | _ -> []
-  in
-  OpSet.fold defs ~init:false
-    ~f:(fun is_def o ->
-        match o with
-        | Var v | Void v ->
-          let def_vars = v.temps in
-          let v_set = Var.Set.of_list vars in
-          let def_set = Var.Set.of_list def_vars in
-          let b = Var.Set.is_empty (Var.Set.inter v_set def_set) in
-          (not b) || is_def
-        | _ -> is_def)
-
 let add_in_vars_blk (b : blk) : blk =
   let ops = b.data @ b.ctrl in
-  let collect_vars_op_list l =
-    List.fold l ~init:OpSet.empty
-      ~f:(fun set o ->
-          match o with
-          | Var _ | Void _ -> OpSet.add set o
-          | _ -> set)
+  (* We need to remember whether temps are Var or Void. We use a boolean flag for this in
+     a Map with domain of temps. *)
+  let collect_temps (l : operand list) temp_map : bool Var.Map.t =
+      let add_temps temp_map (temps : Var.t list) (is_var : bool) =
+         List.fold temps ~init:temp_map ~f:(fun temp_map temp ->
+          Var.Map.set temp_map ~key:temp ~data:is_var
+          )
+      in
+      List.fold l ~init:temp_map
+        ~f:(fun temp_map o ->
+            match o with
+            | Var op_var -> add_temps temp_map op_var.temps true
+            | Void op_var -> add_temps temp_map op_var.temps false
+            | _ -> temp_map)
+  in
+  let lhs_temp_map = List.fold ops ~init:Var.Map.empty
+    ~f:(fun temp_map o -> collect_temps o.lhs temp_map)
   in
-  (* Simultaneously collect defined and undefined vars *)
-  let _, undefined =
-    List.fold ops ~init:(OpSet.empty, OpSet.empty)
-      ~f:(fun (defined, undefined) o ->
-          let undef = collect_vars_op_list o.operands in
-          let undef = OpSet.filter undef
-              ~f:(fun o -> not @@ is_defined defined o)
-          in
-          let undef = OpSet.filter undef
-              ~f:(fun o -> not @@ is_defined undefined o)
-          in
-          let def = collect_vars_op_list o.lhs in
-          OpSet.union defined def, OpSet.union undefined undef)
+  let rhs_temp_map = List.fold ops ~init:Var.Map.empty
+    ~f:(fun temp_map o -> collect_temps o.operands temp_map)
   in
-  let ins = OpSet.to_list undefined |> List.map ~f:freshen_operand
+  (* The indefined temporaries are those that are in right hand sides, 
+     but not left hand sides *)
+  let undef_temps =
+      let lhs_temps = Var.Map.keys lhs_temp_map |> Var.Set.of_list in
+      let rhs_temps = Var.Map.keys rhs_temp_map |> Var.Set.of_list in
+      Var.Set.diff rhs_temps lhs_temps |> Var.Set.to_list in
+  let ins = List.map undef_temps ~f:(fun temp ->
+    let op_var = (simple_var temp) in
+    (* Since set difference, temp should be in rhs_temps, therefore find_exn is ok *)
+    if Var.Map.find_exn rhs_temp_map temp then Var op_var else Void op_var)
   in
   (* We add dummy operation with no instructions and as lhs all the
      [ins] variables *)

bap-vibes/src/ir.mli

@@ -206,6 +206,7 @@ val op_var_exn : operand -> op_var
 
 (** various printer functions *)
 val pretty_operand : operand -> string
+val pretty_blk : blk -> string
 val pretty_ir : t -> string
 (* Alias of pretty_ir *)
 val to_string : t -> string