From ef6e8d5b465f34f56fd39d0a82fe67dec2cc42c0 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 24 Jul 2024 17:52:58 +1000 Subject: [PATCH] update action --- .github/workflows/test.yml | 2 +- libASL/rt_funs.ml | 6 +++--- libASL/symbolic_lifter.ml | 9 ++------- 3 files changed, 6 insertions(+), 11 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 30f14095..9b0bf451 100644 --- 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 index 5217f13d..0850f56b 100644 --- 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 index 21c76063..636a946f 100644 --- 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,11 +400,8 @@ 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 @@ -414,7 +409,7 @@ let run include_pc iset pat env : offline_result = 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