update action

UQ-PAC · Jul 24, 2024 · ef6e8d5 · ef6e8d5
1 parent e473055
commit ef6e8d5
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 11 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -53,7 +53,7 @@ jobs:
     - run: echo 'preparing nix shell environment'
 
     - run: dune build --profile release -j4
-    - run: echo ':gen A64 aarch64_* ocaml offlineASL' | OCAMLRUNPARAM=b dune exec asli
+    - run: echo ':gen A64 aarch64_* ocaml false offlineASL' | OCAMLRUNPARAM=b dune exec asli
 
     - run: dune build offlineASL -j4
 

diff --git a/libASL/rt_funs.ml b/libASL/rt_funs.ml
@@ -13,9 +13,9 @@ let rt_gen_int_lit      = FIdent("gen_int_lit", 0)     (* int -> int rt *)
 let rt_gen_slice        = FIdent("gen_slice", 0)       (* bv rt -> int -> int -> bv rt *)
 
 let rt_gen_branch       = FIdent("gen_branch", 0)      (* bool rt -> (rt_label, rt_label, rt_label) *)
-let rt_true_branch = FIdent("true_branch", 0)
-let rt_false_branch = FIdent("false_branch", 0)
-let rt_merge_branch = FIdent("merge_branch", 0)
+let rt_true_branch      = FIdent("true_branch", 0)
+let rt_false_branch     = FIdent("false_branch", 0)
+let rt_merge_branch     = FIdent("merge_branch", 0)
 
 let rt_switch_context   = FIdent("switch_context", 0)  (* rt_label -> unit *)
 let rt_gen_load         = FIdent("gen_load", 0)        (* sym -> 'a rt *)

diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml
@@ -372,10 +372,8 @@ let run include_pc iset pat env : offline_result =
   Bindings.iter (fun  fn fnsig  -> Eval.Env.addFun Unknown env' fn fnsig) fns;
   (* Run dis over the entry set identifiers with this new environment *)
 
-  let debug = false in
-
   let fns = Bindings.filter_map (fun fn fnsig ->
-    if (debug && (fn <> (FIdent ("aarch64_branch_unconditional_register", 0)))) || (not (Bindings.mem fn instrs))  then None
+    if (not (Bindings.mem fn instrs)) then None
     else Option.map (fnsig_set_body fnsig) (dis_wrapper fn fnsig env')) fns in
   Printf.printf "  Succeeded for %d instructions\n\n" (Bindings.cardinal fns);
 
@@ -402,19 +400,16 @@ let run include_pc iset pat env : offline_result =
   Printf.printf "Stages 7-8: Offline Transform\n";
   flush stdout;
   let offline_fns = Offline_transform.run fns env in
-  (*let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.CopyProp.run k)) offline_fns in *)
   let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.DeadContextSwitch.run k)) offline_fns in
 
-  let use_rt_copyprop = true in
-
   let freachable k = 
     let k = match k with 
       | FIdent (n, _) -> Ident n
       | n -> n in
     Bindings.find k decoderst.instrs 
   in
 
-  let offline_fns = if use_rt_copyprop then (Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (freachable k))) offline_fns) else offline_fns in
+  let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (freachable k))) offline_fns in
   Transforms.BDDSimp.print_unknown_prims (); 
 
   let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in