From 9b786824c090be4c7699677e2772b44daae5765c Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 5 Apr 2024 10:55:45 +1000 Subject: [PATCH 01/19] Add lifttime PC variable Optional support for offline lifter to specify the PC value at lifttime. --- bin/asli.ml | 16 +++++++---- libASL/cpu.ml | 6 ++--- libASL/cpu.mli | 2 +- libASL/decoder_program.ml | 57 ++++++++++++++++++++++----------------- libASL/symbolic_lifter.ml | 36 ++++++++++++++----------- 5 files changed, 69 insertions(+), 48 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index 6d11b34b..6b3249ce 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -42,7 +42,7 @@ let help_msg = [ {|:sem Decode and print opcode semantics|}; {|:ast [file] Decode and write opcode semantics to stdout or a file, in a structured ast format|}; {|:gen Generate an offline lifter using the given backend|}; - {| [backend] [dir]|}; + {| [pc-option] [backend] [dir]|}; {|:project Execute ASLi commands in |}; {|:q :quit Exit the interpreter|}; {|:run Execute instructions|}; @@ -213,18 +213,24 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 (fun s -> Printf.fprintf chan "%s\n" (Utils.to_string (PP.pp_raw_stmt s))) (Dis.dis_decode_entry cpu.env cpu.denv decoder op); Option.iter close_out chan_opt - | ":gen" :: iset :: id :: rest when List.length rest <= 2 -> + | ":gen" :: iset :: id :: rest when List.length rest <= 3 -> + let pc_option = Option.value List.(nth_opt rest 0) ~default:"false" in let backend = Option.value List.(nth_opt rest 0) ~default:"ocaml" in - Printf.printf "Generating lifter for %s %s using %s backend\n" iset id backend; + Printf.printf "Generating lifter for %s %s with pc option %s using %s backend\n" iset id pc_option backend; + + let pc_option = match String.lowercase_ascii pc_option with + | "false" -> false + | "true" -> true + | _ -> invalid_arg @@ Printf.sprintf "unkown pc option %s (expected: true, false)" pc_option in let (backend, default_dir) = match List.assoc_opt backend gen_backends with | Some x -> x | None -> invalid_arg @@ Printf.sprintf "unknown backend %s (supported: %s)" backend (String.concat ", " List.(map fst gen_backends)) in - let dir = Option.value List.(nth_opt rest 1) ~default:default_dir in + let dir = Option.value List.(nth_opt rest 2) ~default:default_dir in let cpu' = Cpu.mkCPU cpu.env cpu.denv in - cpu'.gen iset id backend dir + cpu'.gen iset id pc_option backend dir | ":dump" :: iset :: opcode :: rest -> let fname = (match rest with diff --git a/libASL/cpu.ml b/libASL/cpu.ml index 19430dc6..e734855b 100644 --- a/libASL/cpu.ml +++ b/libASL/cpu.ml @@ -25,7 +25,7 @@ type cpu = { elfwrite : Int64.t -> char -> unit; opcode : string -> Primops.bigint -> unit; sem : string -> Primops.bigint -> unit; - gen : string -> string -> gen_backend -> string -> unit; + gen : string -> string -> bool -> gen_backend -> string -> unit; } let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu = @@ -62,11 +62,11 @@ let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu = (fun s -> Printf.printf "%s\n" (pp_stmt s)) (Dis.dis_decode_entry env denv decoder op) - and gen (iset: string) (pat: string) (backend: gen_backend) (dir: string): unit = + and gen (iset: string) (pat: string) (include_pc: bool) (backend: gen_backend) (dir: string): unit = if not (Sys.file_exists dir) then failwith ("Can't find target dir " ^ dir); (* Build the symbolic lifter *) - let (decoder_id,decoder_fnsig,tests,instrs) = Symbolic_lifter.run iset pat env in + let (decoder_id,decoder_fnsig,tests,instrs) = Symbolic_lifter.run include_pc iset pat env in let run_gen_backend : gen_function = match backend with diff --git a/libASL/cpu.mli b/libASL/cpu.mli index 3b49f2ad..a3a71a12 100644 --- a/libASL/cpu.mli +++ b/libASL/cpu.mli @@ -21,7 +21,7 @@ type cpu = { elfwrite : Int64.t -> char -> unit; opcode : string -> Primops.bigint -> unit; sem : string -> Primops.bigint -> unit; - gen : string -> string -> gen_backend -> string -> unit; + gen : string -> string -> bool -> gen_backend -> string -> unit; } val mkCPU : Eval.Env.t -> Dis.env -> cpu diff --git a/libASL/decoder_program.ml b/libASL/decoder_program.ml index 5558e71c..7d3ac047 100644 --- a/libASL/decoder_program.ml +++ b/libASL/decoder_program.ml @@ -4,17 +4,23 @@ open Asl_utils (* Convert an ASL decoder/instruction construct into an executable ASL program. - The results consits of: + The results consists of: - A decoder function - A series of instruction encoding test functions, to sanity check the result - A series of instruction encoding behaviour functions, corresponding to the instruction execution - All of these functions consume the 32bit instruction encoding, with only the tests - returning a boolean result. + The decoder and instruction behaviour functions take the 32bit instruction encoding and optionally + the current PC, returning nothing. + The test functions take only the current instruction encoding and return a boolean result. *) let enc = Ident("enc") let enc_type = Type_Bits (expr_of_int 32) +let pc = Ident("pc") +let pc_type = Type_Bits (expr_of_int 32) + +let generate_args include_pc = + [enc_type, enc] @ (if include_pc then [pc_type, pc] else []) let expr_in_bits e b = let bv = Value.to_bits Unknown (Value.from_bitsLit b) in @@ -29,7 +35,7 @@ let enc_expr opcode = | Opcode_Bits b -> expr_in_bits (Expr_Var enc) b | Opcode_Mask m -> expr_in_mask (Expr_Var enc) m -let enc_slice lo wd = +let enc_slice lo wd = Expr_Slices (Expr_Var enc, [Slice_LoWd (expr_of_int lo, expr_of_int wd)]) let field_extract loc (IField_Field (f, lo, wd)) = @@ -40,6 +46,11 @@ let unpred_test loc (i, b) = let not_expr a = Expr_TApply (FIdent ("not_bool", 0), [], [a]) +let rec and_exprs = function + | [e] -> e + | e::es -> Expr_TApply (FIdent ("and_bool", 0), [], [e;and_exprs es]) + | [] -> expr_true + let decode_slice_expr s = match s with | DecoderSlice_Slice(lo, wd) -> enc_slice lo wd @@ -65,7 +76,7 @@ let build_test_fn ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, lo (fid, (Some type_bool, [enc_type, enc], [], [enc], loc, stmts)) let get_body_fn nm = FIdent (pprint_ident nm, 0) -let build_instr_fn ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) = +let build_instr_fn include_pc ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) = (* Extract all of the instructions fields *) let stmts = List.map (field_extract loc) fields in (* Add encoding body *) @@ -76,42 +87,40 @@ let build_instr_fn ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, l let stmts = stmts @ exec in (* Build the function decl *) let fid = get_body_fn nm in - (fid, (None, [enc_type, enc], [], [enc], loc, stmts)) - -let rec and_all = function - | [e] -> e - | e::es -> Expr_TApply (FIdent ("and_bool", 0), [], [e;and_all es]) - | [] -> expr_true + let typed_args = generate_args include_pc in + (fid, (None, typed_args, [], List.map snd typed_args, loc, stmts)) -let rec decode_case vs (DecoderAlt_Alt (ps, b)) = +let rec decode_case include_pc vs (DecoderAlt_Alt (ps, b)) = let ps = List.map2 decode_pattern_expr ps vs in let (body, oc) = (match b with | DecoderBody_UNPRED loc -> ([Stmt_Dep_Unpred(loc)], []) | DecoderBody_UNALLOC loc -> ([Stmt_Undefined(loc)], []) | DecoderBody_NOP loc -> ([], []) - | DecoderBody_Encoding(nm, loc) -> + | DecoderBody_Encoding(nm, loc) -> let test_fn = get_test_fn nm in let body_fn = get_body_fn nm in + let args = (Expr_Var enc)::(if include_pc then [Expr_Var pc] else []) in let test = Expr_TApply (test_fn, [], [Expr_Var enc]) in - ([Stmt_TCall(body_fn, [], [Expr_Var enc], loc)], [test]) + ([Stmt_TCall(body_fn, [], args, loc)], [test]) | DecoderBody_Decoder (fs, c, loc) -> let stmts = List.map (field_extract loc) fs in - (stmts @ build_decoder_case c, [])) in - let c = and_all (ps @ oc) in + (stmts @ build_decoder_case include_pc c, [])) in + let c = and_exprs (ps @ oc) in S_Elsif_Cond(c, body) -and build_decoder_case (DecoderCase_Case(ss, alts, loc)) = +and build_decoder_case include_pc (DecoderCase_Case(ss, alts, loc)) = let decode_slices = List.map decode_slice_expr ss in - match List.map (decode_case decode_slices) alts with + match List.map (decode_case include_pc decode_slices) alts with | S_Elsif_Cond(c,body)::xs -> [Stmt_If(c, body, xs, [Stmt_Assert(expr_false,loc)], loc)] | _ -> failwith "Empty decoder case" -let build_decoder iset c loc = - let stmts = build_decoder_case c in +let build_decoder include_pc iset c loc = + let stmts = build_decoder_case include_pc c in let fid = FIdent(iset ^ "_decoder", 0) in - (fid, (None, [enc_type, enc], [], [enc], loc, stmts)) + let typed_args = generate_args include_pc in + (fid, (None, typed_args, [], List.map snd typed_args, loc, stmts)) -let run iset pat env problematic = +let run include_pc iset pat env problematic = let loc = Unknown in (* Find all matching instructions, pulled from testing.ml *) @@ -126,8 +135,8 @@ let run iset pat env problematic = (* Build the encoding functions *) let tests = List.map build_test_fn encs in - let instr = List.map build_instr_fn encs in - let dec = build_decoder iset decoder loc in + let instr = List.map (build_instr_fn include_pc) encs in + let dec = build_decoder include_pc iset decoder loc in (* Add to the environment *) List.iter (fun (f,s) -> Eval.Env.addFun loc env f s) tests; diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 6488855c..45bc8f05 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -13,14 +13,6 @@ open Visitor symbolic_lifter: - Remove unsupported_set with overrides.asl instead - Remove unsupported globals, including partial record removal - - ocaml_backend: - - Break output into many files, better comp + debugging - - Identities on gen_ prims rather immediately building expressions - - Cleaner tuple unpacking - - offline: - - Reduce the number of runtime temporaries generated by offline_transform *) (* Set of functions we do not want to analyse / inline due to their complexity *) @@ -293,13 +285,27 @@ let unsupported_inst tests instrs f = let dis_wrapper fn fnsig env = let (lenv,globals) = Dis.build_env env in + let body = fnsig_get_body fnsig in + let args = fnsig_get_typed_args fnsig in try - let body = fnsig_get_body fnsig in - let sym = Symbolic.Exp (Expr_Var (Decoder_program.enc)) in - let (_,lenv,_) = (Dis.declare_assign_var Unknown (Type_Bits (Expr_LitInt "32")) (Ident "enc") sym) env lenv in - let ((),lenv',stmts) = (Dis.dis_stmts body) env lenv in - let globals = IdentSet.diff globals dead_globals in + + (* Setup initial environment based on function arguments *) + let lenv = + (match args with + | [tenc, enc ; tpc, pc] -> + let (_,lenv,_) = Dis.declare_assign_var Unknown tenc enc (Symbolic.Exp (Expr_Var enc)) env lenv in + Dis.LocalEnv.setVar Unknown (Var (0, "_PC")) (Symbolic.Exp (Expr_Var pc)) lenv + | [tenc, enc] -> + let (_,lenv,_) = Dis.declare_assign_var Unknown tenc enc (Symbolic.Exp (Expr_Var enc)) env lenv in + lenv + | _ -> failwith @@ "Unexpected fn args: " ^ Utils.pp_list (fun (t,v) -> pp_type t ^ " " ^ pprint_ident v) args) in + + (* Run dis over the function body and extract the residual program *) + let ((),lenv',stmts) = Dis.dis_stmts body env lenv in let stmts = Dis.flatten stmts [] in + + (* Cleanup transforms *) + let globals = IdentSet.diff globals dead_globals in let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts in let stmts' = Transforms.RedundantSlice.do_transform Bindings.empty stmts' in let stmts' = Transforms.StatefulIntToBits.run (Dis.enum_types env) stmts' in @@ -320,9 +326,9 @@ let dis_wrapper fn fnsig env = None (* Produce a lifter for the desired parts of the instruction set *) -let run iset pat env = +let run include_pc iset pat env = Printf.printf "Stage 1: Mock decoder & instruction encoding definitions\n"; - let ((did,dsig),tests,instrs) = Decoder_program.run iset pat env problematic_enc in + let ((did,dsig),tests,instrs) = Decoder_program.run include_pc iset pat env problematic_enc in Printf.printf " Collected %d instructions\n\n" (Bindings.cardinal instrs); Printf.printf "Stage 2: Call graph construction\n"; From 6d41bd0ccf9beb4f0b3b197435151185dfc6bb14 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 5 Apr 2024 14:25:29 +1000 Subject: [PATCH 02/19] Remove problematic list, add missing variables --- libASL/decoder_program.ml | 4 ++-- libASL/symbolic_lifter.ml | 18 +----------------- offlineASL/utils.ml | 18 ++++++++++++++---- 3 files changed, 17 insertions(+), 23 deletions(-) diff --git a/libASL/decoder_program.ml b/libASL/decoder_program.ml index 7d3ac047..301bc970 100644 --- a/libASL/decoder_program.ml +++ b/libASL/decoder_program.ml @@ -120,7 +120,7 @@ let build_decoder include_pc iset c loc = let typed_args = generate_args include_pc in (fid, (None, typed_args, [], List.map snd typed_args, loc, stmts)) -let run include_pc iset pat env problematic = +let run include_pc iset pat env = let loc = Unknown in (* Find all matching instructions, pulled from testing.ml *) @@ -128,7 +128,7 @@ let run include_pc iset pat env problematic = let re = Pcre.regexp pat in let filterfn = function | ((Encoding_Block (Ident nm, Ident is, _, _, _, _, _, _)),_,_,_) -> - is = iset && Pcre.pmatch ~rex:re nm && not (List.mem nm problematic) + is = iset && Pcre.pmatch ~rex:re nm | _ -> assert false in let encs = List.filter filterfn (Eval.Env.listInstructions env) in diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 45bc8f05..99df36f4 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -24,22 +24,7 @@ let unsupported_set = IdentSet.of_list [ FIdent ("AArch64.SetExclusiveMonitors", 0); ] -(* Problematic instruction encoding names, due to various disassembly issues *) -let problematic_enc = [ - (* Need to extend RemoveUnsupported to remove all undesirable global variables & fields *) - "aarch64_system_register_system"; - "aarch64_system_register_cpsr"; -] -(* Model doesn't need these globals *) -(* Need to model these for coverage, but really should be excluded -let dead_globals = IdentSet.of_list [ - Ident "BTypeCompatible"; - Ident "__BranchTaken"; - Ident "BTypeNext"; - Ident "__ExclusiveLocal"; -] *) -let dead_globals = IdentSet.empty (** Trivial walk to replace unsupported calls with a corresponding throw *) module RemoveUnsupported = struct @@ -305,7 +290,6 @@ let dis_wrapper fn fnsig env = let stmts = Dis.flatten stmts [] in (* Cleanup transforms *) - let globals = IdentSet.diff globals dead_globals in let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts in let stmts' = Transforms.RedundantSlice.do_transform Bindings.empty stmts' in let stmts' = Transforms.StatefulIntToBits.run (Dis.enum_types env) stmts' in @@ -328,7 +312,7 @@ let dis_wrapper fn fnsig env = (* Produce a lifter for the desired parts of the instruction set *) let run include_pc iset pat env = Printf.printf "Stage 1: Mock decoder & instruction encoding definitions\n"; - let ((did,dsig),tests,instrs) = Decoder_program.run include_pc iset pat env problematic_enc in + let ((did,dsig),tests,instrs) = Decoder_program.run include_pc iset pat env in Printf.printf " Collected %d instructions\n\n" (Bindings.cardinal instrs); Printf.printf "Stage 2: Call graph construction\n"; diff --git a/offlineASL/utils.ml b/offlineASL/utils.ml index 6ead03b3..a6f9bfd5 100644 --- a/offlineASL/utils.ml +++ b/offlineASL/utils.ml @@ -52,10 +52,20 @@ let v_SP_EL0 = Expr_Var(Ident "SP_EL0") let v_FPSR = Expr_Var(Ident "FPSR") let v_FPCR = Expr_Var(Ident "FPCR") -let v_PSTATE_BTYPE = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "BTYPE") -let v_BTypeCompatible = Expr_Var (Ident "BTypeCompatible") -let v___BranchTaken = Expr_Var (Ident "__BranchTaken") -let v_BTypeNext = Expr_Var (Ident "BTypeNext") +let v_PSTATE_A = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "A") +let v_PSTATE_D = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "D") +let v_PSTATE_DIT = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "DIT") +let v_PSTATE_F = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "F") +let v_PSTATE_I = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "I") +let v_PSTATE_PAN = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "PAN") +let v_PSTATE_SP = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "SP") +let v_PSTATE_SSBS = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "SSBS") +let v_PSTATE_TCO = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "TCO") +let v_PSTATE_UAO = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "UAO") +let v_PSTATE_BTYPE = Expr_Field(Expr_Var(Ident "PSTATE"), Ident "BTYPE") +let v_BTypeCompatible = Expr_Var (Ident "BTypeCompatible") +let v___BranchTaken = Expr_Var (Ident "__BranchTaken") +let v_BTypeNext = Expr_Var (Ident "BTypeNext") let v___ExclusiveLocal = Expr_Var (Ident "__ExclusiveLocal") (**************************************************************** From d9fac78fe887ea2b7977e1a9fff4f851226ff6a1 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 5 Apr 2024 17:26:44 +1000 Subject: [PATCH 03/19] Optional pass to remove unsupported globals --- libASL/asl_utils.ml | 29 ++++++++++ libASL/symbolic_lifter.ml | 29 +++++++++- libASL/transforms.ml | 117 +++++++++++++++++++++++++++++++++++++- 3 files changed, 172 insertions(+), 3 deletions(-) diff --git a/libASL/asl_utils.ml b/libASL/asl_utils.ml index b3b13a8d..a282ebc1 100644 --- a/libASL/asl_utils.ml +++ b/libASL/asl_utils.ml @@ -545,6 +545,35 @@ let masklength (x: string): int = String.iter (function ' ' -> () | _ -> r := !r + 1) x; !r +(* Location of a statement *) +let get_loc s = + match s with + | Stmt_If(_, _, _, _, loc) + | Stmt_VarDeclsNoInit(_, _, loc) + | Stmt_VarDecl(_, _, _, loc) + | Stmt_ConstDecl(_, _, _, loc) + | Stmt_Assign(_,_,loc) + | Stmt_FunReturn(_,loc) + | Stmt_ProcReturn(loc) + | Stmt_Assert(_, loc) + | Stmt_Unpred loc + | Stmt_ConstrainedUnpred loc + | Stmt_ImpDef (_, loc) + | Stmt_Undefined loc + | Stmt_ExceptionTaken loc + | Stmt_Dep_Unpred loc + | Stmt_Dep_Undefined loc + | Stmt_See (_,loc) + | Stmt_Throw (_, loc) + | Stmt_DecodeExecute (_, _, loc) + | Stmt_TCall (_, _, _, loc) + | Stmt_Case (_, _, _, loc) + | Stmt_For (_, _, _, _, _, loc) + | Stmt_While (_, _, loc) + | Stmt_Repeat (_, _, loc) + | Stmt_Try (_, _, _, _, loc) + | Stmt_Dep_ImpDef (_, loc) -> loc + (****************************************************************) (** {2 Function signature accessors} *) (****************************************************************) diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 99df36f4..a757d8dd 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -12,7 +12,7 @@ open Visitor symbolic_lifter: - Remove unsupported_set with overrides.asl instead - - Remove unsupported globals, including partial record removal + - Move supported globals to backend *) (* Set of functions we do not want to analyse / inline due to their complexity *) @@ -24,7 +24,25 @@ let unsupported_set = IdentSet.of_list [ FIdent ("AArch64.SetExclusiveMonitors", 0); ] +(* Backend specific: Globals we want to keep in the result *) +let supported_globals = IdentSet.of_list [ + Ident("PSTATE.C"); + Ident("PSTATE.Z"); + Ident("PSTATE.V"); + Ident("PSTATE.N"); + Ident("_PC"); + Ident("_R"); + Ident("_Z"); + Ident("SP_EL0"); + Ident("FPSR"); + Ident("FPCR"); +] +(* Backend specific: Globals we are confident we can ignore *) +let ignored_globals = IdentSet.of_list [ + Ident("__BranchTaken"); + Ident("BTypeNext"); +] (** Trivial walk to replace unsupported calls with a corresponding throw *) module RemoveUnsupported = struct @@ -289,8 +307,15 @@ let dis_wrapper fn fnsig env = let ((),lenv',stmts) = Dis.dis_stmts body env lenv in let stmts = Dis.flatten stmts [] in + (* Optional post-pass to prune unsupported globals and their fields *) + let stmts' = if false then + let flattened_globals = Transforms.UnsupportedVariables.flatten_vars (Eval.Env.readGlobals env) in + let unsupported_globals = IdentSet.diff flattened_globals supported_globals in + Transforms.UnsupportedVariables.do_transform ignored_globals unsupported_globals stmts + else stmts in + (* Cleanup transforms *) - let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts in + let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in let stmts' = Transforms.RedundantSlice.do_transform Bindings.empty stmts' in let stmts' = Transforms.StatefulIntToBits.run (Dis.enum_types env) stmts' in let stmts' = Transforms.IntToBits.ints_to_bits stmts' in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 44065720..fad2aa5a 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -835,6 +835,7 @@ module StatefulIntToBits = struct | Stmt_VarDeclsNoInit _ | Stmt_Assign _ | Stmt_Assert _ + | Stmt_Throw _ | Stmt_TCall _ -> (st,stmt) | _ -> failwith "walk: invalid IR") in (st,acc@[stmt]) @@ -1346,7 +1347,8 @@ module CopyProp = struct let (fstmts, fcopies) = copyProp' fstmts copies in (acc@[Stmt_If (e, tstmts, [], fstmts, loc)], merge tcopies fcopies) - | Stmt_Assert (_, _) -> + | Stmt_Throw _ + | Stmt_Assert _ -> (* Statements that shouldn't clobber *) (acc@[subst_stmt copies stmt], copies) @@ -1816,3 +1818,116 @@ module FixRedefinitions = struct visit_stmts v s end +(* Ensure the program does not write or read a set of variables and fields. + Assumes all record accesses are fully flattened and no name collisions between + variable names and field accesses with '.' concatenation. + Reads and writes to unsupported variables are reduced to throws. + A set of variables and fields can be additionally nominated to be silently ignored, + such that their updates are removed, however, their reads will still become throws. + *) +module UnsupportedVariables = struct + type state = { + unsupported: IdentSet.t; + ignored: IdentSet.t; + debug: bool; + } + + let throw loc = Stmt_Throw(Ident ("UNSUPPORTED"), loc) + + let concat_ident a b = + match a, b with + | Ident a, Ident b -> Ident (a ^ "." ^ b) + | _ -> invalid_arg "concat_ident" + + (* Reduce a series of field accesses into a single ident *) + let rec reduce_expr e = + match e with + | Expr_Var v -> v + | Expr_Field (e, f) -> concat_ident (reduce_expr e) f + | _ -> invalid_arg @@ "reduce_expr: " ^ pp_expr e + let rec reduce_lexpr e = + match e with + | LExpr_Var (v) -> v + | LExpr_Field (e, f) -> concat_ident (reduce_lexpr e) f + | LExpr_Array (e, _) -> reduce_lexpr e + | _ -> invalid_arg @@ "reduce_lexpr: " ^ pp_lexpr e + + (* Test read/write sets, with logging *) + let unsupported_read name st = + let r = IdentSet.mem name st.unsupported || IdentSet.mem name st.ignored in + if r && st.debug then Printf.printf "Unsupported Read: %s\n" (pprint_ident name); + r + let ignored_write name st = + let r = IdentSet.mem name st.ignored in + if r && st.debug then Printf.printf "Ignored Write: %s\n" (pprint_ident name); + r + let unsupported_write name st = + let r = IdentSet.mem name st.unsupported in + if r && st.debug then Printf.printf "Unsupported Write: %s\n" (pprint_ident name); + r + + (* Search a stmt/expr for an unsupported load. + Assumes the load will be evaluated, i.e., no short-circuiting. + *) + class find_unsupported_read st = object + inherit nopAslVisitor + val mutable issue = false + method has_issue = issue + method! vexpr = function + | Expr_Var name -> + if unsupported_read name st then issue <- true; + SkipChildren + | Expr_Field _ as e -> + if unsupported_read (reduce_expr e) st then issue <- true; + SkipChildren + | _ -> DoChildren + end + + let unsupported_stmt stmt st = + let v = new find_unsupported_read st in + let _ = visit_stmt v stmt in + v#has_issue + + let unsupported_expr expr st = + let v = new find_unsupported_read st in + let _ = visit_expr v expr in + v#has_issue + + let rec walk stmts st = + List.fold_right (fun s acc -> + match s with + | Stmt_Assign(lexpr, e, loc) -> + let name = reduce_lexpr lexpr in + if ignored_write name st then acc + else if unsupported_write name st then [throw loc] + else if unsupported_stmt s st then [throw loc] + else s::acc + | Stmt_If(e, tstmts, [], fstmts, loc) when unsupported_expr e st -> + [throw loc] + | Stmt_If(e, tstmts, [], fstmts, loc) -> + let tstmts = walk tstmts st in + let fstmts = walk fstmts st in + Stmt_If(e, tstmts, [], fstmts, loc)::acc + | s -> + if unsupported_stmt s st then [throw (get_loc s)] + else s::acc) stmts [] + + (* Entry point to the transform *) + let do_transform ignored unsupported stmts = + let st = { ignored ; unsupported ; debug = false } in + walk stmts st + + (* Utility to convert a global state into flattened variable identifiers *) + let rec flatten_var (k: ident) (v: Value.value) = + match v with + | Value.VRecord bs -> + let fields = Bindings.bindings bs in + let vals = List.map (fun (f,v) -> flatten_var (concat_ident k f) v) fields in + List.flatten vals + | _ -> [k] + + let flatten_vars vars = + let globals = Bindings.bindings vars in + IdentSet.of_list (List.flatten (List.map (fun (k,v) -> flatten_var k v) globals)) + +end From 529e4d6ed9eedc2cd1c70aa1ec2e83ea6155c22c Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 5 Apr 2024 17:27:26 +1000 Subject: [PATCH 04/19] Whitespace in transforms --- libASL/transforms.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/libASL/transforms.ml b/libASL/transforms.ml index fad2aa5a..700630ee 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -1717,24 +1717,24 @@ module RemoveRegisters = struct end -module type ScopedBindings = sig +module type ScopedBindings = sig type 'elt t = 'elt Bindings.t Stack.t - val push_scope : 'elt t -> unit -> unit - val pop_scope : 'elt t -> unit -> unit - val add_bind : 'elt t -> ident -> 'elt -> unit - val find_binding : 'elt t -> ident -> 'elt option + val push_scope : 'elt t -> unit -> unit + val pop_scope : 'elt t -> unit -> unit + val add_bind : 'elt t -> ident -> 'elt -> unit + val find_binding : 'elt t -> ident -> 'elt option val current_scope_bindings : 'elt t -> 'elt Bindings.t end -module ScopedBindings : ScopedBindings = struct +module ScopedBindings : ScopedBindings = struct type 'elt t = 'elt Bindings.t Stack.t - let push_scope (b:'elt t) (_:unit) : unit = Stack.push (Bindings.empty) b - let pop_scope (b:'elt t) (_:unit) : unit = Stack.pop_opt b |> ignore - let add_bind (b:'elt t) k v : unit = Stack.push (Bindings.add k v (Stack.pop b)) b + let push_scope (b:'elt t) (_:unit) : unit = Stack.push (Bindings.empty) b + let pop_scope (b:'elt t) (_:unit) : unit = Stack.pop_opt b |> ignore + let add_bind (b:'elt t) k v : unit = Stack.push (Bindings.add k v (Stack.pop b)) b let find_binding (b:'elt t) (i) : 'a option = Seq.find_map (fun s -> Bindings.find_opt i s) (Stack.to_seq b) - + (** returns a flattened view of bindings accessible from the current (innermost) scope. *) let current_scope_bindings (b:'elt t) : 'elt Bindings.t = (* inner bindings shadow outer bindings. *) @@ -1762,8 +1762,8 @@ module FixRedefinitions = struct Stack.push (Bindings.empty) s ; s method push_scope (_:unit) : unit = push_scope scoped_bindings () - method pop_scope (_:unit) : unit = pop_scope scoped_bindings () - method add_bind (n: var_t) : unit = add_bind scoped_bindings n.name n + method pop_scope (_:unit) : unit = pop_scope scoped_bindings () + method add_bind (n: var_t) : unit = add_bind scoped_bindings n.name n method existing_binding (i: ident) : var_t option = find_binding scoped_bindings i method incr_binding (i: ident) : var_t = From 1b1e68c625a8fa55718dc3a821ad53d8989a33fe Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Mon, 8 Apr 2024 13:05:14 +1000 Subject: [PATCH 05/19] Re-enable case simp for offline --- libASL/symbolic_lifter.ml | 1 + libASL/transforms.ml | 1 + 2 files changed, 2 insertions(+) diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index a757d8dd..efb4bf6f 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -322,6 +322,7 @@ let dis_wrapper fn fnsig env = (*let stmts' = Transforms.CommonSubExprElim.do_transform stmts' in*) let stmts' = Transforms.CopyProp.copyProp stmts' in let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in + let stmts' = Transforms.CaseSimp.do_transform stmts' in let stmts' = Transforms.RemoveRegisters.run stmts' in let stmts' = Cleanup.run false stmts' in let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 700630ee..e2b8ce0f 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -1626,6 +1626,7 @@ module CaseSimp = struct | Some (w, x', b), Some (r', c), Some res when x' = x && r = r' -> Some (StringMap.add b c res) | _ -> None) | Stmt_Assert (Expr_Var(Ident "FALSE"), _) -> Some StringMap.empty + | Stmt_Throw _ -> Some StringMap.empty | _ -> None (* Match a chain of 'if X = BV_CONSTANT then R := BV_CONSTANT else if ... else assert FALSE', From a6f0cf53f20d48136b5a2965d874ec667cc97342 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Mon, 8 Apr 2024 11:47:55 +1000 Subject: [PATCH 06/19] Decoder cleanup and sanity checks --- asli.opam | 1 + dune-project | 1 + libASL/decoder_program.ml | 282 ++++++++++++++++++++++++++++++++++---- libASL/dune | 2 +- libASL/symbolic.ml | 20 +-- 5 files changed, 265 insertions(+), 41 deletions(-) diff --git a/asli.opam b/asli.opam index 690da900..bbd00841 100644 --- a/asli.opam +++ b/asli.opam @@ -30,6 +30,7 @@ depends: [ "lwt" "cohttp-lwt-unix" "yojson" + "mlbdd" "odoc" {with-doc} ] build: [ diff --git a/dune-project b/dune-project index 6b9b8780..4edbc262 100644 --- a/dune-project +++ b/dune-project @@ -29,6 +29,7 @@ "lwt" "cohttp-lwt-unix" "yojson" + "mlbdd" ) (sites (share aslfiles)) ) diff --git a/libASL/decoder_program.ml b/libASL/decoder_program.ml index 301bc970..29df63ef 100644 --- a/libASL/decoder_program.ml +++ b/libASL/decoder_program.ml @@ -2,18 +2,6 @@ open Asl_ast open Symbolic open Asl_utils -(* - Convert an ASL decoder/instruction construct into an executable ASL program. - The results consists of: - - A decoder function - - A series of instruction encoding test functions, to sanity check the result - - A series of instruction encoding behaviour functions, corresponding to the instruction execution - - The decoder and instruction behaviour functions take the 32bit instruction encoding and optionally - the current PC, returning nothing. - The test functions take only the current instruction encoding and return a boolean result. -*) - let enc = Ident("enc") let enc_type = Type_Bits (expr_of_int 32) let pc = Ident("pc") @@ -29,11 +17,229 @@ let expr_in_bits e b = let expr_in_mask e b = let bv = Value.to_mask Unknown (Value.from_maskLit b) in sym_expr @@ sym_inmask Unknown (Exp e) bv +let get_body_fn nm = FIdent (pprint_ident nm, 0) + + +(* + let mutual e bdds = + let distinct = List.mapi (fun i e' -> (i,MLBDD.(is_false (dand e e')))) bdds in + List.filter_map (fun (i,b) -> if not b then Some i else None) distinct + + let rec order_indep pos bdds = + match bdds with + | e::xs -> + let res = mutual e xs in + let res = List.map (fun offset -> (pos, offset + pos)) res in + let remaining = order_indep (pos+1) xs in + res@remaining + | [] -> [] + + + (* Given a list of bodies and their BDD guards, collapse common bodies *) + let similar_bodies a b = + match a, b with + | DecoderBody_UNPRED _, DecoderBody_UNPRED _ -> true + | DecoderBody_UNALLOC _, DecoderBody_UNALLOC _ -> true + | DecoderBody_NOP _, DecoderBody_NOP _ -> true + | DecoderBody_Encoding(nm, _), DecoderBody_Encoding(nm', _) -> nm = nm' + | _ -> false + + let rec common_bodies xs = + match xs with + | (g,b)::xs -> + let (same,rest) = List.partition (fun (_,b') -> similar_bodies b b') xs in + let conds = List.map (fun (g,_) -> g) same in + let collapse = List.fold_right MLBDD.dor conds g in + let rest = common_bodies rest in + (collapse,b)::rest + | _ -> [] + + let slice_of_mask m (lo,wd) = + let hi = 32 - lo - wd in + DecoderPattern_Mask (String.sub m hi wd) + + let covert_back e slices = + let masks = List.map implicant_to_mask (MLBDD.allprime e) in + List.map (fun m -> List.map (slice_of_mask m) slices) masks +*) + + +module DecoderChecks = struct + type sl = (int * int) + type st = { + ctx: MLBDD.man; + vars: sl Bindings.t; + cur_enc: MLBDD.t; + unpred: MLBDD.t; + unalloc: MLBDD.t; + nop: MLBDD.t; + instrs: MLBDD.t Bindings.t; + } + + let init_state = + let ctx = MLBDD.init ~cache:1024 () in + { + ctx ; + vars = Bindings.empty ; + cur_enc = MLBDD.dtrue ctx ; + unpred = MLBDD.dfalse ctx ; + unalloc = MLBDD.dfalse ctx ; + nop = MLBDD.dfalse ctx ; + instrs = Bindings.empty ; + } + + let get_slice s st = Bindings.find s st.vars + + let extract_field (IField_Field(f, lo, wd)) st = + { st with vars = Bindings.add f (lo,wd) st.vars } + + let add_unpred g st = + { st with unpred = MLBDD.dor st.unpred g } + + let add_unalloc g st = + { st with unalloc = MLBDD.dor st.unalloc g } + + let add_nop g st = + { st with nop = MLBDD.dor st.nop g } + + let add_instr k g st = + let existing = Option.value (Bindings.find_opt k st.instrs) ~default:(MLBDD.dfalse st.ctx) in + { st with instrs = Bindings.add k (MLBDD.dor existing g) st.instrs } + + let restrict_enc g st = + { st with cur_enc = MLBDD.dand st.cur_enc g } + + let set_enc g st = + { st with cur_enc = g } + + let bdd_of_mask bs lo ctx = + snd @@ String.fold_right (fun c (pos,e) -> + match c with + | ' ' -> (pos, e) + | 'x' -> (* No constraint *) + (pos + 1, e) + | '1' -> (* bit hi is true *) + let bit = MLBDD.ithvar ctx pos in + (pos + 1, MLBDD.dand bit e) + | '0' -> (* bit hi is true *) + let bit = MLBDD.dnot (MLBDD.ithvar ctx pos) in + (pos + 1, MLBDD.dand bit e) + | _ -> invalid_arg "bdd_of_mask") bs (lo,MLBDD.dtrue ctx) + + let implicant_to_mask m = + let chars = List.init 32 (fun i -> + if List.mem (true, i) m then '1' else + if List.mem (false, i) m then '0' else + 'x' + ) in + let buf = Buffer.create 32 in + List.iter (Buffer.add_char buf) (List.rev chars); + Buffer.contents buf + + let to_string bdd = + let imps = MLBDD.allprime bdd in + Utils.pp_list implicant_to_mask imps + + (* Represent slices in terms of their position in enc *) + let decode_slice s st = + match s with + | DecoderSlice_Slice(lo, wd) -> (lo,wd) + | DecoderSlice_FieldName f -> get_slice f st + | DecoderSlice_Concat fs -> failwith "DecoderSlice_Concat not expected" + + (* Convert decode patterns into BDDs *) + let rec decode_pattern (lo,wd) p ctx = + match p with + | DecoderPattern_Bits b + | DecoderPattern_Mask b -> bdd_of_mask b lo ctx + | DecoderPattern_Wildcard _ -> MLBDD.dtrue ctx + | DecoderPattern_Not p -> MLBDD.dnot (decode_pattern (lo,wd) p ctx) + + (* Combine the various tests due to a guard into one BDD *) + let decode_case_guard vs ps st = + List.fold_left2 (fun e s p -> MLBDD.dand e (decode_pattern s p st.ctx)) (st.cur_enc) vs ps + + (* Collect reachability for each instruction encoding IGNORING ordering on alts *) + let rec tf_decode_case b st = + match b with + | DecoderBody_UNPRED loc -> add_unpred st.cur_enc st + | DecoderBody_UNALLOC loc -> add_unalloc st.cur_enc st + | DecoderBody_NOP loc -> add_nop st.cur_enc st + | DecoderBody_Encoding(nm, loc) -> add_instr nm st.cur_enc st + | DecoderBody_Decoder(fs, c, loc) -> + tf_decoder c (List.fold_right extract_field fs st) + + and tf_decoder (DecoderCase_Case(ss, alts, loc)) st = + let vs = List.map (fun s -> decode_slice s st) ss in + List.fold_left ( fun st (DecoderAlt_Alt(ps,b))-> + let guard = decode_case_guard vs ps st in + let st' = tf_decode_case b (restrict_enc guard st) in + let st = set_enc st.cur_enc st' in + st ) st alts + + (* *) + let possibly_set pos ctx nm bdd = + let res = MLBDD.(dand bdd (ithvar ctx pos)) in + not (MLBDD.is_false res) + + (* *) + let possibly_clr pos ctx nm bdd = + let res = MLBDD.(dand bdd (dnot (ithvar ctx pos))) in + not (MLBDD.is_false res) + + (* + let rec generate_bit_split pos reach st = + Printf.printf "%d\n" pos; + if pos < 20 || Bindings.cardinal st.instrs < 2 then + (match Bindings.bindings st.instrs with + | (nm,bdd)::xs -> [Stmt_TCall(nm, [], [], Unknown)] + | [] -> []) + else + let set = Bindings.filter (possibly_set pos st.ctx) st.instrs in + let clr = Bindings.filter (possibly_clr pos st.ctx) st.instrs in + let set_reach = MLBDD.(dand reach (ithvar st.ctx pos)) in + let clr_reach = MLBDD.(dand reach (dnot (ithvar st.ctx pos))) in + let set_split = generate_bit_split (pos - 1) set_reach {st with instrs = set} in + let clr_split = generate_bit_split (pos - 1) clr_reach {st with instrs = clr} in + let test = Expr_TApply(FIdent("eq_bits",0), [Expr_LitInt "1"], [Expr_Slices( Expr_Var (Ident "enc"), [Slice_LoWd(expr_of_int pos,expr_of_int 1)]); Expr_LitBits "1"]) in + [Stmt_If(test, set_split, [], clr_split, Unknown)] + *) + + let generate_decoder st = + let stmts = Bindings.fold (fun nm bdd stmts -> + let imps = MLBDD.allprime bdd in + let masks = List.map implicant_to_mask imps in + let body = [Stmt_TCall(get_body_fn nm, [], [], Unknown)] in + stmts@(List.map (fun m -> S_Elsif_Cond(expr_in_mask (Expr_Var enc) m, body)) masks)) st.instrs [] in + match stmts with + | S_Elsif_Cond(c,b)::els -> [Stmt_If(c,b,els,[],Unknown)] + | _ -> failwith "unreachable" + + let do_transform d env = + let st = tf_decoder d init_state in + generate_decoder st + +end + + +(* + Convert an ASL decoder/instruction construct into an executable ASL program. + The results consists of: + - A decoder function + - A series of instruction encoding test functions, to sanity check the result + - A series of instruction encoding behaviour functions, corresponding to the instruction execution + + The decoder and instruction behaviour functions take the 32bit instruction encoding and optionally + the current PC, returning nothing. + The test functions take only the current instruction encoding and return a boolean result. +*) let enc_expr opcode = match opcode with | Opcode_Bits b -> expr_in_bits (Expr_Var enc) b - | Opcode_Mask m -> expr_in_mask (Expr_Var enc) m + | Opcode_Mask m -> + if String.exists (fun c -> c = 'x') m then expr_in_mask (Expr_Var enc) m + else expr_in_bits (Expr_Var enc) m let enc_slice lo wd = Expr_Slices (Expr_Var enc, [Slice_LoWd (expr_of_int lo, expr_of_int wd)]) @@ -64,18 +270,22 @@ let rec decode_pattern_expr p e = | DecoderPattern_Wildcard _ -> expr_true | DecoderPattern_Not p -> not_expr (decode_pattern_expr p e) +(* + Test function to evaluate guard statements on instruction encodings. + Often these tests are trivially true, avoid building the function if so. + No need to sanity test the opcode, we validate this in a pre-pass over the decoder statically. + *) let get_test_fn nm = FIdent (pprint_ident nm ^ "_decode_test", 0) +let is_trivial_test ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) = + unpreds = [] && guard = expr_true let build_test_fn ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) = - (* Assert no unpredictable bits and return true *) - let stmts = List.map (unpred_test loc) unpreds @ [Stmt_FunReturn(expr_true, loc)] in - (* Run the encoding guard given the extracted fields *) - let stmts = List.map (field_extract loc) fields @ [Stmt_If (guard, stmts, [], [Stmt_FunReturn(expr_false, loc)], loc)] in - (* Sanity test the opcode *) - let stmts = [Stmt_If(enc_expr opcode, stmts, [], [Stmt_FunReturn(expr_false, loc)], loc)] in + (* Return the guard result *) + let stmts = [Stmt_FunReturn(guard, loc)] in + (* Assert no unpredictable bits *) + let stmts = List.map (unpred_test loc) unpreds @ stmts in let fid = get_test_fn nm in (fid, (Some type_bool, [enc_type, enc], [], [enc], loc, stmts)) -let get_body_fn nm = FIdent (pprint_ident nm, 0) let build_instr_fn include_pc ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) = (* Extract all of the instructions fields *) let stmts = List.map (field_extract loc) fields in @@ -90,7 +300,7 @@ let build_instr_fn include_pc ((Encoding_Block (nm, _, fields, opcode, guard, un let typed_args = generate_args include_pc in (fid, (None, typed_args, [], List.map snd typed_args, loc, stmts)) -let rec decode_case include_pc vs (DecoderAlt_Alt (ps, b)) = +let rec decode_case include_pc has_test vs (DecoderAlt_Alt (ps, b)) = let ps = List.map2 decode_pattern_expr ps vs in let (body, oc) = (match b with | DecoderBody_UNPRED loc -> ([Stmt_Dep_Unpred(loc)], []) @@ -101,21 +311,21 @@ let rec decode_case include_pc vs (DecoderAlt_Alt (ps, b)) = let body_fn = get_body_fn nm in let args = (Expr_Var enc)::(if include_pc then [Expr_Var pc] else []) in let test = Expr_TApply (test_fn, [], [Expr_Var enc]) in - ([Stmt_TCall(body_fn, [], args, loc)], [test]) + ([Stmt_TCall(body_fn, [], args, loc)], if IdentSet.mem nm has_test then [test] else []) | DecoderBody_Decoder (fs, c, loc) -> let stmts = List.map (field_extract loc) fs in - (stmts @ build_decoder_case include_pc c, [])) in + (stmts @ build_decoder_case include_pc has_test c, [])) in let c = and_exprs (ps @ oc) in S_Elsif_Cond(c, body) -and build_decoder_case include_pc (DecoderCase_Case(ss, alts, loc)) = +and build_decoder_case include_pc has_test (DecoderCase_Case(ss, alts, loc)) = let decode_slices = List.map decode_slice_expr ss in - match List.map (decode_case include_pc decode_slices) alts with + match List.map (decode_case include_pc has_test decode_slices) alts with | S_Elsif_Cond(c,body)::xs -> [Stmt_If(c, body, xs, [Stmt_Assert(expr_false,loc)], loc)] | _ -> failwith "Empty decoder case" -let build_decoder include_pc iset c loc = - let stmts = build_decoder_case include_pc c in +let build_decoder include_pc has_test iset c loc = + let stmts = build_decoder_case include_pc has_test c in let fid = FIdent(iset ^ "_decoder", 0) in let typed_args = generate_args include_pc in (fid, (None, typed_args, [], List.map snd typed_args, loc, stmts)) @@ -133,10 +343,22 @@ let run include_pc iset pat env = in let encs = List.filter filterfn (Eval.Env.listInstructions env) in - (* Build the encoding functions *) - let tests = List.map build_test_fn encs in + (* Run a series of sanity tests over the decoder *) + let dec_body = DecoderChecks.do_transform decoder env in + let fid = FIdent(iset ^ "_decoder", 0) in + let typed_args = generate_args include_pc in + let dec = (fid, (None, typed_args, [], List.map snd typed_args, loc, dec_body)) in + + (* Build the encoding test functions if necessary *) + let (trivial,essen) = List.partition is_trivial_test encs in + let tests = List.map build_test_fn essen in + (*let has_test = IdentSet.of_list ( List.map ( fun ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) -> nm ) essen ) in*) + + (* Build the instruction functions *) let instr = List.map (build_instr_fn include_pc) encs in - let dec = build_decoder include_pc iset decoder loc in + + (* Build the decoder itself *) + (*let dec = build_decoder include_pc has_test iset decoder loc in*) (* Add to the environment *) List.iter (fun (f,s) -> Eval.Env.addFun loc env f s) tests; diff --git a/libASL/dune b/libASL/dune index 6fae933e..1298b6ac 100644 --- a/libASL/dune +++ b/libASL/dune @@ -25,7 +25,7 @@ offline_transform ocaml_backend dis_tc offline_opt ) - (libraries pprint zarith z3 str pcre dune-site)) + (libraries pprint zarith z3 str pcre mlbdd dune-site)) (generate_sites_module (module res) diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index f597b28b..90bdf14f 100644 --- a/libASL/symbolic.ml +++ b/libASL/symbolic.ml @@ -252,16 +252,6 @@ let sym_eq_bits = prim_binop "eq_bits" let sym_eq_real = prim_binop "eq_real" -let sym_inmask loc v mask = - match v with - | Val x -> Val (VBool (prim_in_mask (to_bits loc x) mask)) - | Exp e -> - let n = mask.n in - let ne = Expr_LitInt (string_of_int n) in - let m = val_expr (VBits {v = mask.m; n}) in - let v = val_expr (VBits {v = mask.v; n}) in - Exp (Expr_TApply (FIdent ("eq_bits", 0), [ne], [(Expr_TApply (FIdent ("and_bits", 0), [ne], [e; m]));v])) - let sym_eq (loc: AST.l) (x: sym) (y: sym): sym = (match (x,y) with | (Val x,Val y) -> Val (from_bool (eval_eq loc x y)) @@ -419,6 +409,16 @@ let sym_and_bits loc w (x: sym) (y: sym) = | x, Val y when is_one_bits y -> x | _ -> Exp (Expr_TApply (FIdent ("and_bits", 0), [w], [sym_expr x; sym_expr y]) ) +let sym_inmask loc v mask = + match v with + | Val x -> Val (VBool (prim_in_mask (to_bits loc x) mask)) + | Exp e -> + let n = mask.n in + let ne = Expr_LitInt (string_of_int n) in + let m = Val (VBits {v = mask.m; n}) in + let v = Val (VBits {v = mask.v; n}) in + sym_eq_bits loc (sym_and_bits loc ne (Exp e) m) v + let sym_or_bits loc w (x: sym) (y: sym) = match x, y with | Val x, Val y -> Val (VBits (prim_or_bits (to_bits loc x) (to_bits loc y))) From c9d28d007aad3fca932b9bb1a7b2e20cf67fd3c0 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Tue, 23 Apr 2024 09:13:03 +1000 Subject: [PATCH 07/19] Simplify reachability based on enc --- libASL/decoder_program.ml | 163 +---------- libASL/ocaml_backend.ml | 4 +- libASL/offline_opt.ml | 16 ++ libASL/symbolic_lifter.ml | 5 + libASL/transforms.ml | 553 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 580 insertions(+), 161 deletions(-) diff --git a/libASL/decoder_program.ml b/libASL/decoder_program.ml index 29df63ef..1404b910 100644 --- a/libASL/decoder_program.ml +++ b/libASL/decoder_program.ml @@ -64,162 +64,6 @@ let get_body_fn nm = FIdent (pprint_ident nm, 0) *) -module DecoderChecks = struct - type sl = (int * int) - type st = { - ctx: MLBDD.man; - vars: sl Bindings.t; - cur_enc: MLBDD.t; - unpred: MLBDD.t; - unalloc: MLBDD.t; - nop: MLBDD.t; - instrs: MLBDD.t Bindings.t; - } - - let init_state = - let ctx = MLBDD.init ~cache:1024 () in - { - ctx ; - vars = Bindings.empty ; - cur_enc = MLBDD.dtrue ctx ; - unpred = MLBDD.dfalse ctx ; - unalloc = MLBDD.dfalse ctx ; - nop = MLBDD.dfalse ctx ; - instrs = Bindings.empty ; - } - - let get_slice s st = Bindings.find s st.vars - - let extract_field (IField_Field(f, lo, wd)) st = - { st with vars = Bindings.add f (lo,wd) st.vars } - - let add_unpred g st = - { st with unpred = MLBDD.dor st.unpred g } - - let add_unalloc g st = - { st with unalloc = MLBDD.dor st.unalloc g } - - let add_nop g st = - { st with nop = MLBDD.dor st.nop g } - - let add_instr k g st = - let existing = Option.value (Bindings.find_opt k st.instrs) ~default:(MLBDD.dfalse st.ctx) in - { st with instrs = Bindings.add k (MLBDD.dor existing g) st.instrs } - - let restrict_enc g st = - { st with cur_enc = MLBDD.dand st.cur_enc g } - - let set_enc g st = - { st with cur_enc = g } - - let bdd_of_mask bs lo ctx = - snd @@ String.fold_right (fun c (pos,e) -> - match c with - | ' ' -> (pos, e) - | 'x' -> (* No constraint *) - (pos + 1, e) - | '1' -> (* bit hi is true *) - let bit = MLBDD.ithvar ctx pos in - (pos + 1, MLBDD.dand bit e) - | '0' -> (* bit hi is true *) - let bit = MLBDD.dnot (MLBDD.ithvar ctx pos) in - (pos + 1, MLBDD.dand bit e) - | _ -> invalid_arg "bdd_of_mask") bs (lo,MLBDD.dtrue ctx) - - let implicant_to_mask m = - let chars = List.init 32 (fun i -> - if List.mem (true, i) m then '1' else - if List.mem (false, i) m then '0' else - 'x' - ) in - let buf = Buffer.create 32 in - List.iter (Buffer.add_char buf) (List.rev chars); - Buffer.contents buf - - let to_string bdd = - let imps = MLBDD.allprime bdd in - Utils.pp_list implicant_to_mask imps - - (* Represent slices in terms of their position in enc *) - let decode_slice s st = - match s with - | DecoderSlice_Slice(lo, wd) -> (lo,wd) - | DecoderSlice_FieldName f -> get_slice f st - | DecoderSlice_Concat fs -> failwith "DecoderSlice_Concat not expected" - - (* Convert decode patterns into BDDs *) - let rec decode_pattern (lo,wd) p ctx = - match p with - | DecoderPattern_Bits b - | DecoderPattern_Mask b -> bdd_of_mask b lo ctx - | DecoderPattern_Wildcard _ -> MLBDD.dtrue ctx - | DecoderPattern_Not p -> MLBDD.dnot (decode_pattern (lo,wd) p ctx) - - (* Combine the various tests due to a guard into one BDD *) - let decode_case_guard vs ps st = - List.fold_left2 (fun e s p -> MLBDD.dand e (decode_pattern s p st.ctx)) (st.cur_enc) vs ps - - (* Collect reachability for each instruction encoding IGNORING ordering on alts *) - let rec tf_decode_case b st = - match b with - | DecoderBody_UNPRED loc -> add_unpred st.cur_enc st - | DecoderBody_UNALLOC loc -> add_unalloc st.cur_enc st - | DecoderBody_NOP loc -> add_nop st.cur_enc st - | DecoderBody_Encoding(nm, loc) -> add_instr nm st.cur_enc st - | DecoderBody_Decoder(fs, c, loc) -> - tf_decoder c (List.fold_right extract_field fs st) - - and tf_decoder (DecoderCase_Case(ss, alts, loc)) st = - let vs = List.map (fun s -> decode_slice s st) ss in - List.fold_left ( fun st (DecoderAlt_Alt(ps,b))-> - let guard = decode_case_guard vs ps st in - let st' = tf_decode_case b (restrict_enc guard st) in - let st = set_enc st.cur_enc st' in - st ) st alts - - (* *) - let possibly_set pos ctx nm bdd = - let res = MLBDD.(dand bdd (ithvar ctx pos)) in - not (MLBDD.is_false res) - - (* *) - let possibly_clr pos ctx nm bdd = - let res = MLBDD.(dand bdd (dnot (ithvar ctx pos))) in - not (MLBDD.is_false res) - - (* - let rec generate_bit_split pos reach st = - Printf.printf "%d\n" pos; - if pos < 20 || Bindings.cardinal st.instrs < 2 then - (match Bindings.bindings st.instrs with - | (nm,bdd)::xs -> [Stmt_TCall(nm, [], [], Unknown)] - | [] -> []) - else - let set = Bindings.filter (possibly_set pos st.ctx) st.instrs in - let clr = Bindings.filter (possibly_clr pos st.ctx) st.instrs in - let set_reach = MLBDD.(dand reach (ithvar st.ctx pos)) in - let clr_reach = MLBDD.(dand reach (dnot (ithvar st.ctx pos))) in - let set_split = generate_bit_split (pos - 1) set_reach {st with instrs = set} in - let clr_split = generate_bit_split (pos - 1) clr_reach {st with instrs = clr} in - let test = Expr_TApply(FIdent("eq_bits",0), [Expr_LitInt "1"], [Expr_Slices( Expr_Var (Ident "enc"), [Slice_LoWd(expr_of_int pos,expr_of_int 1)]); Expr_LitBits "1"]) in - [Stmt_If(test, set_split, [], clr_split, Unknown)] - *) - - let generate_decoder st = - let stmts = Bindings.fold (fun nm bdd stmts -> - let imps = MLBDD.allprime bdd in - let masks = List.map implicant_to_mask imps in - let body = [Stmt_TCall(get_body_fn nm, [], [], Unknown)] in - stmts@(List.map (fun m -> S_Elsif_Cond(expr_in_mask (Expr_Var enc) m, body)) masks)) st.instrs [] in - match stmts with - | S_Elsif_Cond(c,b)::els -> [Stmt_If(c,b,els,[],Unknown)] - | _ -> failwith "unreachable" - - let do_transform d env = - let st = tf_decoder d init_state in - generate_decoder st - -end (* @@ -344,21 +188,22 @@ let run include_pc iset pat env = let encs = List.filter filterfn (Eval.Env.listInstructions env) in (* Run a series of sanity tests over the decoder *) - let dec_body = DecoderChecks.do_transform decoder env in + (*let dec_body = DecoderChecks.do_transform decoder env in let fid = FIdent(iset ^ "_decoder", 0) in let typed_args = generate_args include_pc in let dec = (fid, (None, typed_args, [], List.map snd typed_args, loc, dec_body)) in + *) (* Build the encoding test functions if necessary *) let (trivial,essen) = List.partition is_trivial_test encs in let tests = List.map build_test_fn essen in - (*let has_test = IdentSet.of_list ( List.map ( fun ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) -> nm ) essen ) in*) + let has_test = IdentSet.of_list ( List.map ( fun ((Encoding_Block (nm, _, fields, opcode, guard, unpreds, b, loc)),opost,cond,exec) -> nm ) essen ) in (* Build the instruction functions *) let instr = List.map (build_instr_fn include_pc) encs in (* Build the decoder itself *) - (*let dec = build_decoder include_pc has_test iset decoder loc in*) + let dec = build_decoder include_pc has_test iset decoder loc in (* Add to the environment *) List.iter (fun (f,s) -> Eval.Env.addFun loc env f s) tests; diff --git a/libASL/ocaml_backend.ml b/libASL/ocaml_backend.ml index d6e421e2..9eb7cc87 100644 --- a/libASL/ocaml_backend.ml +++ b/libASL/ocaml_backend.ml @@ -313,8 +313,8 @@ and write_stmts s st = write_seq st; write_stmt s st ) xs; - dec_depth st; - assert (not st.skip_seq) + dec_depth st + (*assert (not st.skip_seq)*) let build_args targs args = if List.length targs = 0 && List.length args = 0 then "()" diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index cdb942c0..87f2af3b 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -263,6 +263,22 @@ module CopyProp = struct | None -> false | _ -> true + (* To change this, you'd need to know : + - The condition under which its safe to copy prop + - The current reachability + + If you can't establish you are guarded, implies you need to introduce a branch. + The branch will have the outcomes of both exp reduction and maintaining the current temp. + Then need to specialise everything downstream for this point based on this introduced branch. + + This means you need to pull the condition out to the front. + Which means its needs to be fully reduced and in terms of enc. + BDD approach gives us this flexibility, every single condition in the program in terms of original enc. + Relatively simple to reduce from that point: eliminate guards based on reachability, etc. + + You can implement constant-prop and dead code in a similar fashion, as long as your notions of conditional + use / redefinition / loss of constant precision is purely in terms of the original enc. + *) class copyprop_transform st = object inherit Asl_visitor.nopAslVisitor method! vexpr = function diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index efb4bf6f..fa51d26a 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -369,6 +369,11 @@ let run include_pc iset pat env = 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); + let decoder = Eval.Env.getDecoder env (Ident iset) in + let fns = Transforms.BDDSimp.transform_all fns decoder in + let (_,globals) = Dis.build_env env in + let fns = Bindings.map (fnsig_upd_body (Transforms.RemoveUnused.remove_unused globals)) fns in + Printf.printf "Stmt Counts\n"; let l = Bindings.fold (fun fn fnsig acc -> (fn, stmts_count (fnsig_get_body fnsig))::acc) fns [] in let l = List.sort (fun (_,i) (_,j) -> compare i j) l in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index e2b8ce0f..460b1c54 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -1932,3 +1932,556 @@ module UnsupportedVariables = struct IdentSet.of_list (List.flatten (List.map (fun (k,v) -> flatten_var k v) globals)) end + +module DecoderChecks = struct + type sl = (int * int) + type st = { + ctx: MLBDD.man; + vars: sl Bindings.t; + cur_enc: MLBDD.t; + unpred: MLBDD.t; + unalloc: MLBDD.t; + nop: MLBDD.t; + instrs: MLBDD.t Bindings.t; + } + + let init_state = + let ctx = MLBDD.init ~cache:1024 () in + { + ctx ; + vars = Bindings.empty ; + cur_enc = MLBDD.dtrue ctx ; + unpred = MLBDD.dfalse ctx ; + unalloc = MLBDD.dfalse ctx ; + nop = MLBDD.dfalse ctx ; + instrs = Bindings.empty ; + } + + let get_slice s st = Bindings.find s st.vars + + let extract_field (IField_Field(f, lo, wd)) st = + { st with vars = Bindings.add f (lo,wd) st.vars } + + let add_unpred g st = + { st with unpred = MLBDD.dor st.unpred g } + + let add_unalloc g st = + { st with unalloc = MLBDD.dor st.unalloc g } + + let add_nop g st = + { st with nop = MLBDD.dor st.nop g } + + let add_instr k g st = + let existing = Option.value (Bindings.find_opt k st.instrs) ~default:(MLBDD.dfalse st.ctx) in + { st with instrs = Bindings.add k (MLBDD.dor existing g) st.instrs } + + let restrict_enc g st = + { st with cur_enc = MLBDD.dand st.cur_enc g } + + let set_enc g st = + { st with cur_enc = g } + + let bdd_of_mask bs lo ctx = + snd @@ String.fold_right (fun c (pos,e) -> + match c with + | ' ' -> (pos, e) + | 'x' -> (* No constraint *) + (pos + 1, e) + | '1' -> (* bit hi is true *) + let bit = MLBDD.ithvar ctx pos in + (pos + 1, MLBDD.dand bit e) + | '0' -> (* bit hi is true *) + let bit = MLBDD.dnot (MLBDD.ithvar ctx pos) in + (pos + 1, MLBDD.dand bit e) + | _ -> invalid_arg "bdd_of_mask") bs (lo,MLBDD.dtrue ctx) + + let implicant_to_mask m = + let chars = List.init 32 (fun i -> + if List.mem (true, i) m then '1' else + if List.mem (false, i) m then '0' else + 'x' + ) in + let buf = Buffer.create 32 in + List.iter (Buffer.add_char buf) (List.rev chars); + Buffer.contents buf + + let to_string bdd = + let imps = MLBDD.allprime bdd in + Utils.pp_list implicant_to_mask imps + + (* Represent slices in terms of their position in enc *) + let decode_slice s st = + match s with + | DecoderSlice_Slice(lo, wd) -> (lo,wd) + | DecoderSlice_FieldName f -> get_slice f st + | DecoderSlice_Concat fs -> failwith "DecoderSlice_Concat not expected" + + (* Convert decode patterns into BDDs *) + let rec decode_pattern (lo,wd) p ctx = + match p with + | DecoderPattern_Bits b + | DecoderPattern_Mask b -> bdd_of_mask b lo ctx + | DecoderPattern_Wildcard _ -> MLBDD.dtrue ctx + | DecoderPattern_Not p -> MLBDD.dnot (decode_pattern (lo,wd) p ctx) + + (* Combine the various tests due to a guard into one BDD *) + let decode_case_guard vs ps st = + List.fold_left2 (fun e s p -> MLBDD.dand e (decode_pattern s p st.ctx)) (st.cur_enc) vs ps + + (* Collect reachability for each instruction encoding IGNORING ordering on alts *) + let rec tf_decode_case b st = + match b with + | DecoderBody_UNPRED loc -> add_unpred st.cur_enc st + | DecoderBody_UNALLOC loc -> add_unalloc st.cur_enc st + | DecoderBody_NOP loc -> add_nop st.cur_enc st + | DecoderBody_Encoding(nm, loc) -> add_instr nm st.cur_enc st + | DecoderBody_Decoder(fs, c, loc) -> + tf_decoder c (List.fold_right extract_field fs st) + + and tf_decoder (DecoderCase_Case(ss, alts, loc)) st = + let vs = List.map (fun s -> decode_slice s st) ss in + let (st,_) = List.fold_left ( fun (st,prior) (DecoderAlt_Alt(ps,b))-> + let guard = decode_case_guard vs ps st in + let st' = tf_decode_case b (set_enc (MLBDD.dand prior guard) st) in + let prior = MLBDD.dand prior (MLBDD.dnot guard) in + let st = set_enc st.cur_enc st' in + (st,prior) ) (st,st.cur_enc) alts in + st + + let do_transform d = + tf_decoder d init_state + +end + +module BDDSimp = struct + type abs = + Top | + Val of MLBDD.t list | + Bot + + type state = { + man: MLBDD.man; + vars: abs Bindings.t; + ctx: MLBDD.t; + stmts: stmt list; + } + + let init_state (ctx : MLBDD.t) = { + man = MLBDD.manager ctx; + vars = Bindings.empty ; + ctx ; + stmts = [] + } + + + let to_string bdd = + let imps = MLBDD.allprime bdd in + Utils.pp_list DecoderChecks.implicant_to_mask imps + + let pp_abs a = + match a with + | Top -> "Top" + | Bot -> "Bot" + | Val v -> Printf.sprintf "Val (%s)" (Utils.pp_list to_string v) + + let pp_state st = + Printf.sprintf "{ ctx = %s ; vars = %s }" (to_string st.ctx) (pp_bindings pp_abs st.vars) + + let is_true a st = + match a with + | Val [v] -> MLBDD.is_true (MLBDD.imply st.ctx v) + | _ -> false + + let is_false a st = + match a with + | Val [v] -> MLBDD.(is_true (imply st.ctx (dnot v))) + | _ -> false + + let halt st = + { st with ctx = MLBDD.dfalse st.man } + + let write s st = + { st with stmts = st.stmts @ [s] } + + let writeall stmts st = + { st with stmts = st.stmts @ stmts } + + let get_var v st = + match Bindings.find_opt v st.vars with + | Some v -> v + | _ -> Top (* logically this should be Bot, but need to init globals *) + + let add_var v abs st = + { st with vars = Bindings.add v abs st.vars } + + let restrict_ctx cond st = + match cond with + | Top -> st + | Bot -> st + | Val [cond] -> { st with ctx = MLBDD.dand st.ctx cond } + | _ -> invalid_arg "restrict_ctx" + + let to_bool abs st = + match abs with + | Top + | Bot -> MLBDD.dtrue st.man + | Val [v] -> v + | _ -> failwith "unexpected to_bool" + + let trivial_eq a b = + if List.length a <> List.length b then false + else List.fold_right2 (fun a b acc -> MLBDD.equal a b && acc) a b true + + let join_abs cond a b = + match cond, a, b with + | _, Top, _ + | _, _, Top -> Top + | _, Bot, a + | _, a, Bot -> a + | _, Val a, Val b when trivial_eq a b -> Val a + | Val [c], Val a, Val b when List.length a = List.length b -> + let a = List.map (MLBDD.dand c) a in + let ncond = MLBDD.dnot c in + let b = List.map (MLBDD.dand ncond) b in + Val (List.map2 MLBDD.dor a b) + | _, Val a, Val b -> Top + + let join_state cond a b = + let vars = Bindings.merge (fun k a b -> + match a, b with + | Some x, Some y -> Some (join_abs cond x y) + | Some x, _ -> Some x + | _, Some y -> Some y + | _ -> None) a.vars b.vars in + let ctx = MLBDD.dor a.ctx b.ctx in + { man = a.man ; vars ; ctx ; stmts = [] } + + let wrap_bop f a b = + match a, b with + | Bot, _ + | _, Bot -> Bot + | Top, _ + | _, Top -> Top + | Val a, Val b -> Val (f a b) + + let wrap_uop f a = + match a with + | Top -> Top + | Bot -> Bot + | Val a -> Val (f a) + + (****************************************************************) + (** Boolean Prims *) + (****************************************************************) + + let and_bool = wrap_bop (fun a b -> + match a, b with + | [a], [b] -> [MLBDD.dand a b] + | _ -> failwith "bad bool width") + + let or_bool = wrap_bop (fun a b -> + match a, b with + | [a], [b] -> [MLBDD.dor a b] + | _ -> failwith "bad bool width") + + let not_bool = wrap_uop (fun a -> + match a with + | [a] -> [MLBDD.dnot a] + | _ -> failwith "bad bool width") + + let eq_bool = wrap_bop (fun a b -> + match a, b with + | [a], [b] -> [MLBDD.eq a b] + | _ -> failwith "bad bool width") + + let ne_bool = wrap_bop (fun a b -> + match a, b with + | [a], [b] -> [MLBDD.(dnot (eq a b))] + | _ -> failwith "bad bool width") + + (****************************************************************) + (** Bitvector Prims *) + (****************************************************************) + + let and_bits = wrap_bop (List.map2 MLBDD.dand) + let or_bits = wrap_bop (List.map2 MLBDD.dor) + let eor_bits = wrap_bop (List.map2 MLBDD.xor) + + let not_bits = wrap_uop (List.map MLBDD.dnot) + + let eq_bits = wrap_bop (fun a b -> + let bits = List.map2 MLBDD.eq a b in + match bits with + | x::xs -> [List.fold_right MLBDD.dand xs x] + | _ -> failwith "bad bits width" + ) + let ne_bits a b = not_bool (eq_bits a b) + + let zero_extend_bits x nw st = + match x with + | Val v -> Val (List.init (nw - List.length v) (fun _ -> MLBDD.dfalse st.man) @ v) + | _ -> x + + let sign_extend_bits x nw st = + match x with + | Val (x::xs) -> Val (List.init (nw - List.length xs - 1) (fun _ -> x) @ (x::xs)) + | _ -> x + + let append_bits = wrap_bop (@) + + let rec sublist l start wd = + match l, start, wd with + | _, 0, 0 -> [] + | x::xs, 0, n -> x::(sublist xs 0 (n-1)) + | x::xs, n, _ -> sublist xs (n-1) wd + | _ -> invalid_arg "sublist" + + let extract_bits e lo wd = + match e with + | Top -> Top + | Bot -> Bot + | Val v -> + let start = List.length v - lo - wd in + Val (sublist v start wd) + + (****************************************************************) + (** Expr Walk *) + (****************************************************************) + + let eval_prim f tes es st = + match f, tes, es with + | "and_bool", [], [x; y] -> and_bool x y + | "or_bool", [], [x; y] -> or_bool x y + | "eq_enum", [], [x; y] -> eq_bool x y + | "ne_enum", [], [x; y] -> ne_bool x y + | "not_bool", [], [x] -> not_bool x + + | "and_bits", [w], [x; y] -> and_bits x y + | "or_bits", [w], [x; y] -> or_bits x y + | "not_bits", [w], [x] -> not_bits x + | "eq_bits", [w], [x; y] -> eq_bits x y + | "ne_bits", [w], [x; y] -> ne_bits x y + | "eor_bits", [w], [x; y] -> eor_bits x y + + | "append_bits", [w;w'], [x; y] -> append_bits x y + + | "ZeroExtend", [w;Expr_LitInt nw], [x; y] -> + zero_extend_bits x (int_of_string nw) st + | "SignExtend", [w;Expr_LitInt nw], [x; y] -> + sign_extend_bits x (int_of_string nw) st + + | "sle_bits", [w], [x; y] -> Top + | "add_bits", [w], [x; y] -> Top + | "lsr_bits", [w;w'], [x; y] -> Top + + | _, _, _ -> + Printf.printf "unknown prim %s\n" f; + Top + + let rec eval_expr e st = + match e with + | Expr_Var (Ident "TRUE") -> Val ([ MLBDD.dtrue st.man ]) + | Expr_Var (Ident "FALSE") -> Val ([ MLBDD.dfalse st.man ]) + | Expr_LitBits b -> + Val (String.fold_right (fun c acc -> + match c with + | '1' -> (MLBDD.dtrue st.man)::acc + | '0' -> (MLBDD.dfalse st.man)::acc + | _ -> acc) b []) + | Expr_LitInt e -> Top + + | Expr_Var id -> get_var id st + + (* Simply not going to track these *) + | Expr_Field _ -> Top + | Expr_Array _ -> Top + + (* Prims *) + | Expr_TApply (FIdent (f, 0), tes, es) -> + let es = List.map (fun e -> eval_expr e st) es in + eval_prim f tes es st + | Expr_Slices(e, [Slice_LoWd(Expr_LitInt lo,Expr_LitInt wd)]) -> + let lo = int_of_string lo in + let wd = int_of_string wd in + let e = eval_expr e st in + extract_bits e lo wd + | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> + Top + + | _ -> failwith @@ "unexpected expr: " ^ (pp_expr e) + + (****************************************************************) + (** Stmt Walk *) + (****************************************************************) + + let join_imps a b = + List.filter (fun v -> List.mem v b) a + + let ctx_to_mask c = + let imps = MLBDD.allprime c in + match imps with + | x::xs -> List.fold_right join_imps xs x + | _ -> invalid_arg "ctx_to_mask" + + let clear_bits a c = + List.filter (fun (b,v) -> + if List.mem (b,v) c then false + else if List.mem (not b,v) c then false + else true) a + + + let rebuild_expr e cond st = + match cond with + | Val [cond] -> + let c = ctx_to_mask st.ctx in + let imps = MLBDD.allprime cond in + let imps = List.map (fun v -> clear_bits v c) imps in + let rebuild = List.fold_right (fun vars -> + MLBDD.dor + (List.fold_right (fun (b,v) -> + MLBDD.(dand (if b then ithvar st.man v else dnot (ithvar st.man v))) + ) vars (MLBDD.dtrue st.man)) + ) imps (MLBDD.dfalse st.man) in + let imps = MLBDD.allprime rebuild in + let masks = List.map DecoderChecks.implicant_to_mask imps in + (match masks with + | [b] -> + let bv = Value.to_mask Unknown (Value.from_maskLit b) in + sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv + | _ -> + let try2 = MLBDD.dnot cond in + (if List.length (MLBDD.allprime try2) = 1 then + Printf.printf "Neg candidate %s %s\n" (pp_expr e) (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime try2)) + else + Printf.printf "Can't simp %s %s\n" (pp_expr e) (Utils.pp_list (fun i -> i) masks)); + Printf.printf "Ctx %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime st.ctx)); + e) + | _ -> + Printf.printf "no value %s %s\n" (pp_expr e) (pp_abs cond); + e + + let rec eval_stmt s st = + match s with + | Stmt_VarDeclsNoInit(t, [v], loc) -> + let st = add_var v Bot st in + write s st + | Stmt_VarDecl(t, v, e, loc) -> + let abs = eval_expr e st in + let st = add_var v abs st in + write s st + | Stmt_ConstDecl(t, v, e, loc) -> + let abs = eval_expr e st in + let st = add_var v abs st in + write s st + | Stmt_Assign(LExpr_Var v, e, loc) -> + let abs = eval_expr e st in + let st = add_var v abs st in + write s st + + (* Eval the assert, attempt to discharge it & strengthen ctx *) + | Stmt_Assert(e, loc) -> + let abs = eval_expr e st in + if is_false abs st then st + else + let e = rebuild_expr e abs st in + let st = write (Stmt_Assert(e,loc)) st in + restrict_ctx abs st + + (* State becomes bot - unreachable *) + | Stmt_Throw _ -> + Printf.printf "%s : %s\n" (pp_stmt s) (pp_state st); + let st = write s st in + halt st + + (* If we can reduce c to true/false, collapse *) + | Stmt_If(c, tstmts, [], fstmts, loc) -> + let cond = eval_expr c st in + if is_true cond st then + eval_stmts tstmts st + else if is_false cond st then + eval_stmts fstmts st + else + let c = rebuild_expr c cond st in + let ncond = not_bool cond in + let tst = eval_stmts tstmts (restrict_ctx cond {st with stmts = []}) in + let fst = eval_stmts fstmts (restrict_ctx ncond {st with stmts = []}) in + let st' = join_state cond tst fst in + let st' = writeall st.stmts st' in + let st' = write (Stmt_If (c, tst.stmts, [], fst.stmts, loc)) st' in + st' + + (* Can't do anything here *) + | Stmt_Assign _ + | Stmt_TCall _ -> + write s st + + | _ -> failwith "unknown stmt" + + and eval_stmts stmts st = + List.fold_left (fun st s -> if MLBDD.is_false st.ctx then st else eval_stmt s st) st stmts + + let set_enc st = + let enc = Val (List.rev (List.init 32 (MLBDD.ithvar st.man))) in + {st with vars = Bindings.add (Ident "enc") enc st.vars} + + let do_transform fn stmts reach = + let st = init_state reach in + let st = set_enc st in + let st' = eval_stmts stmts st in + st'.stmts + + + let rec split_on_bit imps = + if List.length imps == 0 then begin + Printf.printf "Dead end\n"; + 1 + end + else if List.length imps == 1 then begin + Printf.printf "Match on %s\n" (match imps with [(k,e)] -> pprint_ident k | _ -> failwith "huh"); + 1 + end + else + (* rank bits by the frequency with which they are constrained *) + let bits = List.init 32 (fun i -> + let freq = List.length (List.filter (fun (k,e) -> List.exists (fun (_,j) -> i = j) e) imps) in + (i,freq)) in + let max = List.fold_right (fun (i,f) (j,m) -> if f > m then (i,f) else (j,m)) bits (-1,0) in + if fst max == -1 then begin + Printf.printf "Ended up with %s\n" (Utils.pp_list (fun (k,s) -> pprint_ident k ^ ":" ^ DecoderChecks.implicant_to_mask s) imps); + failwith "huh" + end; + let set = List.filter (fun (k,e) -> not (List.mem (false,fst max) e)) imps in + let set = List.map (fun (k,e) -> (k,List.filter (fun (f,i) -> i <> fst max) e)) set in + let clr = List.filter (fun (k,e) -> not (List.mem (true,fst max) e)) imps in + let clr = List.map (fun (k,e) -> (k,List.filter (fun (f,i) -> i <> fst max) e)) clr in + Printf.printf "Splitting on %d, sub-lists %d %d of %d\n" (fst max) (List.length set) (List.length clr) (List.length imps); + if List.length set + List.length clr <> List.length imps then begin + Printf.printf "Duplication for %s\n" (Utils.pp_list (fun (k,s) -> pprint_ident k ^ ":" ^ DecoderChecks.implicant_to_mask s) imps); + 1 + end + else begin + let d1 = split_on_bit set in + let d2 = split_on_bit clr in + 1 + (Int.max d1 d2) + end + + let transform_all instrs decoder = + let st = DecoderChecks.do_transform decoder in + (* get all prim implicants for each instruction, one list *) + let imps = Bindings.fold (fun k e acc -> + let imps = MLBDD.allprime e in + let entries = List.map (fun e -> (k,e)) imps in + acc@entries) st.instrs [] in + + let res = split_on_bit imps in + + Printf.printf "Max depth of %d\n" res; + + + Bindings.mapi (fun nm fnsig -> + let i = match nm with FIdent(s,_) -> Ident s | s -> s in + match Bindings.find_opt i st.instrs with + | Some reach -> fnsig_upd_body (fun b -> do_transform nm b reach) fnsig + | None -> fnsig) instrs + +end From 2257e8d6adbbded4c93dad947af17f6ae87a7767 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Fri, 3 May 2024 18:08:16 +1000 Subject: [PATCH 08/19] wip rt copyprop --- libASL/offline_opt.ml | 283 ++++++++++++++++++++++++++++++++++++++++++ libASL/rt_funs.ml | 26 ++++ 2 files changed, 309 insertions(+) create mode 100644 libASL/rt_funs.ml diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 87f2af3b..2b28e02e 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -325,3 +325,286 @@ module DeadContextSwitch = struct let run fn body = let (s,_) = walk_stmts body false in s end + + +module RtCopyProp = struct + type clas = + Declared | + Defined of IdentSet.t | + Clobbered | + Essential + + let pp_clas c = + match c with + | Declared -> "Declared" + | Defined ids -> "Defined (" ^ pp_identset ids ^ ")" + | Clobbered -> "Clobbered" + | Essential -> "Essential" + + let merge_clas a b = + match a, b with + | Declared, Declared -> Declared + + (* Ignore declared? *) + | Declared, Defined d + | Defined d, Declared -> Defined d + | Declared, Clobbered + | Clobbered, Declared -> Clobbered + + (* Can't drop essential though - needs to hold once set *) + | Declared, Essential + | Essential, Declared -> Essential + + (* Union deps, consider essential even if only conditional *) + | Defined d, Defined d' -> Defined (IdentSet.union d d') + | Defined _, Clobbered + | Clobbered, Defined _ -> Clobbered + | Defined _, Essential + | Essential, Defined _ -> Essential + + (* *) + | Clobbered, Clobbered -> Clobbered + | Clobbered, Essential + | Essential, Clobbered + | Essential, Essential -> Essential + + type state = { + var_clas : clas Bindings.t; + ctx : ident list; + cond_clobbered: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) + cond_dep: (Transforms.BDDSimp.abs * IdentSet.t) Bindings.t; (* binding -> condition * deps *) + bdd: Transforms.BDDSimp.state; + } + + let set_var v k st = + let var_clas = Bindings.add v k st.var_clas in + { st with var_clas } + let clobber_var v st = + + let var_clas = Bindings.map (fun c -> match c with Defined ids when IdentSet.mem v ids -> Clobbered | _ -> c) st.var_clas in + { st with var_clas } + + let get_var v st = Bindings.find_opt v st.var_clas + + let merge_st cond a b = + assert (a.ctx = b.ctx); + let ctx = a.ctx in + let merged_bdd a b = Bindings.merge (fun (k:ident) (a:Transforms.BDDSimp.abs option) (b:Transforms.BDDSimp.abs option) -> match a,b with + | Some a, Some b -> Some (Transforms.BDDSimp.join_abs cond a b) + | Some a, None -> Some a + | None, Some a -> Some a + | None, None -> None) a b in + let cond_clobbered = merged_bdd a.cond_clobbered b.cond_clobbered in + let cond_dep = Bindings.merge (fun k a b -> match a,b with + | Some (isa, a), Some (isb, b) -> Some (Transforms.BDDSimp.join_abs cond isa isb, IdentSet.union a b) + | Some a, None -> Some a + | None, Some a -> Some a + | _ -> None + ) a.cond_dep b.cond_dep in + let var_clas = Bindings.merge (fun k a b -> + match a, b with + | Some a, Some b -> Some (merge_clas a b) + | Some a, None + | None, Some a -> Some a + | None, None -> None) a.var_clas b.var_clas in + let bdd = Transforms.BDDSimp.join_state cond a.bdd b.bdd in + { bdd; var_clas ; ctx ; cond_clobbered; cond_dep } + let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; var_clas = Bindings.empty; ctx = []; cond_clobbered = Bindings.empty ; cond_dep = Bindings.empty} + let push_context m st = { st with ctx = m::st.ctx } + let peek_context st = match st.ctx with x::xs -> x | _ -> invalid_arg "peek_context" + let pop_context st = { st with ctx = (match st.ctx with x::xs -> xs | _ -> invalid_arg "pop_context") } + let has_context st = List.length st.ctx > 0 + + let decl_var v st = set_var v Declared st + let define_var v deps st = set_var v (Defined deps) st + + let read_var v (st,i) = + match get_var v st with + (* Reading undeclared generally means a value that is gradually constructed through partial updates *) + | Some (Declared) -> + (set_var v Essential st, i) + (* Reading clobbered implies we cannot reorder *) + | Some (Clobbered) -> + (set_var v Essential st, i) + (* Collect ids for transitive walk given a defined variable *) + | Some (Defined ids) -> + (st, IdentSet.union i ids) + | _ -> (st, i) + + let impure_ident = Ident "CopyProp_impure" + + let read_vars (vs: IdentSet.t) (st: state): state = + let read_set s st = IdentSet.fold read_var s (st,IdentSet.empty) in + (* If impure is in the readset, the reads are not pure. Clobber any impure dependencies now. *) + let st = if IdentSet.mem impure_ident vs then clobber_var impure_ident st else st in + (* Reading variables after they are clobbered shifts them to essential vars *) + let rec iter delta seen st = + let (st,deps) = read_set delta st in + let seen = IdentSet.union seen delta in + let delta = IdentSet.diff deps seen in + if IdentSet.cardinal delta = 0 then st + else iter delta seen st in + iter vs IdentSet.empty st + + (* TODO: Updating, check if this has some context dependence *) + let update_deps v deps st = + if has_context st then set_var v Essential st + else + match get_var v st with + | Some (Declared) -> + set_var v (Defined deps) st + | Some (Defined d') -> + set_var v (Defined (IdentSet.union deps d')) st + | _ -> st + + class deps_walker = object (self) + inherit Asl_visitor.nopAslVisitor + val mutable deps = IdentSet.empty + + method add_dep i = deps <- IdentSet.add i deps + method get_deps = deps + + method! vexpr = function + | Expr_TApply (f, _, _) when is_lit f -> + SkipChildren + | Expr_TApply (f, [], [Expr_Var v]) when is_var_load f -> + self#add_dep v; + SkipChildren + | Expr_TApply (f, [], [e;_;_]) when is_slice f -> + let _ = self#vexpr e in + SkipChildren + | Expr_TApply (f, tes, es) when is_pure_expr f -> + let _ = List.map (self#vexpr) es in + SkipChildren + | Expr_TApply (f, [], [Expr_Var a;i]) when is_array_load f -> + self#add_dep a; + SkipChildren + | Expr_TApply(f, _, es) when is_gen_call f -> + self#add_dep impure_ident; + let _ = List.map (self#vexpr) es in + SkipChildren + | e -> failwith @@ "Unknown runtime expression: " ^ (pp_expr e) + end + + let get_deps e = + let v = new deps_walker in + let _ = Asl_visitor.visit_expr v e in + v#get_deps + + let pp_state st = + pp_bindings pp_clas st.var_clas + + let pp_essential st = + pp_bindings pp_clas (Bindings.filter (fun f v -> v = Essential) st.var_clas) + + let rec walk_stmt s st = + match s with + (* Var decl *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> + decl_var v st + + (* Var assign *) + | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> + (* Collect reads and process them all *) + let deps = get_deps e in + let st = read_vars deps st in + (* Clobber anything dependent on v *) + let st = clobber_var v st in + (* Update deps for v *) + update_deps v deps st + + (* Array assign *) + | Stmt_TCall(f, [], [Expr_Var a; i; e], loc) when is_array_store f -> + (* Collect reads and process them all *) + let deps = get_deps e in + let st = read_vars deps st in + (* Clobber anything dependent on a *) + clobber_var a st + + (* Assert *) + | Stmt_TCall(f, [], [e], loc) when is_assert f -> + (* Collect reads and process them all *) + let deps = get_deps e in + read_vars deps st + + (* LiftTime branch *) + | Stmt_If(c, t, [], f, loc) -> + let tst = walk_stmts t st in + let fst = walk_stmts f st in + merge_st tst fst + + (* RunTime branch *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], [c]), loc) when is_branch f -> + (* Collect reads and process them all *) + let deps = get_deps c in + let st = read_vars deps st in + (* Push the merge point *) + push_context v st + + (* Context switch *) + | Stmt_TCall(f, [], [Expr_TApply(f2, [], [Expr_Var i])], loc) when is_context_switch f && is_merge_target f2 -> + let top = peek_context st in + if i = top then pop_context st else st + + (* Impure effect *) + | Stmt_TCall(f, _, es, loc) when is_gen_call f -> + (* Collect reads and process them all *) + let st = List.fold_right (fun e st -> + let deps = get_deps e in + read_vars deps st) es st in + (* Clobber everything linked to global state *) + clobber_var impure_ident st + + | _ -> st + + and walk_stmts s st = + List.fold_left (fun st s -> walk_stmt s st) st s + + let candidate_var v st = + match get_var v st with + | Some Essential -> false + | None -> false + | _ -> true + + (* To change this, you'd need to know : + - The condition under which its safe to copy prop + - The current reachability + + If you can't establish you are guarded, implies you need to introduce a branch. + The branch will have the outcomes of both exp reduction and maintaining the current temp. + Then need to specialise everything downstream for this point based on this introduced branch. + + This means you need to pull the condition out to the front. + Which means its needs to be fully reduced and in terms of enc. + BDD approach gives us this flexibility, every single condition in the program in terms of original enc. + Relatively simple to reduce from that point: eliminate guards based on reachability, etc. + + You can implement constant-prop and dead code in a similar fashion, as long as your notions of conditional + use / redefinition / loss of constant precision is purely in terms of the original enc. + *) + class copyprop_transform st = object + inherit Asl_visitor.nopAslVisitor + method! vexpr = function + (* Transform loads into direct variable accesses *) + | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f && candidate_var v st -> + ChangeTo (Expr_Var v) + | _ -> DoChildren + method! vstmt = function + (* Transform runtime variable decls into expression decls *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && candidate_var v st -> + ChangeDoChildrenPost(Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc), fun e -> e) + (* Transform stores into assigns *) + | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f && candidate_var v st -> + ChangeDoChildrenPost(Stmt_Assign(LExpr_Var v, e, loc), fun e -> e) + | _ -> DoChildren + end + + let run fn body = + let st = init_state in + let st = walk_stmts body st in + (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_essential st); *) + (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_state st); *) + let v = new copyprop_transform st in + Asl_visitor.visit_stmts v body + +end diff --git a/libASL/rt_funs.ml b/libASL/rt_funs.ml new file mode 100644 index 00000000..5217f13d --- /dev/null +++ b/libASL/rt_funs.ml @@ -0,0 +1,26 @@ + +open Asl_ast + +let rt_var_ty = Type_Constructor (Ident "rt_sym") +let rt_label_ty = Type_Constructor (Ident "rt_label") +let rt_expr_ty = Type_Constructor (Ident "rt_expr") + +let rt_decl_bv = FIdent("decl_bv", 0) (* string -> int -> sym *) +let rt_decl_bool = FIdent("decl_bool", 0) (* string -> sym *) +let rt_gen_bit_lit = FIdent("gen_bit_lit", 0) (* bv -> bv rt *) +let rt_gen_bool_lit = FIdent("gen_bool_lit", 0) (* bool -> bool rt *) +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_switch_context = FIdent("switch_context", 0) (* rt_label -> unit *) +let rt_gen_load = FIdent("gen_load", 0) (* sym -> 'a rt *) +let rt_gen_store = FIdent("gen_store", 0) (* sym -> 'a rt -> unit *) +let rt_gen_assert = FIdent("gen_assert", 0) (* bool rt -> unit *) + +let rt_gen_array_store = FIdent("gen_array_store", 0) (* sym -> int -> 'a rt -> unit *) +let rt_gen_array_load = FIdent("gen_array_load", 0) (* sym -> int -> 'a rt *) From 4cbba1f10a345e26528244c5c15752d15b6f209a Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Tue, 7 May 2024 17:22:42 +1000 Subject: [PATCH 09/19] use bdd lattice for clobbered & read --- libASL/offline_opt.ml | 177 ++++++++++++++++++++++++++++++++++++------ libASL/transforms.ml | 47 +++++++---- 2 files changed, 183 insertions(+), 41 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 2b28e02e..37dcab31 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -331,8 +331,8 @@ module RtCopyProp = struct type clas = Declared | Defined of IdentSet.t | - Clobbered | - Essential + Clobbered | (* means there is a clobber on at least one branch *) + Essential (* not a candidate: there is a read following a clobber or dependent on rt branch *) let pp_clas c = match c with @@ -370,19 +370,48 @@ module RtCopyProp = struct type state = { var_clas : clas Bindings.t; - ctx : ident list; + ctx : (ident * MLBDD.t) list; + (* maps idents to the condution under which they are clobbered *) cond_clobbered: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) + (* maps idents to the condition under which they are read after clobbering *) + cond_read: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) + (* not used; stores dep sets for bindings (and the def reachability) *) cond_dep: (Transforms.BDDSimp.abs * IdentSet.t) Bindings.t; (* binding -> condition * deps *) + (* the bdd context *) bdd: Transforms.BDDSimp.state; } let set_var v k st = let var_clas = Bindings.add v k st.var_clas in + let _ = match k with + | Declared -> () + | Defined x -> () + | Clobbered -> () + | Essential -> () + in { st with var_clas } - let clobber_var v st = + + let cond_merge al bl = Bindings.merge (fun i a b -> match a,b with + | Some a, Some b -> Some (Transforms.BDDSimp.or_bits a b) + | Some a, _ -> Some a + | _ , Some b -> Some b + | _ -> None) al bl + + let add_cond i c bs = Bindings.add i (match (Bindings.find_opt i bs) with + | Some x -> (Transforms.BDDSimp.or_bits c x) + | None -> c + ) bs + + let add_conds is c bs = cond_merge bs (Seq.map (fun i -> i, c) is |> Bindings.of_seq) + + let clobber_var v st = let var_clas = Bindings.map (fun c -> match c with Defined ids when IdentSet.mem v ids -> Clobbered | _ -> c) st.var_clas in - { st with var_clas } + (* TODO: should clobbering transitive?*) + let deps = Bindings.filter_map (fun i c -> match c with Defined ids when IdentSet.mem v ids -> + Some (Transforms.BDDSimp.Val [st.bdd.ctx]) | _ -> None) st.var_clas in + let cond_clobbered = cond_merge st.cond_clobbered deps in + { st with var_clas ; cond_clobbered } let get_var v st = Bindings.find_opt v st.var_clas @@ -395,6 +424,7 @@ module RtCopyProp = struct | None, Some a -> Some a | None, None -> None) a b in let cond_clobbered = merged_bdd a.cond_clobbered b.cond_clobbered in + let cond_read = merged_bdd a.cond_read b.cond_read in let cond_dep = Bindings.merge (fun k a b -> match a,b with | Some (isa, a), Some (isb, b) -> Some (Transforms.BDDSimp.join_abs cond isa isb, IdentSet.union a b) | Some a, None -> Some a @@ -408,24 +438,49 @@ module RtCopyProp = struct | None, Some a -> Some a | None, None -> None) a.var_clas b.var_clas in let bdd = Transforms.BDDSimp.join_state cond a.bdd b.bdd in - { bdd; var_clas ; ctx ; cond_clobbered; cond_dep } - let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; var_clas = Bindings.empty; ctx = []; cond_clobbered = Bindings.empty ; cond_dep = Bindings.empty} + { bdd; var_clas ; ctx ; cond_clobbered; cond_read; cond_dep } + let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; + var_clas = Bindings.empty; ctx = []; + cond_clobbered = Bindings.empty ; + cond_read = Bindings.empty ; + cond_dep = Bindings.empty} let push_context m st = { st with ctx = m::st.ctx } let peek_context st = match st.ctx with x::xs -> x | _ -> invalid_arg "peek_context" - let pop_context st = { st with ctx = (match st.ctx with x::xs -> xs | _ -> invalid_arg "pop_context") } + let pop_context st = let (i,c),tl = (match st.ctx with x::xs -> x,xs | _ -> invalid_arg "pop_context") in + { st with ctx = tl ; bdd = {st.bdd with ctx = c} } let has_context st = List.length st.ctx > 0 let decl_var v st = set_var v Declared st - let define_var v deps st = set_var v (Defined deps) st + let define_var v deps st = + let r = set_var v (Defined deps) st in + let cond_dep = Bindings.find_opt v st.cond_dep |> + Option.map (fun (c,b) -> Transforms.BDDSimp.or_bits c (Transforms.BDDSimp.Val [st.bdd.ctx]), IdentSet.union b deps) |> + function + | Some c -> Bindings.add v c st.cond_dep + | None -> st.cond_dep + in + {r with cond_dep } + + + type xform = + | Prop + | PropCond of MLBDD.t * MLBDD.t + | No let read_var v (st,i) = + (* record read reachability *) + let st = {st with cond_read = (add_cond v (Val [st.bdd.ctx]) st.cond_read)} in match get_var v st with (* Reading undeclared generally means a value that is gradually constructed through partial updates *) | Some (Declared) -> (set_var v Essential st, i) (* Reading clobbered implies we cannot reorder *) | Some (Clobbered) -> - (set_var v Essential st, i) + (* TODO: only record read ctx in when read is subsequent to clobber; ie we are conditionally essential *) + let clobbered = (match (Bindings.find_opt v st.cond_clobbered) with + | Some x -> Transforms.BDDSimp.is_true x st.bdd + | None -> failwith "unreachable?") + in if clobbered then (set_var v Essential st, i) else st, i (* Collect ids for transitive walk given a defined variable *) | Some (Defined ids) -> (st, IdentSet.union i ids) @@ -448,7 +503,7 @@ module RtCopyProp = struct (* TODO: Updating, check if this has some context dependence *) let update_deps v deps st = - if has_context st then set_var v Essential st + if has_context st then set_var v Essential st (* cannot copy-prop exprs dependent on a run-time branch*) else match get_var v st with | Some (Declared) -> @@ -498,10 +553,14 @@ module RtCopyProp = struct pp_bindings pp_clas (Bindings.filter (fun f v -> v = Essential) st.var_clas) let rec walk_stmt s st = + let eval_post s st = {st with bdd = Transforms.BDDSimp.eval_stmt Transforms.BDDSimp.nop_transform s st.bdd } in match s with (* Var decl *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> - decl_var v st + decl_var v st + |> eval_post s + + (* Var assign *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> @@ -512,6 +571,7 @@ module RtCopyProp = struct let st = clobber_var v st in (* Update deps for v *) update_deps v deps st + |> eval_post s (* Array assign *) | Stmt_TCall(f, [], [Expr_Var a; i; e], loc) when is_array_store f -> @@ -520,18 +580,27 @@ module RtCopyProp = struct let st = read_vars deps st in (* Clobber anything dependent on a *) clobber_var a st + |> eval_post s (* Assert *) | Stmt_TCall(f, [], [e], loc) when is_assert f -> (* Collect reads and process them all *) let deps = get_deps e in read_vars deps st + |> eval_post s (* LiftTime branch *) | Stmt_If(c, t, [], f, loc) -> - let tst = walk_stmts t st in - let fst = walk_stmts f st in - merge_st tst fst + (* merge in the bdds as well *) + let cond = Transforms.BDDSimp.eval_expr c st.bdd in + let c = Transforms.BDDSimp.rebuild_expr c cond st.bdd in + let ncond = Transforms.BDDSimp.not_bool cond in + let tst:state = walk_stmts t {st with bdd = (Transforms.BDDSimp.restrict_ctx cond {st.bdd with stmts = []})} in + let fst:state = walk_stmts f {st with bdd = (Transforms.BDDSimp.restrict_ctx ncond {st.bdd with stmts = []})} in + let st': state = merge_st cond tst fst in + let st'= {st' with bdd = Transforms.BDDSimp.writeall st.bdd.stmts st'.bdd} in + let st' = {st' with bdd = Transforms.BDDSimp.write (Stmt_If (c, tst.bdd.stmts, [], fst.bdd.stmts, loc)) st'.bdd} in + st' (* RunTime branch *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], [c]), loc) when is_branch f -> @@ -539,12 +608,14 @@ module RtCopyProp = struct let deps = get_deps c in let st = read_vars deps st in (* Push the merge point *) - push_context v st + push_context (v, st.bdd.ctx) st + |> eval_post s (* Context switch *) | Stmt_TCall(f, [], [Expr_TApply(f2, [], [Expr_Var i])], loc) when is_context_switch f && is_merge_target f2 -> - let top = peek_context st in - if i = top then pop_context st else st + let top = fst (peek_context st) in + if i = top then ((pop_context st)) else st + |> eval_post s (* Impure effect *) | Stmt_TCall(f, _, es, loc) when is_gen_call f -> @@ -554,10 +625,11 @@ module RtCopyProp = struct read_vars deps st) es st in (* Clobber everything linked to global state *) clobber_var impure_ident st + |> eval_post s - | _ -> st + | v -> eval_post v st - and walk_stmts s st = + and walk_stmts s st : state = List.fold_left (fun st s -> walk_stmt s st) st s let candidate_var v st = @@ -599,12 +671,69 @@ module RtCopyProp = struct | _ -> DoChildren end - let run fn body = - let st = init_state in + (* + Decl of candidate -> decl of expr ref + decl of tmp (unless its never clobbered) + Write to candidate -> if !clobbered, write to expr ref, else write to tmp + Read of candidate -> Wrap whole statement in same test, read from appropriate var + *) + let cond_candidate v st rtst = + match get_var v st with + | Some Essential -> No + | Some Clobbered -> let c = Bindings.find_opt v st.cond_clobbered in + (match c with + | Some x -> + if (Transforms.BDDSimp.is_true x rtst) then No else (No) + | None -> No) + | None -> Prop + | _ -> Prop + + + (* + + Cond proped = + + clobber reachable && read reachable ==> doesn't exclude clobber is subsequent to read + + *) + + + class cond_copyprop_transform cpst = object(self) + inherit Asl_visitor.nopAslVisitor + val mutable rtst = None + + method xf_stmt (x:stmt) (st:Transforms.BDDSimp.state) = + rtst <- Some st; Asl_visitor.visit_stmt self x + + method! vexpr = function + (* Transform loads into direct variable accesses *) + | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f && Prop = (cond_candidate v cpst (Option.get rtst)) -> + ChangeTo (Expr_Var v) + | _ -> DoChildren + + method! vstmt = function + (* Transform runtime variable decls into expression decls *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && Prop = (cond_candidate v cpst (Option.get rtst)) -> + ChangeDoChildrenPost(Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc), fun e -> e) + (* Transform stores into assigns *) + | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f && Prop = (cond_candidate v cpst (Option.get rtst)) -> + ChangeDoChildrenPost(Stmt_Assign(LExpr_Var v, e, loc), fun e -> e) + | _ -> DoChildren + end + + let do_transform reachable copyprop_st stmts = + (* apply BDD AI a second time to compare reachability with candidates in analysis pass *) + let st = Transforms.BDDSimp.init_state reachable in + let st = Transforms.BDDSimp.set_enc st in + let st' = Transforms.BDDSimp.eval_stmts (copyprop_st) stmts st in + st'.stmts + + + let run reachable fn body = + let st = init_state reachable in let st = walk_stmts body st in (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_essential st); *) (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_state st); *) - let v = new copyprop_transform st in - Asl_visitor.visit_stmts v body + let v = new cond_copyprop_transform st in + do_transform reachable v body end diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 460b1c54..20e7597a 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -1786,13 +1786,14 @@ module FixRedefinitions = struct this#add_bind b; DoChildren | Stmt_If (c, t, els, e, loc) -> let c' = visit_expr this c in - this#push_scope () ; + (* Don't push or pop scopes anymore so that variables are also unique across branches *) + (*this#push_scope () ; *) let t' = visit_stmts this t in - this#pop_scope (); this#push_scope () ; + (*this#pop_scope (); this#push_scope () ; *) let els' = mapNoCopy (visit_s_elsif this ) els in - this#pop_scope (); this#push_scope () ; + (*this#pop_scope (); this#push_scope () ; *) let e' = visit_stmts this e in - this#pop_scope (); + (*this#pop_scope (); *) ChangeTo (Stmt_If (c', t', els', e', loc)) (* Statements with child scopes that shouldn't appear towards the end of transform pipeline *) | Stmt_Case _ -> failwith "(FixRedefinitions) case not expected" @@ -2053,7 +2054,9 @@ module DecoderChecks = struct end + module BDDSimp = struct + type abs = Top | Val of MLBDD.t list | @@ -2360,23 +2363,31 @@ module BDDSimp = struct Printf.printf "no value %s %s\n" (pp_expr e) (pp_abs cond); e - let rec eval_stmt s st = + + class nopvis = object(self) + method xf_stmt (x:stmt) (st:state) = x + end + + let nop_transform = new nopvis + + let rec eval_stmt xf s st = + let ns = xf#xf_stmt s st in match s with | Stmt_VarDeclsNoInit(t, [v], loc) -> let st = add_var v Bot st in - write s st + write ns st | Stmt_VarDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write s st + write ns st | Stmt_ConstDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write s st + write ns st | Stmt_Assign(LExpr_Var v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write s st + write ns st (* Eval the assert, attempt to discharge it & strengthen ctx *) | Stmt_Assert(e, loc) -> @@ -2390,21 +2401,21 @@ module BDDSimp = struct (* State becomes bot - unreachable *) | Stmt_Throw _ -> Printf.printf "%s : %s\n" (pp_stmt s) (pp_state st); - let st = write s st in + let st = write ns st in halt st (* If we can reduce c to true/false, collapse *) | Stmt_If(c, tstmts, [], fstmts, loc) -> let cond = eval_expr c st in if is_true cond st then - eval_stmts tstmts st + eval_stmts xf tstmts st else if is_false cond st then - eval_stmts fstmts st + eval_stmts xf fstmts st else let c = rebuild_expr c cond st in let ncond = not_bool cond in - let tst = eval_stmts tstmts (restrict_ctx cond {st with stmts = []}) in - let fst = eval_stmts fstmts (restrict_ctx ncond {st with stmts = []}) in + let tst = eval_stmts xf tstmts (restrict_ctx cond {st with stmts = []}) in + let fst = eval_stmts xf fstmts (restrict_ctx ncond {st with stmts = []}) in let st' = join_state cond tst fst in let st' = writeall st.stmts st' in let st' = write (Stmt_If (c, tst.stmts, [], fst.stmts, loc)) st' in @@ -2417,17 +2428,19 @@ module BDDSimp = struct | _ -> failwith "unknown stmt" - and eval_stmts stmts st = - List.fold_left (fun st s -> if MLBDD.is_false st.ctx then st else eval_stmt s st) st stmts + and eval_stmts xf stmts st = + List.fold_left (fun st s -> if MLBDD.is_false st.ctx then st else eval_stmt xf s st) st stmts let set_enc st = let enc = Val (List.rev (List.init 32 (MLBDD.ithvar st.man))) in {st with vars = Bindings.add (Ident "enc") enc st.vars} + + let do_transform fn stmts reach = let st = init_state reach in let st = set_enc st in - let st' = eval_stmts stmts st in + let st' = eval_stmts (new nopvis) stmts st in st'.stmts From 861df1938795dcccfa09556a5b2add079a060bda Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 8 May 2024 11:45:53 +1000 Subject: [PATCH 10/19] refac --- libASL/offline_opt.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 37dcab31..76e59f3d 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -377,7 +377,7 @@ module RtCopyProp = struct cond_read: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) (* not used; stores dep sets for bindings (and the def reachability) *) cond_dep: (Transforms.BDDSimp.abs * IdentSet.t) Bindings.t; (* binding -> condition * deps *) - (* the bdd context *) + (**) bdd: Transforms.BDDSimp.state; } @@ -560,8 +560,6 @@ module RtCopyProp = struct decl_var v st |> eval_post s - - (* Var assign *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> (* Collect reads and process them all *) @@ -700,24 +698,30 @@ module RtCopyProp = struct class cond_copyprop_transform cpst = object(self) inherit Asl_visitor.nopAslVisitor val mutable rtst = None + val mutable candidates : expr Bindings.t = Bindings.empty method xf_stmt (x:stmt) (st:Transforms.BDDSimp.state) = rtst <- Some st; Asl_visitor.visit_stmt self x + method candidate v = (Prop = (cond_candidate v cpst (Option.get rtst))) + method essential v = (No = (cond_candidate v cpst (Option.get rtst))) + method! vexpr = function (* Transform loads into direct variable accesses *) - | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f && Prop = (cond_candidate v cpst (Option.get rtst)) -> + | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f && (self#candidate v) -> ChangeTo (Expr_Var v) | _ -> DoChildren - method! vstmt = function + method vvisit_stmt : stmt -> stmt list = function (* Transform runtime variable decls into expression decls *) - | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && Prop = (cond_candidate v cpst (Option.get rtst)) -> - ChangeDoChildrenPost(Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc), fun e -> e) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && (self#essential v) -> + [Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc)] + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && not (self#essential v) -> + [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [v], loc)] (* Transform stores into assigns *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f && Prop = (cond_candidate v cpst (Option.get rtst)) -> - ChangeDoChildrenPost(Stmt_Assign(LExpr_Var v, e, loc), fun e -> e) - | _ -> DoChildren + [(Stmt_Assign (LExpr_Var v, e, loc))] + | _ -> [] end let do_transform reachable copyprop_st stmts = From ca20b600f460e3cdbe050a415009f7cb89dfbd88 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 8 May 2024 14:39:40 +1000 Subject: [PATCH 11/19] untested xform to ternary --- libASL/offline_opt.ml | 96 ++++++++++++++++++++++++++++++--------- libASL/symbolic_lifter.ml | 6 ++- libASL/transforms.ml | 42 +++++++++++++---- 3 files changed, 112 insertions(+), 32 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 76e59f3d..0880b649 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -464,7 +464,7 @@ module RtCopyProp = struct type xform = | Prop - | PropCond of MLBDD.t * MLBDD.t + | PropCond of MLBDD.t * MLBDD.t (* copyprop not allowed , should copyprop *) | No let read_var v (st,i) = @@ -651,6 +651,9 @@ module RtCopyProp = struct You can implement constant-prop and dead code in a similar fashion, as long as your notions of conditional use / redefinition / loss of constant precision is purely in terms of the original enc. + +statement s is the only definition of x reaching u
on every path from s to u there are no assignments to y
 + *) class copyprop_transform st = object inherit Asl_visitor.nopAslVisitor @@ -662,10 +665,10 @@ module RtCopyProp = struct method! vstmt = function (* Transform runtime variable decls into expression decls *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && candidate_var v st -> - ChangeDoChildrenPost(Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc), fun e -> e) + ChangeDoChildrenPost([Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc)], fun e -> e) (* Transform stores into assigns *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f && candidate_var v st -> - ChangeDoChildrenPost(Stmt_Assign(LExpr_Var v, e, loc), fun e -> e) + ChangeDoChildrenPost([Stmt_Assign(LExpr_Var v, e, loc)], fun e -> e) | _ -> DoChildren end @@ -688,40 +691,90 @@ module RtCopyProp = struct (* - Cond proped = - - clobber reachable && read reachable ==> doesn't exclude clobber is subsequent to read *) + let cp_idents = function + | Ident c -> Ident (c ^ "_nocopyprop") , Ident (c ^ "_copyprop") + | _ -> failwith "only copyprop vars" + + type cand = { + typ: ty + } + class cond_copyprop_transform cpst = object(self) inherit Asl_visitor.nopAslVisitor val mutable rtst = None - val mutable candidates : expr Bindings.t = Bindings.empty - method xf_stmt (x:stmt) (st:Transforms.BDDSimp.state) = + val mutable candidates : cand Bindings.t = Bindings.empty + + method xf_stmt (x:stmt) (st:Transforms.BDDSimp.state) : stmt list = rtst <- Some st; Asl_visitor.visit_stmt self x method candidate v = (Prop = (cond_candidate v cpst (Option.get rtst))) method essential v = (No = (cond_candidate v cpst (Option.get rtst))) - method! vexpr = function - (* Transform loads into direct variable accesses *) - | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f && (self#candidate v) -> - ChangeTo (Expr_Var v) - | _ -> DoChildren + method! vstmt s = ChangeDoChildrenPost (self#stmt_xform s, fun x -> x) + method! vexpr e = ChangeDoChildrenPost (self#expr_xform e, fun x -> x) - method vvisit_stmt : stmt -> stmt list = function + (* + For run-time variables that we have determined we can copyprop, + pull them to lift-time variables so they can be conditionally + copy-propagated at lift time. + *) + method stmt_xform (s : stmt) : stmt list = match s with (* Transform runtime variable decls into expression decls *) - | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && (self#essential v) -> - [Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc)] - | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && not (self#essential v) -> - [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [v], loc)] + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> + candidates <- Bindings.add v {typ=t} candidates; + (match (cond_candidate v cpst (Option.get rtst)) with + (* essential, leave as-is *) + | No -> [s] + (* move run-time to lift-time *) + | Prop -> [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [v], loc)] + | PropCond _ -> let ncp,cp = cp_idents v in + (* lift-time conditionally generates the copy-propagated or non-propagated form *) + [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [ncp], loc); + Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], loc)] + ) (* Transform stores into assigns *) - | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f && Prop = (cond_candidate v cpst (Option.get rtst)) -> - [(Stmt_Assign (LExpr_Var v, e, loc))] + | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> + (match (cond_candidate v cpst (Option.get rtst)) with + | No -> [s] + | Prop -> [(Stmt_Assign (LExpr_Var v, e, loc))] + | PropCond (no,yes) -> let nocp,cp = cp_idents v in + (* + - if copy-prop'ed form is reachable then generate a store statement + - if non-copyprop'ed form is reachable then generate an assignment statement + *) + (* can re-evaluating an expression have side effects? *) + (if (Transforms.BDDSimp.is_true (Val [no]) (Option.get rtst)) + then [Stmt_TCall(f, [], [Expr_Var nocp; e], loc)] (* gen store to rt variable *) + else []) + @ + (if (Transforms.BDDSimp.is_true (Val [yes]) (Option.get rtst)) + then [Stmt_Assign(LExpr_Var cp, e, loc)] (* assign to rt variable for copyprop *) + else []) + ) | _ -> [] + + method expr_xform (e:expr) : expr = match e with + | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f -> + (match (cond_candidate v cpst (Option.get rtst)) with + | No -> e + | Prop -> Expr_Var v + | PropCond (nocpcond,yescpcond) -> let ncp,cp = cp_idents v in + let load = Expr_TApply(f, [], [Expr_Var ncp]) in + let prop = Expr_Var cp in + let bdd_to_cond c = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (Val [c]) (Option.get rtst) in + let nocpcond = bdd_to_cond nocpcond in + let yescpcond = bdd_to_cond yescpcond in + let vt = Bindings.find v candidates in + (* TODO: would be good to check that yes and no are disjoint *) + let e = Expr_If (vt.typ, yescpcond, prop, [E_Elsif_Cond (nocpcond, load)], e (* should be unreachable *)) in + e + ) + | _ -> e end let do_transform reachable copyprop_st stmts = @@ -731,8 +784,7 @@ module RtCopyProp = struct let st' = Transforms.BDDSimp.eval_stmts (copyprop_st) stmts st in st'.stmts - - let run reachable fn body = + let run fn reachable body = let st = init_state reachable in let st = walk_stmts body st in (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_essential st); *) diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index fa51d26a..54f97d41 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -370,7 +370,8 @@ let run include_pc iset pat env = Printf.printf " Succeeded for %d instructions\n\n" (Bindings.cardinal fns); let decoder = Eval.Env.getDecoder env (Ident iset) in - let fns = Transforms.BDDSimp.transform_all fns decoder in + let decoderst : Transforms.DecoderChecks.st = Transforms.DecoderChecks.do_transform decoder in + let fns = Transforms.BDDSimp.transform_all fns decoderst in let (_,globals) = Dis.build_env env in let fns = Bindings.map (fnsig_upd_body (Transforms.RemoveUnused.remove_unused globals)) fns in @@ -390,6 +391,9 @@ let run include_pc iset pat env = 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 offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (Bindings.find k decoderst.instrs) )) offline_fns in + let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in Printf.printf "\n"; diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 20e7597a..d54c97ec 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2049,7 +2049,7 @@ module DecoderChecks = struct (st,prior) ) (st,st.cur_enc) alts in st - let do_transform d = + let do_transform d : st = tf_decoder d init_state end @@ -2333,6 +2333,31 @@ module BDDSimp = struct else true) a + let bdd_to_expr cond st = + let c = ctx_to_mask st.ctx in + let imps = MLBDD.allprime cond in + let imps = List.map (fun v -> clear_bits v c) imps in + let rebuild = List.fold_right (fun vars -> + MLBDD.dor + (List.fold_right (fun (b,v) -> + MLBDD.(dand (if b then ithvar st.man v else dnot (ithvar st.man v))) + ) vars (MLBDD.dtrue st.man)) + ) imps (MLBDD.dfalse st.man) in + let imps = MLBDD.allprime rebuild in + let masks = List.map DecoderChecks.implicant_to_mask imps in + (match masks with + | [b] -> + let bv = Value.to_mask Unknown (Value.from_maskLit b) in + sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv + | _ -> + let try2 = MLBDD.dnot cond in + (if List.length (MLBDD.allprime try2) = 1 then + Printf.printf "Neg candidate %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime try2)) + else + Printf.eprintf "Can't simp %s\n" (Utils.pp_list (fun i -> i) masks)); + failwith (Printf.sprintf "Ctx %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime st.ctx)))) + + let rebuild_expr e cond st = match cond with | Val [cond] -> @@ -2365,7 +2390,7 @@ module BDDSimp = struct class nopvis = object(self) - method xf_stmt (x:stmt) (st:state) = x + method xf_stmt (x:stmt) (st:state) : stmt list = [x] end let nop_transform = new nopvis @@ -2375,19 +2400,19 @@ module BDDSimp = struct match s with | Stmt_VarDeclsNoInit(t, [v], loc) -> let st = add_var v Bot st in - write ns st + writeall ns st | Stmt_VarDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write ns st + writeall ns st | Stmt_ConstDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write ns st + writeall ns st | Stmt_Assign(LExpr_Var v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write ns st + writeall ns st (* Eval the assert, attempt to discharge it & strengthen ctx *) | Stmt_Assert(e, loc) -> @@ -2401,7 +2426,7 @@ module BDDSimp = struct (* State becomes bot - unreachable *) | Stmt_Throw _ -> Printf.printf "%s : %s\n" (pp_stmt s) (pp_state st); - let st = write ns st in + let st = writeall ns st in halt st (* If we can reduce c to true/false, collapse *) @@ -2478,8 +2503,7 @@ module BDDSimp = struct 1 + (Int.max d1 d2) end - let transform_all instrs decoder = - let st = DecoderChecks.do_transform decoder in + let transform_all instrs (st:DecoderChecks.st)= (* get all prim implicants for each instruction, one list *) let imps = Bindings.fold (fun k e acc -> let imps = MLBDD.allprime e in From 2a5f3c0544f02246fe70bb26ff327fe639818d1d Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 8 May 2024 18:23:01 +1000 Subject: [PATCH 12/19] not working --- bin/asli.ml | 4 +- libASL/ocaml_backend.ml | 1 + libASL/offline_opt.ml | 103 +++++++++++++++++++------------------- libASL/symbolic_lifter.ml | 11 +++- libASL/transforms.ml | 6 +-- 5 files changed, 69 insertions(+), 56 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index 6b3249ce..3694fd48 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -29,7 +29,9 @@ let opt_verbose = ref false let opt_debug_level = ref (-1) -let () = Printexc.register_printer +let () = + Printexc.record_backtrace true ; + Printexc.register_printer (function | Value.EvalError (loc, msg) -> Some (Printf.sprintf "EvalError at %s: %s" (pp_loc loc) msg) diff --git a/libASL/ocaml_backend.ml b/libASL/ocaml_backend.ml index 9eb7cc87..a492897a 100644 --- a/libASL/ocaml_backend.ml +++ b/libASL/ocaml_backend.ml @@ -133,6 +133,7 @@ let rec prints_expr e st = | Expr_LitString s -> "\"" ^ s ^ "\"" | Expr_Tuple(es) -> "(" ^ (String.concat "," (List.map (fun e -> prints_expr e st) es)) ^ ")" | Expr_Unknown(ty) -> default_value ty st + | Expr_If (ty, c, t, [], e) -> Printf.sprintf "(if (%s) then (%s) else (%s))" (prints_expr c st) (prints_expr t st) (prints_expr e st) | _ -> failwith @@ "prints_expr: " ^ pp_expr e diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 0880b649..41b771e3 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -180,7 +180,7 @@ module CopyProp = struct self#add_dep impure_ident; let _ = List.map (self#vexpr) es in SkipChildren - | e -> failwith @@ "Unknown runtime expression: " ^ (pp_expr e) + | e -> (Printf.printf "Unknown runtime expression: %s\n" (pp_expr e)); DoChildren end let get_deps e = @@ -374,7 +374,7 @@ module RtCopyProp = struct (* maps idents to the condution under which they are clobbered *) cond_clobbered: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) (* maps idents to the condition under which they are read after clobbering *) - cond_read: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) + cond_read_after_clobber: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) (* not used; stores dep sets for bindings (and the def reachability) *) cond_dep: (Transforms.BDDSimp.abs * IdentSet.t) Bindings.t; (* binding -> condition * deps *) (**) @@ -416,7 +416,6 @@ module RtCopyProp = struct let get_var v st = Bindings.find_opt v st.var_clas let merge_st cond a b = - assert (a.ctx = b.ctx); let ctx = a.ctx in let merged_bdd a b = Bindings.merge (fun (k:ident) (a:Transforms.BDDSimp.abs option) (b:Transforms.BDDSimp.abs option) -> match a,b with | Some a, Some b -> Some (Transforms.BDDSimp.join_abs cond a b) @@ -424,7 +423,7 @@ module RtCopyProp = struct | None, Some a -> Some a | None, None -> None) a b in let cond_clobbered = merged_bdd a.cond_clobbered b.cond_clobbered in - let cond_read = merged_bdd a.cond_read b.cond_read in + let cond_read_after_clobber = merged_bdd a.cond_read_after_clobber b.cond_read_after_clobber in let cond_dep = Bindings.merge (fun k a b -> match a,b with | Some (isa, a), Some (isb, b) -> Some (Transforms.BDDSimp.join_abs cond isa isb, IdentSet.union a b) | Some a, None -> Some a @@ -438,11 +437,11 @@ module RtCopyProp = struct | None, Some a -> Some a | None, None -> None) a.var_clas b.var_clas in let bdd = Transforms.BDDSimp.join_state cond a.bdd b.bdd in - { bdd; var_clas ; ctx ; cond_clobbered; cond_read; cond_dep } + { bdd; var_clas ; ctx ; cond_clobbered; cond_read_after_clobber; cond_dep } let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; var_clas = Bindings.empty; ctx = []; cond_clobbered = Bindings.empty ; - cond_read = Bindings.empty ; + cond_read_after_clobber = Bindings.empty ; cond_dep = Bindings.empty} let push_context m st = { st with ctx = m::st.ctx } let peek_context st = match st.ctx with x::xs -> x | _ -> invalid_arg "peek_context" @@ -461,26 +460,24 @@ module RtCopyProp = struct in {r with cond_dep } - type xform = | Prop - | PropCond of MLBDD.t * MLBDD.t (* copyprop not allowed , should copyprop *) + | PropCond of Transforms.BDDSimp.abs (* copyprop not allowed , should copyprop *) | No let read_var v (st,i) = - (* record read reachability *) - let st = {st with cond_read = (add_cond v (Val [st.bdd.ctx]) st.cond_read)} in match get_var v st with (* Reading undeclared generally means a value that is gradually constructed through partial updates *) | Some (Declared) -> (set_var v Essential st, i) (* Reading clobbered implies we cannot reorder *) - | Some (Clobbered) -> - (* TODO: only record read ctx in when read is subsequent to clobber; ie we are conditionally essential *) - let clobbered = (match (Bindings.find_opt v st.cond_clobbered) with - | Some x -> Transforms.BDDSimp.is_true x st.bdd - | None -> failwith "unreachable?") - in if clobbered then (set_var v Essential st, i) else st, i + | Some (Clobbered) -> ( + (* record read reachability *) + let clobbered = (Bindings.find v st.cond_clobbered) in + let read_after_clobber = Transforms.BDDSimp.and_bits clobbered (Val [st.bdd.ctx]) in + let st = {st with cond_read_after_clobber = (add_cond v read_after_clobber st.cond_read_after_clobber)} in + st, i ) + (*if (Transforms.BDDSimp.is_true clobbered st.bdd) then (set_var v Essential st, i) else st, i) *) (* Collect ids for transitive walk given a defined variable *) | Some (Defined ids) -> (st, IdentSet.union i ids) @@ -538,7 +535,7 @@ module RtCopyProp = struct self#add_dep impure_ident; let _ = List.map (self#vexpr) es in SkipChildren - | e -> failwith @@ "Unknown runtime expression: " ^ (pp_expr e) + | e -> (Printf.printf "Unknown runtime expression: %s\n" (pp_expr e)); DoChildren end let get_deps e = @@ -672,27 +669,21 @@ statement s is the only definition of x reaching u
on every path from s to u t | _ -> DoChildren end + (* - Decl of candidate -> decl of expr ref + decl of tmp (unless its never clobbered) - Write to candidate -> if !clobbered, write to expr ref, else write to tmp - Read of candidate -> Wrap whole statement in same test, read from appropriate var + variable is not clobbered then read *) let cond_candidate v st rtst = match get_var v st with | Some Essential -> No - | Some Clobbered -> let c = Bindings.find_opt v st.cond_clobbered in + | Some Clobbered -> + let c = Bindings.find_opt v st.cond_read_after_clobber in (match c with - | Some x -> - if (Transforms.BDDSimp.is_true x rtst) then No else (No) + | Some x -> PropCond x | None -> No) - | None -> Prop - | _ -> Prop - - - (* - - - *) + | Some Defined _ -> Prop + | Some Declared -> No + | None -> No let cp_idents = function @@ -718,12 +709,21 @@ statement s is the only definition of x reaching u
on every path from s to u t method! vstmt s = ChangeDoChildrenPost (self#stmt_xform s, fun x -> x) method! vexpr e = ChangeDoChildrenPost (self#expr_xform e, fun x -> x) + + (* + Decl of candidate -> decl of expr ref + decl of tmp (unless its never clobbered) + Write to candidate -> if !clobbered, write to expr ref, else write to tmp + Read of candidate -> Wrap whole statement in same test, read from appropriate var + *) + (* For run-time variables that we have determined we can copyprop, pull them to lift-time variables so they can be conditionally copy-propagated at lift time. *) - method stmt_xform (s : stmt) : stmt list = match s with + method stmt_xform (s : stmt) : stmt list = + let cp_cond c = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (c) (Option.get rtst) in + match s with (* Transform runtime variable decls into expression decls *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> candidates <- Bindings.add v {typ=t} candidates; @@ -732,46 +732,47 @@ statement s is the only definition of x reaching u
on every path from s to u t | No -> [s] (* move run-time to lift-time *) | Prop -> [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [v], loc)] - | PropCond _ -> let ncp,cp = cp_idents v in + | PropCond cond -> let ncp,cp = cp_idents v in + let c = cp_cond cond in + let rt_decl = Stmt_If (c, [], [] , [Stmt_Assign (LExpr_Var ncp, Expr_TApply(f, [], args), Unknown)], Unknown) in (* lift-time conditionally generates the copy-propagated or non-propagated form *) - [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [ncp], loc); - Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], loc)] + [ + Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [ncp], loc); + Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], loc); + rt_decl + ] ) (* Transform stores into assigns *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> (match (cond_candidate v cpst (Option.get rtst)) with | No -> [s] | Prop -> [(Stmt_Assign (LExpr_Var v, e, loc))] - | PropCond (no,yes) -> let nocp,cp = cp_idents v in + | PropCond cond -> let nocp,cp = cp_idents v in (* - if copy-prop'ed form is reachable then generate a store statement - if non-copyprop'ed form is reachable then generate an assignment statement *) (* can re-evaluating an expression have side effects? *) - (if (Transforms.BDDSimp.is_true (Val [no]) (Option.get rtst)) - then [Stmt_TCall(f, [], [Expr_Var nocp; e], loc)] (* gen store to rt variable *) - else []) - @ - (if (Transforms.BDDSimp.is_true (Val [yes]) (Option.get rtst)) - then [Stmt_Assign(LExpr_Var cp, e, loc)] (* assign to rt variable for copyprop *) - else []) - ) - | _ -> [] + + let gen_store_rt_var = Stmt_TCall(f, [], [Expr_Var nocp; e], loc) in + let assign_lt_var = Stmt_Assign(LExpr_Var cp, e, loc) in + (* TODO: could further narrow cases here using bdd*) + [Stmt_If ( cp_cond cond, [gen_store_rt_var], [], [assign_lt_var], Unknown)] + ) + | _ -> [s] method expr_xform (e:expr) : expr = match e with | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f -> (match (cond_candidate v cpst (Option.get rtst)) with | No -> e | Prop -> Expr_Var v - | PropCond (nocpcond,yescpcond) -> let ncp,cp = cp_idents v in + | PropCond cpcond -> let ncp,cp = cp_idents v in let load = Expr_TApply(f, [], [Expr_Var ncp]) in let prop = Expr_Var cp in - let bdd_to_cond c = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (Val [c]) (Option.get rtst) in - let nocpcond = bdd_to_cond nocpcond in - let yescpcond = bdd_to_cond yescpcond in + let yescpcond = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) cpcond (Option.get rtst) in let vt = Bindings.find v candidates in - (* TODO: would be good to check that yes and no are disjoint *) - let e = Expr_If (vt.typ, yescpcond, prop, [E_Elsif_Cond (nocpcond, load)], e (* should be unreachable *)) in + (* TODO: might be good to check that yes and no are disjoint here *) + let e = Expr_If (vt.typ, yescpcond, prop, [] , load) in e ) | _ -> e diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 54f97d41..09b62f9f 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -392,7 +392,16 @@ let run include_pc iset pat env = 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 offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (Bindings.find k decoderst.instrs) )) offline_fns in + let useoffline = 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 useoffline then (Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (freachable k))) offline_fns) else offline_fns in let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index d54c97ec..c88661e1 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2308,10 +2308,10 @@ module BDDSimp = struct let wd = int_of_string wd in let e = eval_expr e st in extract_bits e lo wd - | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> - Top + | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> Top + | Expr_Unknown t -> Top - | _ -> failwith @@ "unexpected expr: " ^ (pp_expr e) + | _ -> Printf.printf "BDDSimp eval_expr: unexpected expr: %s\n" (pp_expr e) ; Top (****************************************************************) (** Stmt Walk *) From 38b386348a73b3bddcd52c179ecee70e03a3a897 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Thu, 9 May 2024 17:31:35 +1000 Subject: [PATCH 13/19] refactor so analysis and transform both called into from bdd AI walk --- libASL/offline_opt.ml | 162 +++++++++++++++++++++++++++++------------- libASL/transforms.ml | 76 ++++++++++++++------ 2 files changed, 166 insertions(+), 72 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 41b771e3..b5ba4540 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -43,6 +43,7 @@ let is_pure_expr f = let is_var_decl f = f = Offline_transform.rt_decl_bv || f = Offline_transform.rt_decl_bool + module CopyProp = struct type clas = Declared | @@ -328,17 +329,18 @@ end module RtCopyProp = struct + type clas = Declared | Defined of IdentSet.t | - Clobbered | (* means there is a clobber on at least one branch *) - Essential (* not a candidate: there is a read following a clobber or dependent on rt branch *) + Clobbered of IdentSet.t | + Essential let pp_clas c = match c with | Declared -> "Declared" | Defined ids -> "Defined (" ^ pp_identset ids ^ ")" - | Clobbered -> "Clobbered" + | Clobbered ids -> "Clobbered" | Essential -> "Essential" let merge_clas a b = @@ -348,8 +350,8 @@ module RtCopyProp = struct (* Ignore declared? *) | Declared, Defined d | Defined d, Declared -> Defined d - | Declared, Clobbered - | Clobbered, Declared -> Clobbered + | Declared, Clobbered c + | Clobbered c , Declared -> Clobbered c (* Can't drop essential though - needs to hold once set *) | Declared, Essential @@ -357,75 +359,90 @@ module RtCopyProp = struct (* Union deps, consider essential even if only conditional *) | Defined d, Defined d' -> Defined (IdentSet.union d d') - | Defined _, Clobbered - | Clobbered, Defined _ -> Clobbered + | Defined d, Clobbered d' + | Clobbered d, Clobbered d' + | Clobbered d, Defined d' -> Clobbered (IdentSet.union d d') | Defined _, Essential | Essential, Defined _ -> Essential (* *) - | Clobbered, Clobbered -> Clobbered - | Clobbered, Essential - | Essential, Clobbered + | Clobbered _, Essential + | Essential, Clobbered _ | Essential, Essential -> Essential + + type state = { var_clas : clas Bindings.t; ctx : (ident * MLBDD.t) list; (* maps idents to the condution under which they are clobbered *) - cond_clobbered: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) + cond_clobbered: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) (* maps idents to the condition under which they are read after clobbering *) - cond_read_after_clobber: (Transforms.BDDSimp.abs) Bindings.t; (* ident -> clobber condition (any dep updated) *) + cond_read_after_clobber: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) (* not used; stores dep sets for bindings (and the def reachability) *) - cond_dep: (Transforms.BDDSimp.abs * IdentSet.t) Bindings.t; (* binding -> condition * deps *) + cond_dep: (MLBDD.t * IdentSet.t) Bindings.t; (* binding -> condition * deps *) (**) bdd: Transforms.BDDSimp.state; } + type rt = state + type olt = MLBDD.t + + + let set_var v k st = let var_clas = Bindings.add v k st.var_clas in + (* TODO: need to be adapted for new lattice ? *) let _ = match k with | Declared -> () | Defined x -> () - | Clobbered -> () + | Clobbered i -> () | Essential -> () in { st with var_clas } let cond_merge al bl = Bindings.merge (fun i a b -> match a,b with - | Some a, Some b -> Some (Transforms.BDDSimp.or_bits a b) + | Some a, Some b -> Some (MLBDD.dor a b) | Some a, _ -> Some a | _ , Some b -> Some b | _ -> None) al bl let add_cond i c bs = Bindings.add i (match (Bindings.find_opt i bs) with - | Some x -> (Transforms.BDDSimp.or_bits c x) + | Some x -> (MLBDD.dor c x) | None -> c ) bs let add_conds is c bs = cond_merge bs (Seq.map (fun i -> i, c) is |> Bindings.of_seq) let clobber_var v st = - let var_clas = Bindings.map (fun c -> match c with Defined ids when IdentSet.mem v ids -> Clobbered | _ -> c) st.var_clas in - (* TODO: should clobbering transitive?*) - let deps = Bindings.filter_map (fun i c -> match c with Defined ids when IdentSet.mem v ids -> - Some (Transforms.BDDSimp.Val [st.bdd.ctx]) | _ -> None) st.var_clas in + let var_clas = Bindings.map (fun c -> match c with Defined ids | Clobbered ids when IdentSet.mem v ids -> Clobbered ids | _ -> c) st.var_clas in + let deps = Bindings.filter_map (fun i c -> match c with + | Defined ids + | Clobbered ids when IdentSet.mem v ids -> Some (st.bdd.ctx) + | _ -> None) var_clas in let cond_clobbered = cond_merge st.cond_clobbered deps in { st with var_clas ; cond_clobbered } let get_var v st = Bindings.find_opt v st.var_clas - let merge_st cond a b = + + let merge_st (cond: Transforms.BDDSimp.abs) a b = let ctx = a.ctx in - let merged_bdd a b = Bindings.merge (fun (k:ident) (a:Transforms.BDDSimp.abs option) (b:Transforms.BDDSimp.abs option) -> match a,b with - | Some a, Some b -> Some (Transforms.BDDSimp.join_abs cond a b) + let unpack x = match x with + | Transforms.BDDSimp.Val [a] -> Some a + | Transforms.BDDSimp.Val (h::tl) -> failwith "why?" + | _ -> None + in + let merged_bdd a b = Bindings.merge (fun (k:ident) (a) (b) -> match a,b with + | Some a, Some b -> (unpack (Transforms.BDDSimp.join_abs cond (Val [a]) (Val [b]))) | Some a, None -> Some a | None, Some a -> Some a | None, None -> None) a b in let cond_clobbered = merged_bdd a.cond_clobbered b.cond_clobbered in let cond_read_after_clobber = merged_bdd a.cond_read_after_clobber b.cond_read_after_clobber in let cond_dep = Bindings.merge (fun k a b -> match a,b with - | Some (isa, a), Some (isb, b) -> Some (Transforms.BDDSimp.join_abs cond isa isb, IdentSet.union a b) + | Some (isa, a), Some (isb, b) -> Option.map (fun x -> x, IdentSet.union a b) (unpack (Transforms.BDDSimp.join_abs cond (Val [isa]) (Val [isb]))) | Some a, None -> Some a | None, Some a -> Some a | _ -> None @@ -438,22 +455,26 @@ module RtCopyProp = struct | None, None -> None) a.var_clas b.var_clas in let bdd = Transforms.BDDSimp.join_state cond a.bdd b.bdd in { bdd; var_clas ; ctx ; cond_clobbered; cond_read_after_clobber; cond_dep } + + let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; var_clas = Bindings.empty; ctx = []; cond_clobbered = Bindings.empty ; cond_read_after_clobber = Bindings.empty ; cond_dep = Bindings.empty} + let push_context m st = { st with ctx = m::st.ctx } let peek_context st = match st.ctx with x::xs -> x | _ -> invalid_arg "peek_context" let pop_context st = let (i,c),tl = (match st.ctx with x::xs -> x,xs | _ -> invalid_arg "pop_context") in { st with ctx = tl ; bdd = {st.bdd with ctx = c} } + let has_context st = List.length st.ctx > 0 let decl_var v st = set_var v Declared st let define_var v deps st = let r = set_var v (Defined deps) st in let cond_dep = Bindings.find_opt v st.cond_dep |> - Option.map (fun (c,b) -> Transforms.BDDSimp.or_bits c (Transforms.BDDSimp.Val [st.bdd.ctx]), IdentSet.union b deps) |> + Option.map (fun (c,b) -> MLBDD.dor c (st.bdd.ctx), IdentSet.union b deps) |> function | Some c -> Bindings.add v c st.cond_dep | None -> st.cond_dep @@ -462,7 +483,7 @@ module RtCopyProp = struct type xform = | Prop - | PropCond of Transforms.BDDSimp.abs (* copyprop not allowed , should copyprop *) + | PropCond of MLBDD.t (* copyprop not allowed , should copyprop *) | No let read_var v (st,i) = @@ -471,10 +492,10 @@ module RtCopyProp = struct | Some (Declared) -> (set_var v Essential st, i) (* Reading clobbered implies we cannot reorder *) - | Some (Clobbered) -> ( + | Some (Clobbered ids) -> ( (* record read reachability *) let clobbered = (Bindings.find v st.cond_clobbered) in - let read_after_clobber = Transforms.BDDSimp.and_bits clobbered (Val [st.bdd.ctx]) in + let read_after_clobber = MLBDD.dand clobbered (st.bdd.ctx) in let st = {st with cond_read_after_clobber = (add_cond v read_after_clobber st.cond_read_after_clobber)} in st, i ) (*if (Transforms.BDDSimp.is_true clobbered st.bdd) then (set_var v Essential st, i) else st, i) *) @@ -507,6 +528,8 @@ module RtCopyProp = struct set_var v (Defined deps) st | Some (Defined d') -> set_var v (Defined (IdentSet.union deps d')) st + | Some (Clobbered d') -> + set_var v (Clobbered (IdentSet.union deps d')) st | _ -> st class deps_walker = object (self) @@ -549,13 +572,13 @@ module RtCopyProp = struct let pp_essential st = pp_bindings pp_clas (Bindings.filter (fun f v -> v = Essential) st.var_clas) + + let rec walk_stmt s st = - let eval_post s st = {st with bdd = Transforms.BDDSimp.eval_stmt Transforms.BDDSimp.nop_transform s st.bdd } in match s with (* Var decl *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> decl_var v st - |> eval_post s (* Var assign *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> @@ -566,7 +589,6 @@ module RtCopyProp = struct let st = clobber_var v st in (* Update deps for v *) update_deps v deps st - |> eval_post s (* Array assign *) | Stmt_TCall(f, [], [Expr_Var a; i; e], loc) when is_array_store f -> @@ -575,27 +597,34 @@ module RtCopyProp = struct let st = read_vars deps st in (* Clobber anything dependent on a *) clobber_var a st - |> eval_post s (* Assert *) | Stmt_TCall(f, [], [e], loc) when is_assert f -> (* Collect reads and process them all *) let deps = get_deps e in read_vars deps st - |> eval_post s (* LiftTime branch *) - | Stmt_If(c, t, [], f, loc) -> + | Stmt_If(c, t, [], f, loc) -> st (* handled by caller splitting, walking children, and joining *) (* merge in the bdds as well *) + + (* let cond = Transforms.BDDSimp.eval_expr c st.bdd in let c = Transforms.BDDSimp.rebuild_expr c cond st.bdd in let ncond = Transforms.BDDSimp.not_bool cond in let tst:state = walk_stmts t {st with bdd = (Transforms.BDDSimp.restrict_ctx cond {st.bdd with stmts = []})} in let fst:state = walk_stmts f {st with bdd = (Transforms.BDDSimp.restrict_ctx ncond {st.bdd with stmts = []})} in + + let condbdd = match cond with + | Val [t] -> t + | _ -> failwith (Printf.sprintf "unable to eval cond branch %s %s %s" (Transforms.BDDSimp.pp_abs cond) (Transforms.BDDSimp.pp_state st.bdd) (pp_expr c) ) + in + let st': state = merge_st cond tst fst in let st'= {st' with bdd = Transforms.BDDSimp.writeall st.bdd.stmts st'.bdd} in let st' = {st' with bdd = Transforms.BDDSimp.write (Stmt_If (c, tst.bdd.stmts, [], fst.bdd.stmts, loc)) st'.bdd} in - st' + *) + (* RunTime branch *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], [c]), loc) when is_branch f -> @@ -604,13 +633,11 @@ module RtCopyProp = struct let st = read_vars deps st in (* Push the merge point *) push_context (v, st.bdd.ctx) st - |> eval_post s (* Context switch *) | Stmt_TCall(f, [], [Expr_TApply(f2, [], [Expr_Var i])], loc) when is_context_switch f && is_merge_target f2 -> let top = fst (peek_context st) in if i = top then ((pop_context st)) else st - |> eval_post s (* Impure effect *) | Stmt_TCall(f, _, es, loc) when is_gen_call f -> @@ -620,9 +647,8 @@ module RtCopyProp = struct read_vars deps st) es st in (* Clobber everything linked to global state *) clobber_var impure_ident st - |> eval_post s - | v -> eval_post v st + | v -> st and walk_stmts s st : state = List.fold_left (fun st s -> walk_stmt s st) st s @@ -633,6 +659,7 @@ module RtCopyProp = struct | None -> false | _ -> true + (* To change this, you'd need to know : - The condition under which its safe to copy prop - The current reachability @@ -670,13 +697,14 @@ statement s is the only definition of x reaching u
on every path from s to u t end + (* variable is not clobbered then read *) let cond_candidate v st rtst = match get_var v st with | Some Essential -> No - | Some Clobbered -> + | Some Clobbered deps -> let c = Bindings.find_opt v st.cond_read_after_clobber in (match c with | Some x -> PropCond x @@ -687,13 +715,22 @@ statement s is the only definition of x reaching u
on every path from s to u t let cp_idents = function - | Ident c -> Ident (c ^ "_nocopyprop") , Ident (c ^ "_copyprop") + | Ident c -> Ident (c) , Ident (c ^ "_copyprop") | _ -> failwith "only copyprop vars" type cand = { typ: ty } + class copyprop_vis icpst = object(self) + inherit Asl_visitor.nopAslVisitor + val mutable cpst = icpst + + method xfer_stmt s = cpst <- walk_stmt s cpst + method join cond os = cpst <- merge_st cond cpst os + end + + class cond_copyprop_transform cpst = object(self) inherit Asl_visitor.nopAslVisitor val mutable rtst = None @@ -722,7 +759,7 @@ statement s is the only definition of x reaching u
on every path from s to u t copy-propagated at lift time. *) method stmt_xform (s : stmt) : stmt list = - let cp_cond c = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (c) (Option.get rtst) in + let cp_cond c = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (Val [MLBDD.dnot c]) (Option.get rtst) in match s with (* Transform runtime variable decls into expression decls *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> @@ -734,7 +771,7 @@ statement s is the only definition of x reaching u
on every path from s to u t | Prop -> [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [v], loc)] | PropCond cond -> let ncp,cp = cp_idents v in let c = cp_cond cond in - let rt_decl = Stmt_If (c, [], [] , [Stmt_Assign (LExpr_Var ncp, Expr_TApply(f, [], args), Unknown)], Unknown) in + let rt_decl = Stmt_If (c, [Stmt_Assign (LExpr_Var ncp, Expr_TApply(f, [], args), Unknown)], [], [], Unknown) in (* lift-time conditionally generates the copy-propagated or non-propagated form *) [ Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [ncp], loc); @@ -757,7 +794,7 @@ statement s is the only definition of x reaching u
on every path from s to u t let gen_store_rt_var = Stmt_TCall(f, [], [Expr_Var nocp; e], loc) in let assign_lt_var = Stmt_Assign(LExpr_Var cp, e, loc) in (* TODO: could further narrow cases here using bdd*) - [Stmt_If ( cp_cond cond, [gen_store_rt_var], [], [assign_lt_var], Unknown)] + [Stmt_If ( cp_cond cond, [assign_lt_var], [], [gen_store_rt_var], Unknown)] ) | _ -> [s] @@ -769,7 +806,7 @@ statement s is the only definition of x reaching u
on every path from s to u t | PropCond cpcond -> let ncp,cp = cp_idents v in let load = Expr_TApply(f, [], [Expr_Var ncp]) in let prop = Expr_Var cp in - let yescpcond = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) cpcond (Option.get rtst) in + let yescpcond = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (Val [cpcond]) (Option.get rtst) in let vt = Bindings.find v candidates in (* TODO: might be good to check that yes and no are disjoint here *) let e = Expr_If (vt.typ, yescpcond, prop, [] , load) in @@ -778,19 +815,42 @@ statement s is the only definition of x reaching u
on every path from s to u t | _ -> e end + + module AnalysisLat = struct + type rt = state + type olt = Transforms.BDDSimp.state + let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = walk_stmt s r,[s] + let join (ol:olt) (rta: rt) (rtb: rt) = merge_st (Val[ol.ctx]) rta rtb + let init s = init_state s + end + + module TransformLat = struct + (* warning: internally mutable because order should not matter etc, join is no-op *) + type rt = {cpst: cond_copyprop_transform} + type olt = Transforms.BDDSimp.state + let xfer_stmt ol ss s = ss,ss.cpst#xf_stmt s ol + let join r a b = if (a != b) then (failwith "not allowed") else a (* only have one instance of the object so should be fine *) + let init st = {cpst = new cond_copyprop_transform st} + end + + module BDDAnalysis = Transforms.BDDSimp.EvalWithXfer(AnalysisLat) + module BDDTransform = Transforms.BDDSimp.EvalWithXfer(TransformLat) + let do_transform reachable copyprop_st stmts = (* apply BDD AI a second time to compare reachability with candidates in analysis pass *) let st = Transforms.BDDSimp.init_state reachable in let st = Transforms.BDDSimp.set_enc st in - let st' = Transforms.BDDSimp.eval_stmts (copyprop_st) stmts st in - st'.stmts + let olt,ort = BDDTransform.eval_stmts (TransformLat.init copyprop_st) stmts st in + olt.stmts let run fn reachable body = - let st = init_state reachable in - let st = walk_stmts body st in + let st : AnalysisLat.rt = init_state reachable in + let rtst = Transforms.BDDSimp.init_state reachable in + let rtst = Transforms.BDDSimp.set_enc rtst in + (*let st = walk_stmts body st in *) + let a,b = BDDAnalysis.eval_stmts st body rtst in (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_essential st); *) (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_state st); *) - let v = new cond_copyprop_transform st in - do_transform reachable v body + do_transform reachable b body end diff --git a/libASL/transforms.ml b/libASL/transforms.ml index c88661e1..45a6c38e 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2054,6 +2054,12 @@ module DecoderChecks = struct end +module type RTAnalysisLattice = sig + type rt (* RT lattice type *) + type olt (* LT lattice type *) + val xfer_stmt : olt -> rt -> stmt -> rt*stmt list + val join: olt -> rt -> rt -> rt +end module BDDSimp = struct @@ -2069,6 +2075,17 @@ module BDDSimp = struct stmts: stmt list; } + module type Lattice = RTAnalysisLattice with type olt = state + + module NopAnalysis = struct + type rt = unit + type olt = state + let xfer_stmt o r s = r,[s] + let join o r ro = () + let init _ = () + end + + let init_state (ctx : MLBDD.t) = { man = MLBDD.manager ctx; vars = Bindings.empty ; @@ -2303,15 +2320,22 @@ module BDDSimp = struct | Expr_TApply (FIdent (f, 0), tes, es) -> let es = List.map (fun e -> eval_expr e st) es in eval_prim f tes es st - | Expr_Slices(e, [Slice_LoWd(Expr_LitInt lo,Expr_LitInt wd)]) -> + | Expr_Slices(e, [Slice_LoWd(Expr_LitInt lo, Expr_LitInt wd)]) -> let lo = int_of_string lo in let wd = int_of_string wd in let e = eval_expr e st in extract_bits e lo wd | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> Top - | Expr_Unknown t -> Top + | Expr_Parens(e) -> eval_expr e st + | Expr_Fields _ -> Printf.printf "unexpected Expr_Fields %s" (pp_expr e); Top + | Expr_In _ -> Printf.printf "unexpected Expr_In %s" (pp_expr e); Top + | Expr_Unop _ -> Printf.printf "unexpected Expr_Unop %s" (pp_expr e); Top + | Expr_Unknown _ -> Printf.printf "unexpected Expr_Unkonwn %s" (pp_expr e); Top + | Expr_ImpDef _ -> Printf.printf "unexpected Expr_ImpDef %s" (pp_expr e); Top + | Expr_LitString _ -> Printf.printf "unexpected Expr_LitString %s" (pp_expr e); Top + | Expr_If _ -> Printf.printf "unexpected Expr_If %s" (pp_expr e); Top - | _ -> Printf.printf "BDDSimp eval_expr: unexpected expr: %s\n" (pp_expr e) ; Top + | _ -> failwith @@ Printf.sprintf "BDDSimp eval_expr: unexpected expr: %s\n" (pp_expr e) (****************************************************************) (** Stmt Walk *) @@ -2395,77 +2419,87 @@ module BDDSimp = struct let nop_transform = new nopvis - let rec eval_stmt xf s st = - let ns = xf#xf_stmt s st in + module EvalWithXfer (Xf: Lattice) = struct + + let rec eval_stmt (xs:Xf.rt) (s:stmt) (st:state) = + let xs,ns = Xf.xfer_stmt st xs s in match s with | Stmt_VarDeclsNoInit(t, [v], loc) -> let st = add_var v Bot st in - writeall ns st + writeall ns st, xs | Stmt_VarDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - writeall ns st + writeall ns st, xs | Stmt_ConstDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - writeall ns st + writeall ns st,xs | Stmt_Assign(LExpr_Var v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - writeall ns st + writeall ns st,xs (* Eval the assert, attempt to discharge it & strengthen ctx *) | Stmt_Assert(e, loc) -> let abs = eval_expr e st in - if is_false abs st then st + if is_false abs st then st,xs else let e = rebuild_expr e abs st in let st = write (Stmt_Assert(e,loc)) st in - restrict_ctx abs st + restrict_ctx abs st, xs (* State becomes bot - unreachable *) | Stmt_Throw _ -> Printf.printf "%s : %s\n" (pp_stmt s) (pp_state st); let st = writeall ns st in - halt st + halt st,xs (* If we can reduce c to true/false, collapse *) | Stmt_If(c, tstmts, [], fstmts, loc) -> let cond = eval_expr c st in + if is_true cond st then - eval_stmts xf tstmts st + eval_stmts xs tstmts st else if is_false cond st then - eval_stmts xf fstmts st + eval_stmts xs fstmts st else let c = rebuild_expr c cond st in let ncond = not_bool cond in - let tst = eval_stmts xf tstmts (restrict_ctx cond {st with stmts = []}) in - let fst = eval_stmts xf fstmts (restrict_ctx ncond {st with stmts = []}) in + + let tst,xsa = eval_stmts xs tstmts (restrict_ctx cond {st with stmts = []}) in + let fst,xsb = eval_stmts xs fstmts (restrict_ctx ncond {st with stmts = []}) in let st' = join_state cond tst fst in + let xs = Xf.join st' xsa xsb in + let st' = writeall st.stmts st' in let st' = write (Stmt_If (c, tst.stmts, [], fst.stmts, loc)) st' in - st' + st',xs (* Can't do anything here *) | Stmt_Assign _ | Stmt_TCall _ -> - write s st + write s st,xs | _ -> failwith "unknown stmt" - and eval_stmts xf stmts st = - List.fold_left (fun st s -> if MLBDD.is_false st.ctx then st else eval_stmt xf s st) st stmts + and eval_stmts xs stmts st = + List.fold_left (fun (st,xs) s -> if MLBDD.is_false st.ctx then st,xs else (eval_stmt xs s st)) (st,xs) stmts + + end let set_enc st = let enc = Val (List.rev (List.init 32 (MLBDD.ithvar st.man))) in {st with vars = Bindings.add (Ident "enc") enc st.vars} + module Eval = EvalWithXfer(NopAnalysis) + let just_eval a b c = fst (Eval.eval_stmts (NopAnalysis.init ()) a b) let do_transform fn stmts reach = let st = init_state reach in let st = set_enc st in - let st' = eval_stmts (new nopvis) stmts st in + let st',xs = Eval.eval_stmts (NopAnalysis.init ()) stmts st in st'.stmts From 510fa7285684ef911331d69c6fe2cc7dc39a6482 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Fri, 10 May 2024 18:46:56 +1000 Subject: [PATCH 14/19] fix anlaysis a bit and add bvadd --- libASL/offline_opt.ml | 62 +++++++++++++++-------- libASL/symbolic_lifter.ml | 9 ++-- libASL/transforms.ml | 103 +++++++++++++++++++++++++++++--------- 3 files changed, 128 insertions(+), 46 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index b5ba4540..a5aa63d7 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -707,11 +707,21 @@ statement s is the only definition of x reaching u
on every path from s to u t | Some Clobbered deps -> let c = Bindings.find_opt v st.cond_read_after_clobber in (match c with - | Some x -> PropCond x - | None -> No) + | Some x -> (if (Transforms.BDDSimp.is_true (Val [x]) rtst) then ( + (* we don't need to generate a condition at read if we know statically *) + Printf.printf "Condcopyprop: var %s BDD %s simplifies to TRUE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [x])); + No) + else if (Transforms.BDDSimp.is_false (Val [x]) rtst) then ( + Printf.printf "Condcopyprop: var %s BDD %s simplifies to FALSE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [x])) ; + Prop + ) + else PropCond (MLBDD.dnot x)) + | None -> Printf.printf "Condcopyprop: Clobbered variable missing cond read %s\n" (pprint_ident v); + No) (* TODO: clobbered but not subsequently read? *) | Some Defined _ -> Prop | Some Declared -> No - | None -> No + | None -> Printf.printf "Unexpected variable with no candidate decision status %s\n" (pprint_ident v); No + let cp_idents = function @@ -743,8 +753,8 @@ statement s is the only definition of x reaching u
on every path from s to u t method candidate v = (Prop = (cond_candidate v cpst (Option.get rtst))) method essential v = (No = (cond_candidate v cpst (Option.get rtst))) - method! vstmt s = ChangeDoChildrenPost (self#stmt_xform s, fun x -> x) - method! vexpr e = ChangeDoChildrenPost (self#expr_xform e, fun x -> x) + method! vstmt s = ChangeDoChildrenPost ([s], fun s -> List.concat_map self#stmt_xform s) + method! vexpr e = ChangeDoChildrenPost (e, fun e -> self#expr_xform e) (* @@ -759,32 +769,39 @@ statement s is the only definition of x reaching u
on every path from s to u t copy-propagated at lift time. *) method stmt_xform (s : stmt) : stmt list = - let cp_cond c = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (Val [MLBDD.dnot c]) (Option.get rtst) in + let cp_cond c = Transforms.BDDSimp.bdd_to_expr (c) (Option.get rtst) in match s with (* Transform runtime variable decls into expression decls *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> candidates <- Bindings.add v {typ=t} candidates; (match (cond_candidate v cpst (Option.get rtst)) with (* essential, leave as-is *) - | No -> [s] + | No -> + Printf.printf "Condcopyprop: NOT PROP at DEFINITION of var %s\n " (pprint_ident v); + [s] (* move run-time to lift-time *) - | Prop -> [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [v], loc)] + | Prop -> + Printf.printf "Condcopyprop: UNCOND prop at DEFINITION of var %s\n " (pprint_ident v); + [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [snd (cp_idents v)], Unknown)] | PropCond cond -> let ncp,cp = cp_idents v in + Printf.printf "Condcopyprop: CONDITIONAL prop at DEFINITION : %s\n " (Transforms.BDDSimp.pp_abs (Val [cond])); let c = cp_cond cond in - let rt_decl = Stmt_If (c, [Stmt_Assign (LExpr_Var ncp, Expr_TApply(f, [], args), Unknown)], [], [], Unknown) in + (Printf.printf("Successfully simplified bdd cond to %s on stmt %s \n") (pp_expr c) (pp_stmt s) ; (* lift-time conditionally generates the copy-propagated or non-propagated form *) [ - Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [ncp], loc); - Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], loc); - rt_decl - ] + Stmt_ConstDecl (Offline_transform.rt_expr_ty, ncp, Expr_TApply(f, [], args), Unknown); + Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], Unknown); + ]) ) (* Transform stores into assigns *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> (match (cond_candidate v cpst (Option.get rtst)) with - | No -> [s] - | Prop -> [(Stmt_Assign (LExpr_Var v, e, loc))] + | No -> (Printf.printf "Condcopyprop: UNCOND DISABLE PROP on STORE of var %s\n " (pprint_ident v)); [s] + | Prop -> + (Printf.printf "Condcopyprop: UNCOND RT PROP on STORE of var %s\n " (pprint_ident v); + [(Stmt_Assign (LExpr_Var (snd (cp_idents v)), e, loc))]) | PropCond cond -> let nocp,cp = cp_idents v in + Printf.printf "Condcopyprop: CONDITIONAL rt prop on STORE of var %s\n " (pprint_ident v); (* - if copy-prop'ed form is reachable then generate a store statement - if non-copyprop'ed form is reachable then generate an assignment statement @@ -796,22 +813,25 @@ statement s is the only definition of x reaching u
on every path from s to u t (* TODO: could further narrow cases here using bdd*) [Stmt_If ( cp_cond cond, [assign_lt_var], [], [gen_store_rt_var], Unknown)] ) + | Stmt_TCall(f, _, _, _) when is_var_store f -> failwith "unhandled store" | _ -> [s] method expr_xform (e:expr) : expr = match e with | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f -> (match (cond_candidate v cpst (Option.get rtst)) with | No -> e - | Prop -> Expr_Var v + | Prop -> Expr_Var (snd (cp_idents v)) | PropCond cpcond -> let ncp,cp = cp_idents v in let load = Expr_TApply(f, [], [Expr_Var ncp]) in let prop = Expr_Var cp in - let yescpcond = Transforms.BDDSimp.rebuild_expr (Expr_Var (Ident "TRUE")) (Val [cpcond]) (Option.get rtst) in + let yescpcond = Transforms.BDDSimp.bdd_to_expr cpcond (Option.get rtst) in let vt = Bindings.find v candidates in (* TODO: might be good to check that yes and no are disjoint here *) let e = Expr_If (vt.typ, yescpcond, prop, [] , load) in e ) + + | Expr_TApply(f, [], [Expr_Var v; e]) when is_var_store f -> failwith "store expression"; | _ -> e end @@ -819,7 +839,7 @@ statement s is the only definition of x reaching u
on every path from s to u t module AnalysisLat = struct type rt = state type olt = Transforms.BDDSimp.state - let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = walk_stmt s r,[s] + let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = Printf.printf "%s ::\n%s\n" (pp_stmt s) (Transforms.BDDSimp.pp_state l); (walk_stmt s r,[s]) let join (ol:olt) (rta: rt) (rtb: rt) = merge_st (Val[ol.ctx]) rta rtb let init s = init_state s end @@ -839,14 +859,16 @@ statement s is the only definition of x reaching u
on every path from s to u t let do_transform reachable copyprop_st stmts = (* apply BDD AI a second time to compare reachability with candidates in analysis pass *) let st = Transforms.BDDSimp.init_state reachable in - let st = Transforms.BDDSimp.set_enc st in + let st = Transforms.BDDSimp.set_enc st in let olt,ort = BDDTransform.eval_stmts (TransformLat.init copyprop_st) stmts st in olt.stmts let run fn reachable body = + flush stdout; + Printf.printf "transforming %s\n" (pprint_ident fn); let st : AnalysisLat.rt = init_state reachable in let rtst = Transforms.BDDSimp.init_state reachable in - let rtst = Transforms.BDDSimp.set_enc rtst in + let rtst = Transforms.BDDSimp.set_enc rtst in (*let st = walk_stmts body st in *) let a,b = BDDAnalysis.eval_stmts st body rtst in (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_essential st); *) diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 09b62f9f..3bb0abd5 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -364,8 +364,11 @@ let run include_pc iset pat env = let env' = Eval.Env.copy env in 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 not (Bindings.mem fn instrs) then None + if (debug && (fn <> (FIdent ("aarch64_branch_unconditional_register", 0)))) || (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); @@ -392,7 +395,7 @@ let run include_pc iset pat env = 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 useoffline = true in + let use_rt_copyprop = true in let freachable k = let k = match k with @@ -401,7 +404,7 @@ let run include_pc iset pat env = Bindings.find k decoderst.instrs in - let offline_fns = if useoffline then (Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (freachable k))) offline_fns) else offline_fns 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 dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 45a6c38e..03b0ff2f 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2129,7 +2129,7 @@ module BDDSimp = struct let get_var v st = match Bindings.find_opt v st.vars with | Some v -> v - | _ -> Top (* logically this should be Bot, but need to init globals *) + | _ -> (Printf.printf "no var %s\n" (pprint_ident v)); Top (* logically this should be Bot, but need to init globals *) let add_var v abs st = { st with vars = Bindings.add v abs st.vars } @@ -2268,6 +2268,57 @@ module BDDSimp = struct (** Expr Walk *) (****************************************************************) + + let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) + + let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)= + let full_add_bit l r carry = + let s1,c1 = half_add_bit l r in + let o, c2 = half_add_bit s1 carry in + let ocarry = MLBDD.dor c1 c2 in + o,ocarry + in + match (List.rev xs),(List.rev ys) with + | [x],[y] -> let c , s = half_add_bit x y in c, [s] + | hx::tlx,hy::tly -> + let lsb,lscarry = half_add_bit hx hy in + let xs = List.rev tlx in let ys = List.rev tly in + let bits,carry = + List.fold_right2 + (fun (l:MLBDD.t) (r:MLBDD.t) (acc,carry) -> let o,carry = (full_add_bit l r carry) in o::acc, carry) + xs ys ([], lscarry) + in carry,bits@[lsb] + | _,_ -> failwith "invalid bit strings" + + let signed_add_wrap x y = let _,bits = twos_comp_add x y in bits + let signed_negation x = (List.map MLBDD.dnot x) + + let signed_sub_wrap x y = let _,bits = twos_comp_add x (signed_negation y) in bits + + let signed_lt x y = + let xneg = List.hd x in let yneg = List.hd y in + let carry,subbits = (twos_comp_add x (signed_negation y)) in + let b = MLBDD.dand xneg (MLBDD.dnot yneg) in (* x < 0 < y*) + let b1 = MLBDD.dand (MLBDD.dand xneg yneg) (List.hd subbits) in (* x < y < 0*) + let b2 = MLBDD.dand (MLBDD.dnot (MLBDD.dor xneg yneg)) (MLBDD.dnot (List.hd subbits)) (* 0 < x < y*) + in [MLBDD.dor b (MLBDD.dor b1 b2)] + + let signed_gt x y = List.map MLBDD.dnot (signed_lt x y) + + let eq_bvs a b = + let bits = List.map2 MLBDD.eq a b in + match bits with + | x::xs -> List.fold_right MLBDD.dand xs x + | _ -> failwith "bad bits width" + + let signed_lte_bits x y = [MLBDD.dor (eq_bvs x y) (List.hd (signed_lt x y))] + let signed_gte_bits x y = [MLBDD.dor (eq_bvs x y) (List.hd (signed_gt x y))] + + + let twos_comp_sub man (xs : MLBDD.t list) (ys: MLBDD.t list) = () + + + let eval_prim f tes es st = match f, tes, es with | "and_bool", [], [x; y] -> and_bool x y @@ -2290,8 +2341,12 @@ module BDDSimp = struct | "SignExtend", [w;Expr_LitInt nw], [x; y] -> sign_extend_bits x (int_of_string nw) st - | "sle_bits", [w], [x; y] -> Top - | "add_bits", [w], [x; y] -> Top + | "sle_bits", [w], [x; y] -> (match x,y with + | Val x, Val y -> Val (signed_lte_bits x y) + | _,_ -> Top) + | "add_bits", [w], [x; y] -> (match x,y with + | Val x, Val y -> Val (signed_add_wrap x y) + | _,_ -> Top) | "lsr_bits", [w;w'], [x; y] -> Top | _, _, _ -> @@ -2308,13 +2363,13 @@ module BDDSimp = struct | '1' -> (MLBDD.dtrue st.man)::acc | '0' -> (MLBDD.dfalse st.man)::acc | _ -> acc) b []) - | Expr_LitInt e -> Top + | Expr_LitInt e -> Printf.printf "Overapprox litint %s\n" (e);Top | Expr_Var id -> get_var id st (* Simply not going to track these *) - | Expr_Field _ -> Top - | Expr_Array _ -> Top + | Expr_Field _ -> Printf.printf "Overapprox field %s\n" (pp_expr e) ; Top + | Expr_Array _ -> Printf.printf "Overapprox array %s\n" (pp_expr e); Top (* Prims *) | Expr_TApply (FIdent (f, 0), tes, es) -> @@ -2325,7 +2380,7 @@ module BDDSimp = struct let wd = int_of_string wd in let e = eval_expr e st in extract_bits e lo wd - | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> Top + | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> Printf.printf "Overapprox slice\n" ; Top | Expr_Parens(e) -> eval_expr e st | Expr_Fields _ -> Printf.printf "unexpected Expr_Fields %s" (pp_expr e); Top | Expr_In _ -> Printf.printf "unexpected Expr_In %s" (pp_expr e); Top @@ -2361,26 +2416,24 @@ module BDDSimp = struct let c = ctx_to_mask st.ctx in let imps = MLBDD.allprime cond in let imps = List.map (fun v -> clear_bits v c) imps in - let rebuild = List.fold_right (fun vars -> + (*let rebuild = List.fold_right (fun vars -> MLBDD.dor (List.fold_right (fun (b,v) -> MLBDD.(dand (if b then ithvar st.man v else dnot (ithvar st.man v))) ) vars (MLBDD.dtrue st.man)) - ) imps (MLBDD.dfalse st.man) in - let imps = MLBDD.allprime rebuild in + ) imps (MLBDD.dfalse st.man) in + let imps = MLBDD.allprime rebuild in *) let masks = List.map DecoderChecks.implicant_to_mask imps in - (match masks with - | [b] -> + let bd_to_test b = + (*("and_bits", [VInt n], [VBits x; VBits y ])*) let bv = Value.to_mask Unknown (Value.from_maskLit b) in sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv - | _ -> - let try2 = MLBDD.dnot cond in - (if List.length (MLBDD.allprime try2) = 1 then - Printf.printf "Neg candidate %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime try2)) - else - Printf.eprintf "Can't simp %s\n" (Utils.pp_list (fun i -> i) masks)); - failwith (Printf.sprintf "Ctx %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime st.ctx)))) - + in + (match masks with + | [b] -> bd_to_test b + | bs -> let tests = (List.map bd_to_test (List.tl bs)) in + let boolor a b = Expr_TApply(FIdent("or_bool", 0), [], [a;b]) in + List.fold_left boolor (List.hd tests) (List.tl tests)) let rebuild_expr e cond st = match cond with @@ -2401,12 +2454,13 @@ module BDDSimp = struct let bv = Value.to_mask Unknown (Value.from_maskLit b) in sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv | _ -> + (* let try2 = MLBDD.dnot cond in (if List.length (MLBDD.allprime try2) = 1 then Printf.printf "Neg candidate %s %s\n" (pp_expr e) (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime try2)) else Printf.printf "Can't simp %s %s\n" (pp_expr e) (Utils.pp_list (fun i -> i) masks)); - Printf.printf "Ctx %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime st.ctx)); + Printf.printf "Ctx %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime st.ctx)); *) e) | _ -> Printf.printf "no value %s %s\n" (pp_expr e) (pp_abs cond); @@ -2422,6 +2476,7 @@ module BDDSimp = struct module EvalWithXfer (Xf: Lattice) = struct let rec eval_stmt (xs:Xf.rt) (s:stmt) (st:state) = + (* (transfer : xs, s, st -> xs', s' ; eval : st -> s -> st' ; write s' : s' , st' -> st'' ) -> xs' s' st'' *) let xs,ns = Xf.xfer_stmt st xs s in match s with | Stmt_VarDeclsNoInit(t, [v], loc) -> @@ -2479,7 +2534,7 @@ module BDDSimp = struct (* Can't do anything here *) | Stmt_Assign _ | Stmt_TCall _ -> - write s st,xs + writeall ns st,xs | _ -> failwith "unknown stmt" @@ -2552,7 +2607,9 @@ module BDDSimp = struct Bindings.mapi (fun nm fnsig -> let i = match nm with FIdent(s,_) -> Ident s | s -> s in match Bindings.find_opt i st.instrs with - | Some reach -> fnsig_upd_body (fun b -> do_transform nm b reach) fnsig + | Some reach -> fnsig_upd_body (fun b -> + Printf.printf "transforming %s\n" (pprint_ident nm); + do_transform nm b reach) fnsig | None -> fnsig) instrs end From 1a124a25f418bf14d8df13ef7d6415db8560e6ce Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Fri, 10 May 2024 19:36:47 +1000 Subject: [PATCH 15/19] cleanup bvops --- libASL/offline_opt.ml | 4 +++- libASL/transforms.ml | 41 +++++++++++++++++++++++------------------ 2 files changed, 26 insertions(+), 19 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index a5aa63d7..aae7f427 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -839,7 +839,9 @@ statement s is the only definition of x reaching u
on every path from s to u t module AnalysisLat = struct type rt = state type olt = Transforms.BDDSimp.state - let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = Printf.printf "%s ::\n%s\n" (pp_stmt s) (Transforms.BDDSimp.pp_state l); (walk_stmt s r,[s]) + let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = + (*Printf.printf "%s ::\n%s\n" (pp_stmt s) (Transforms.BDDSimp.pp_state l);*) + (walk_stmt s r,[s]) let join (ol:olt) (rta: rt) (rtb: rt) = merge_st (Val[ol.ctx]) rta rtb let init s = init_state s end diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 03b0ff2f..711cbaaa 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2264,30 +2264,23 @@ module BDDSimp = struct let start = List.length v - lo - wd in Val (sublist v start wd) - (****************************************************************) - (** Expr Walk *) - (****************************************************************) - - - let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)= + let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) in let full_add_bit l r carry = let s1,c1 = half_add_bit l r in let o, c2 = half_add_bit s1 carry in let ocarry = MLBDD.dor c1 c2 in o,ocarry in - match (List.rev xs),(List.rev ys) with - | [x],[y] -> let c , s = half_add_bit x y in c, [s] + let xs = List.rev xs in let ys = List.rev ys in + match xs,ys with | hx::tlx,hy::tly -> let lsb,lscarry = half_add_bit hx hy in - let xs = List.rev tlx in let ys = List.rev tly in - let bits,carry = - List.fold_right2 - (fun (l:MLBDD.t) (r:MLBDD.t) (acc,carry) -> let o,carry = (full_add_bit l r carry) in o::acc, carry) - xs ys ([], lscarry) - in carry,bits@[lsb] + let bits,carry = List.fold_left2 + (fun (acc,carry) (l:MLBDD.t) (r:MLBDD.t) -> let o,carry = (full_add_bit l r carry) in o::acc, carry) + ([lsb], lscarry) tlx tly + in carry,bits | _,_ -> failwith "invalid bit strings" let signed_add_wrap x y = let _,bits = twos_comp_add x y in bits @@ -2317,6 +2310,14 @@ module BDDSimp = struct let twos_comp_sub man (xs : MLBDD.t list) (ys: MLBDD.t list) = () + let replicate_bits newlen bits = match bits with + | Val bits -> if Int.rem newlen (List.length bits) <> 0 then failwith "indivisible rep length" ; + let repeats = newlen / (List.length bits) in Val (List.concat (List.init repeats (fun i -> bits))) + | _ -> Top + + (****************************************************************) + (** Expr Walk *) + (****************************************************************) let eval_prim f tes es st = @@ -2334,7 +2335,8 @@ module BDDSimp = struct | "ne_bits", [w], [x; y] -> ne_bits x y | "eor_bits", [w], [x; y] -> eor_bits x y - | "append_bits", [w;w'], [x; y] -> append_bits x y + | "append_bits", [w;w'], [x; y] -> append_bits x y + (*| "replicate_bits", [w;Expr_LitInt nw], [x;times] -> replicate_bits (int_of_string nw) x *) | "ZeroExtend", [w;Expr_LitInt nw], [x; y] -> zero_extend_bits x (int_of_string nw) st @@ -2344,9 +2346,12 @@ module BDDSimp = struct | "sle_bits", [w], [x; y] -> (match x,y with | Val x, Val y -> Val (signed_lte_bits x y) | _,_ -> Top) - | "add_bits", [w], [x; y] -> (match x,y with - | Val x, Val y -> Val (signed_add_wrap x y) + | "add_bits", [Expr_LitInt w], [x; y] -> (match x,y with + | Val x, Val y -> let r = (signed_add_wrap x y) in assert (List.length r == (int_of_string w)); Val r | _,_ -> Top) + | "sub_bits", [w], [x; y] -> (match x,y with + | Val x, Val y -> Val (signed_add_wrap x (signed_negation y)) + | _,_ -> Top) | "lsr_bits", [w;w'], [x; y] -> Top | _, _, _ -> @@ -2363,7 +2368,7 @@ module BDDSimp = struct | '1' -> (MLBDD.dtrue st.man)::acc | '0' -> (MLBDD.dfalse st.man)::acc | _ -> acc) b []) - | Expr_LitInt e -> Printf.printf "Overapprox litint %s\n" (e);Top + | Expr_LitInt e -> Top | Expr_Var id -> get_var id st From aa07c66124f2534069ae34f246aecee7035faf19 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Tue, 21 May 2024 16:03:16 +1000 Subject: [PATCH 16/19] passing cov disabled --- libASL/offline_opt.ml | 4 +- libASL/symbolic_lifter.ml | 2 +- libASL/transforms.ml | 168 +++++++++++++++++++++++--------------- 3 files changed, 105 insertions(+), 69 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index aae7f427..cb204b61 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -769,7 +769,7 @@ statement s is the only definition of x reaching u
on every path from s to u t copy-propagated at lift time. *) method stmt_xform (s : stmt) : stmt list = - let cp_cond c = Transforms.BDDSimp.bdd_to_expr (c) (Option.get rtst) in + let cp_cond c = Option.get (Transforms.BDDSimp.bdd_to_expr (Val [c]) (Option.get rtst)) in match s with (* Transform runtime variable decls into expression decls *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> @@ -824,7 +824,7 @@ statement s is the only definition of x reaching u
on every path from s to u t | PropCond cpcond -> let ncp,cp = cp_idents v in let load = Expr_TApply(f, [], [Expr_Var ncp]) in let prop = Expr_Var cp in - let yescpcond = Transforms.BDDSimp.bdd_to_expr cpcond (Option.get rtst) in + let yescpcond = Option.get (Transforms.BDDSimp.bdd_to_expr (Val [cpcond]) (Option.get rtst)) in let vt = Bindings.find v candidates in (* TODO: might be good to check that yes and no are disjoint here *) let e = Expr_If (vt.typ, yescpcond, prop, [] , load) in diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 3bb0abd5..c029fb0a 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -395,7 +395,7 @@ let run include_pc iset pat env = 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 use_rt_copyprop = false in let freachable k = let k = match k with diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 6bab72a2..f37a3a86 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2320,14 +2320,14 @@ module BDDSimp = struct Val (sublist v start wd) + let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) + let full_add_bit l r carry = + let s1,c1 = half_add_bit l r in + let o, c2 = half_add_bit s1 carry in + let ocarry = MLBDD.dor c1 c2 in + o,ocarry + let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)= - let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) in - let full_add_bit l r carry = - let s1,c1 = half_add_bit l r in - let o, c2 = half_add_bit s1 carry in - let ocarry = MLBDD.dor c1 c2 in - o,ocarry - in let xs = List.rev xs in let ys = List.rev ys in match xs,ys with | hx::tlx,hy::tly -> @@ -2338,20 +2338,33 @@ module BDDSimp = struct in carry,bits | _,_ -> failwith "invalid bit strings" - let signed_add_wrap x y = let _,bits = twos_comp_add x y in bits - let signed_negation x = (List.map MLBDD.dnot x) + let signed_add_wrap x y = Printf.printf "SIGNED ADD WRAP\n"; let _,bits = twos_comp_add x y in bits + + + let addone m xs = let one = MLBDD.dtrue m in + let xs = List.rev xs in + let c,rs = match xs with + | hx::tlx -> + let lsb,lscarry = half_add_bit hx one in + let bits,carry = List.fold_left + (fun (acc,carry) (l:MLBDD.t) -> let o,carry = (half_add_bit l carry) in o::acc, carry) + ([lsb], lscarry) tlx + in carry,bits + | _ -> failwith "no" + in rs + + + let signed_negation m (x:MLBDD.t list) = addone m (List.map MLBDD.dnot x) - let signed_sub_wrap x y = let _,bits = twos_comp_add x (signed_negation y) in bits + let signed_sub_wrap m x y = let _,bits = twos_comp_add x (signed_negation m y) in bits + +(* + let signed_lt m x y = + + let signed_gt m x y = List.map MLBDD.dnot (signed_lt m x y) + *) - let signed_lt x y = - let xneg = List.hd x in let yneg = List.hd y in - let carry,subbits = (twos_comp_add x (signed_negation y)) in - let b = MLBDD.dand xneg (MLBDD.dnot yneg) in (* x < 0 < y*) - let b1 = MLBDD.dand (MLBDD.dand xneg yneg) (List.hd subbits) in (* x < y < 0*) - let b2 = MLBDD.dand (MLBDD.dnot (MLBDD.dor xneg yneg)) (MLBDD.dnot (List.hd subbits)) (* 0 < x < y*) - in [MLBDD.dor b (MLBDD.dor b1 b2)] - let signed_gt x y = List.map MLBDD.dnot (signed_lt x y) let eq_bvs a b = let bits = List.map2 MLBDD.eq a b in @@ -2359,8 +2372,39 @@ module BDDSimp = struct | x::xs -> List.fold_right MLBDD.dand xs x | _ -> failwith "bad bits width" - let signed_lte_bits x y = [MLBDD.dor (eq_bvs x y) (List.hd (signed_lt x y))] - let signed_gte_bits x y = [MLBDD.dor (eq_bvs x y) (List.hd (signed_gt x y))] + let sle_bits m x y = + MLBDD.dor + (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) + (MLBDD.dnot (MLBDD.xor (List.hd x) (List.hd y)) ) + + (* https://cs.nyu.edu/pipermail/smt-lib/2007/000182.html *) + + + let bvugt m x y : MLBDD.t = List.fold_left2 (fun acc x y -> MLBDD.dor acc (MLBDD.dand (MLBDD.dnot acc) (MLBDD.dand x (MLBDD.dnot y)))) (MLBDD.dfalse m) x y + let bvult m x y : MLBDD.t = bvugt m y x + let bvule m x y = MLBDD.dor (bvult m x y) (eq_bvs x y) + let bvuge m x y = MLBDD.dor (bvugt m x y) (eq_bvs x y) + let eq_bit a b = MLBDD.dnot (MLBDD.xor a b) + + let bvslt m x y = MLBDD.dor + (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) + (MLBDD.dand (eq_bit (List.hd x) (List.hd y)) (bvult m x y)) + + let bvsgt m x y = bvslt m y x + + let bvsle m x y = MLBDD.dor + (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) + (MLBDD.dand (eq_bit (List.hd x) (List.hd y)) (bvule m x y)) + + let bvsge m x y = bvsle m y x + + let wrap_bv_bool f m x y = match x , y with + | Val x, Val y -> Val [(f m x y)] + | _,_ -> Top + + (* + let signed_gte_bits m x y = [MLBDD.dor (eq_bvs x y) (List.hd (signed_gt m x y))] + *) let twos_comp_sub man (xs : MLBDD.t list) (ys: MLBDD.t list) = () @@ -2397,17 +2441,29 @@ module BDDSimp = struct zero_extend_bits x (int_of_string nw) st | "SignExtend", [w;Expr_LitInt nw], [x; y] -> sign_extend_bits x (int_of_string nw) st - - | "sle_bits", [w], [x; y] -> (match x,y with - | Val x, Val y -> Val (signed_lte_bits x y) - | _,_ -> Top) + | "add_bits", [Expr_LitInt w], [x; y] -> (match x,y with | Val x, Val y -> let r = (signed_add_wrap x y) in assert (List.length r == (int_of_string w)); Val r | _,_ -> Top) | "sub_bits", [w], [x; y] -> (match x,y with - | Val x, Val y -> Val (signed_add_wrap x (signed_negation y)) + | Val x, Val y -> Val (signed_add_wrap x (signed_negation st.man y)) | _,_ -> Top) - | "lsr_bits", [w;w'], [x; y] -> Top + + | "ule_bits", [w], [x; y] -> wrap_bv_bool bvule st.man x y + | "uge_bits", [w], [x; y] -> wrap_bv_bool bvuge st.man x y + | "sle_bits", [w], [x; y] -> wrap_bv_bool bvsle st.man x y + | "sge_bits", [w], [x; y] -> wrap_bv_bool bvsge st.man x y + + + (* + | "slt_bits", [w], [x; y] -> wrap_bv_bool bvslt st.man x y + | "sgt_bits", [w], [x; y] -> wrap_bv_bool bvsgt st.man x y + + | "lsl_bits", [w], [x; y] -> Top + | "lsr_bits", [w], [x; y] -> Top + | "asr_bits", [w], [x; y] -> Top + | "mul_bits", _, [x; y] -> Top + *) | _, _, _ -> Printf.printf "unknown prim %s\n" f; @@ -2473,58 +2529,38 @@ module BDDSimp = struct let bdd_to_expr cond st = - let c = ctx_to_mask st.ctx in - let imps = MLBDD.allprime cond in - let imps = List.map (fun v -> clear_bits v c) imps in - (*let rebuild = List.fold_right (fun vars -> - MLBDD.dor - (List.fold_right (fun (b,v) -> - MLBDD.(dand (if b then ithvar st.man v else dnot (ithvar st.man v))) - ) vars (MLBDD.dtrue st.man)) - ) imps (MLBDD.dfalse st.man) in - let imps = MLBDD.allprime rebuild in *) - let masks = List.map DecoderChecks.implicant_to_mask imps in - let bd_to_test b = - (*("and_bits", [VInt n], [VBits x; VBits y ])*) + let bd_to_test b = let bv = Value.to_mask Unknown (Value.from_maskLit b) in sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv in - (match masks with - | [b] -> bd_to_test b - | bs -> let tests = (List.map bd_to_test (List.tl bs)) in - let boolor a b = Expr_TApply(FIdent("or_bool", 0), [], [a;b]) in - List.fold_left boolor (List.hd tests) (List.tl tests)) - - let rebuild_expr e cond st = match cond with | Val [cond] -> - let c = ctx_to_mask st.ctx in let imps = MLBDD.allprime cond in - let imps = List.map (fun v -> clear_bits v c) imps in - let rebuild = List.fold_right (fun vars -> - MLBDD.dor - (List.fold_right (fun (b,v) -> + let rebuild = List.fold_right (fun vars -> + MLBDD.dor + (List.fold_right (fun (b,v) -> MLBDD.(dand (if b then ithvar st.man v else dnot (ithvar st.man v))) ) vars (MLBDD.dtrue st.man)) ) imps (MLBDD.dfalse st.man) in let imps = MLBDD.allprime rebuild in let masks = List.map DecoderChecks.implicant_to_mask imps in (match masks with - | [b] -> - let bv = Value.to_mask Unknown (Value.from_maskLit b) in - sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv - | _ -> - (* - let try2 = MLBDD.dnot cond in - (if List.length (MLBDD.allprime try2) = 1 then - Printf.printf "Neg candidate %s %s\n" (pp_expr e) (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime try2)) - else - Printf.printf "Can't simp %s %s\n" (pp_expr e) (Utils.pp_list (fun i -> i) masks)); - Printf.printf "Ctx %s\n" (Utils.pp_list DecoderChecks.implicant_to_mask (MLBDD.allprime st.ctx)); *) - e) - | _ -> - Printf.printf "no value %s %s\n" (pp_expr e) (pp_abs cond); - e + | [] -> None + | [b] -> Some (bd_to_test b) + | b::bs -> + let try2 = MLBDD.dnot cond |> MLBDD.allprime |> List.map DecoderChecks.implicant_to_mask in + match try2 with + | [b] -> Some (Expr_TApply (FIdent ("not_bool", 0), [], [bd_to_test b])) + | _ -> (let r = (let tests = (List.map bd_to_test (b::bs)) in + let bool_or x y = Expr_TApply(FIdent("or_bool", 0), [], [x;y]) in + List.fold_left bool_or (List.hd tests) (List.tl tests)) in + Some r) + ) + | _ -> None + + let rebuild_expr e cond st = match bdd_to_expr cond st with + | Some x -> x + | None -> Printf.printf "Unable to simplify expr" ; e class nopvis = object(self) From e7b760f8287e15d9b71a8bf7864dff73691365e6 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Tue, 21 May 2024 18:58:10 +1000 Subject: [PATCH 17/19] test and fix bdd sle/slt --- libASL/transforms.ml | 34 ++++++++++++--------- tests/bdd_ops.ml | 73 ++++++++++++++++++++++++++++++++++++++++++++ tests/dune | 8 +++++ 3 files changed, 101 insertions(+), 14 deletions(-) create mode 100644 tests/bdd_ops.ml diff --git a/libASL/transforms.ml b/libASL/transforms.ml index f37a3a86..76e6922d 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2322,32 +2322,32 @@ module BDDSimp = struct let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) let full_add_bit l r carry = - let s1,c1 = half_add_bit l r in - let o, c2 = half_add_bit s1 carry in + let c1,s1 = half_add_bit l r in + let c2,o = half_add_bit s1 carry in let ocarry = MLBDD.dor c1 c2 in - o,ocarry + ocarry,o let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)= let xs = List.rev xs in let ys = List.rev ys in match xs,ys with | hx::tlx,hy::tly -> - let lsb,lscarry = half_add_bit hx hy in + let lscarry,lsb = half_add_bit hx hy in let bits,carry = List.fold_left2 - (fun (acc,carry) (l:MLBDD.t) (r:MLBDD.t) -> let o,carry = (full_add_bit l r carry) in o::acc, carry) + (fun (acc,carry) (l:MLBDD.t) (r:MLBDD.t) -> let carry,o = (full_add_bit l r carry) in o::acc , carry) ([lsb], lscarry) tlx tly in carry,bits | _,_ -> failwith "invalid bit strings" - let signed_add_wrap x y = Printf.printf "SIGNED ADD WRAP\n"; let _,bits = twos_comp_add x y in bits - + let signed_add_wrap x y = let _,bits = twos_comp_add x y in bits + let addone m xs = let one = MLBDD.dtrue m in let xs = List.rev xs in let c,rs = match xs with | hx::tlx -> - let lsb,lscarry = half_add_bit hx one in + let lscarry,lsb = half_add_bit hx one in let bits,carry = List.fold_left - (fun (acc,carry) (l:MLBDD.t) -> let o,carry = (half_add_bit l carry) in o::acc, carry) + (fun (acc,carry) (l:MLBDD.t) -> let carry,o = (half_add_bit l carry) in o::acc, carry) ([lsb], lscarry) tlx in carry,bits | _ -> failwith "no" @@ -2380,11 +2380,18 @@ module BDDSimp = struct (* https://cs.nyu.edu/pipermail/smt-lib/2007/000182.html *) - let bvugt m x y : MLBDD.t = List.fold_left2 (fun acc x y -> MLBDD.dor acc (MLBDD.dand (MLBDD.dnot acc) (MLBDD.dand x (MLBDD.dnot y)))) (MLBDD.dfalse m) x y + let eq_bit a b = MLBDD.dnot (MLBDD.xor a b) + + let bvugt m s t : MLBDD.t = let a, b = (List.fold_left2 (fun (gt, bnotsetfirst) a b -> + MLBDD.dor gt (MLBDD.dand (bnotsetfirst) ((MLBDD.dand a (MLBDD.dnot b)))), (* false until a > b*) + MLBDD.dand bnotsetfirst (MLBDD.dnot (MLBDD.dand (MLBDD.dnot gt) (MLBDD.dand b (MLBDD.dnot a)))) (* true until a < b*) + ) + (MLBDD.dfalse m, MLBDD.dtrue m) (s) (t)) + in (MLBDD.dand a b) + let bvult m x y : MLBDD.t = bvugt m y x let bvule m x y = MLBDD.dor (bvult m x y) (eq_bvs x y) let bvuge m x y = MLBDD.dor (bvugt m x y) (eq_bvs x y) - let eq_bit a b = MLBDD.dnot (MLBDD.xor a b) let bvslt m x y = MLBDD.dor (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) @@ -2453,12 +2460,11 @@ module BDDSimp = struct | "uge_bits", [w], [x; y] -> wrap_bv_bool bvuge st.man x y | "sle_bits", [w], [x; y] -> wrap_bv_bool bvsle st.man x y | "sge_bits", [w], [x; y] -> wrap_bv_bool bvsge st.man x y - - - (* | "slt_bits", [w], [x; y] -> wrap_bv_bool bvslt st.man x y | "sgt_bits", [w], [x; y] -> wrap_bv_bool bvsgt st.man x y + (* + | "lsl_bits", [w], [x; y] -> Top | "lsr_bits", [w], [x; y] -> Top | "asr_bits", [w], [x; y] -> Top diff --git a/tests/bdd_ops.ml b/tests/bdd_ops.ml new file mode 100644 index 00000000..f59d5ffa --- /dev/null +++ b/tests/bdd_ops.ml @@ -0,0 +1,73 @@ +open LibASL +open Asl_utils +open AST +open LibASL.Primops +open LibASL.Utils + +module TC = Tcheck +module AST = Asl_ast + +let man = MLBDD.init ~cache:1024 () + + +let from_bitsLit x = + let x' = Value.drop_chars x ' ' in + (Primops.mkBits (String.length x') (Z.of_string_base 2 x')) + +let it i = assert (MLBDD.is_true i || MLBDD.is_false i ) ; MLBDD.is_true i + +let bdd_to_bv (b:MLBDD.t list) = let l = List.map (fun i -> + assert (MLBDD.is_true i || MLBDD.is_false i ) ; MLBDD.is_true i) b + in let l = List.map (function + | true -> '1' + | false -> '0') l |> List.to_seq |> String.of_seq in + from_bitsLit l + +let prim_cvt_bits_str (x: bitvector): string = + let n = Z.of_int x.n in + if Z.equal n Z.zero then begin + "''" + end else begin + let s = Z.format "%0b" x.v in + let pad = String.make (Z.to_int n - String.length s) '0' in + pad ^ s + end + + +let bv_to_bdd (bv:bitvector) = + let l = prim_cvt_bits_str bv in + let l = String.to_seq l |> List.of_seq in + List.map (function + | '1' -> MLBDD.dtrue man + | '0' -> MLBDD.dfalse man + | x -> failwith (Printf.sprintf "no %c" x) ) l + +let ppbit = prim_cvt_bits_str + + + +let test_add = + let width = 8 in + let cases = List.init 256 (fun i -> (i - 128)) in + let cases_bits = List.map (fun i -> mkBits width (Z.of_int i)) cases in + let cases_bdd = List.map bv_to_bdd cases_bits in + let compar = List.concat_map (fun i -> List.map (fun j -> i , j) cases_bits) cases_bits in + let to_check = List.concat_map (fun i -> List.map (fun j -> i , j) cases_bdd) cases_bdd in + let res_add = List.map2 (fun (i,j) (i', j') -> (i, j), prim_add_bits i j, bdd_to_bv (LibASL.Transforms.BDDSimp.signed_add_wrap i' j')) compar to_check in + List.iter (fun ((i,j),c,r) -> Alcotest.(check string) (Printf.sprintf "%s + %s = %s" (ppbit i) (ppbit j) (ppbit c)) (prim_cvt_bits_str c) (prim_cvt_bits_str r)) res_add ; + + let res_sub = List.map2 (fun (i,j) (i', j') -> (i, j), prim_sub_bits i j, bdd_to_bv (LibASL.Transforms.BDDSimp.signed_sub_wrap man i' j')) compar to_check in + List.iter (fun ((i,j),c,r) -> Alcotest.(check string) (Printf.sprintf "%s - %s = %s" (ppbit i) (ppbit j) (ppbit c)) (prim_cvt_bits_str c) (prim_cvt_bits_str r)) res_sub ; + + let compare_binop format f1 f2 = + let res = List.map2 (fun (i,j) (i', j') -> (i, j), f1 i j, (f2 i' j')) compar to_check in + List.iter (fun ((i,j),c,r) -> Alcotest.(check bool) (Printf.sprintf format (ppbit i) (ppbit j) (c)) (c) r) res in + compare_binop "%s > %s = %b" (fun x y -> prim_gt_int (Primops.prim_cvt_bits_uint x) (Primops.prim_cvt_bits_uint y)) (fun x y -> it (LibASL.Transforms.BDDSimp.bvugt man x y)) ; + compare_binop "%s < %s = %b" (fun x y -> prim_lt_int (Primops.prim_cvt_bits_sint x) (Primops.prim_cvt_bits_sint y)) (fun x y -> it (LibASL.Transforms.BDDSimp.bvslt man x y)) ; + compare_binop "%s <= %s = %b" (fun x y -> prim_le_int (Primops.prim_cvt_bits_sint x) (Primops.prim_cvt_bits_sint y)) (fun x y -> it (LibASL.Transforms.BDDSimp.bvsle man x y)) ; + + + + + + diff --git a/tests/dune b/tests/dune index 1c01889f..8b603284 100644 --- a/tests/dune +++ b/tests/dune @@ -1,4 +1,12 @@ (test (name test_asl) (modes exe) (flags (-cclib -lstdc++)) + (modules test_asl) + (libraries alcotest libASL)) + + +(test (name bdd_ops) + (modes exe) + (flags (-cclib -lstdc++)) +(modules bdd_ops) (libraries alcotest libASL)) From a59eab861b53a0da75b566e94e6f4133e26e69af Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 22 May 2024 18:27:26 +1000 Subject: [PATCH 18/19] progress --- libASL/offline_opt.ml | 249 +++++++++++++++++++++----------------- libASL/symbolic_lifter.ml | 7 +- libASL/transforms.ml | 12 +- 3 files changed, 147 insertions(+), 121 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index cb204b61..aae2ac29 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -44,6 +44,7 @@ let is_var_decl f = f = Offline_transform.rt_decl_bv || f = Offline_transform.rt_decl_bool + (* module CopyProp = struct type clas = Declared | @@ -306,6 +307,7 @@ module CopyProp = struct Asl_visitor.visit_stmts v body end +*) module DeadContextSwitch = struct (* Backwards walk to reduce consecutive context switches. @@ -340,7 +342,7 @@ module RtCopyProp = struct match c with | Declared -> "Declared" | Defined ids -> "Defined (" ^ pp_identset ids ^ ")" - | Clobbered ids -> "Clobbered" + | Clobbered ids -> "Clobbered (" ^ pp_identset ids ^ ")" | Essential -> "Essential" let merge_clas a b = @@ -378,7 +380,10 @@ module RtCopyProp = struct (* maps idents to the condution under which they are clobbered *) cond_clobbered: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) (* maps idents to the condition under which they are read after clobbering *) - cond_read_after_clobber: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) + cond_read: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) + + (*deps: IdentSet.t Bindings.t; (* ident -> ident *) *) + (* not used; stores dep sets for bindings (and the def reachability) *) cond_dep: (MLBDD.t * IdentSet.t) Bindings.t; (* binding -> condition * deps *) (**) @@ -389,16 +394,19 @@ module RtCopyProp = struct type olt = MLBDD.t + let pp_state st = + (pp_bindings pp_clas st.var_clas) ^ "\n" ^ + "cond read: " ^ + (pp_bindings (fun i -> Printf.sprintf "%s\n" (Transforms.BDDSimp.pp_abs (Val [i]))) st.cond_read) ^ + "\ncond clob: " ^ + (pp_bindings (fun i -> Printf.sprintf "%s\n" (Transforms.BDDSimp.pp_abs (Val [i]))) st.cond_clobbered) + + let pp_essential st = + pp_bindings pp_clas (Bindings.filter (fun f v -> v = Essential) st.var_clas) let set_var v k st = let var_clas = Bindings.add v k st.var_clas in (* TODO: need to be adapted for new lattice ? *) - let _ = match k with - | Declared -> () - | Defined x -> () - | Clobbered i -> () - | Essential -> () - in { st with var_clas } @@ -415,52 +423,66 @@ module RtCopyProp = struct let add_conds is c bs = cond_merge bs (Seq.map (fun i -> i, c) is |> Bindings.of_seq) + + (* only update deps *) let clobber_var v st = let var_clas = Bindings.map (fun c -> match c with Defined ids | Clobbered ids when IdentSet.mem v ids -> Clobbered ids | _ -> c) st.var_clas in - let deps = Bindings.filter_map (fun i c -> match c with - | Defined ids - | Clobbered ids when IdentSet.mem v ids -> Some (st.bdd.ctx) - | _ -> None) var_clas in - let cond_clobbered = cond_merge st.cond_clobbered deps in - { st with var_clas ; cond_clobbered } + (*let st = {st with cond_clobbered = (add_cond v (st.bdd.ctx) st.cond_clobbered)} in *) + let st = Seq.fold_left (fun st (i,c) -> + match c with + | Defined ids + | Clobbered ids when IdentSet.mem v ids + -> {st with cond_clobbered = (add_cond v (st.bdd.ctx) st.cond_clobbered)} + | _ -> st + ) st (Bindings.to_seq var_clas) in + { st with var_clas } - let get_var v st = Bindings.find_opt v st.var_clas + let update_clobbers st = + (* update everything based on the conditions of their dependencies *) + let ids = Bindings.to_seq st.cond_clobbered in + Seq.fold_left (fun st (iv,cond) -> + let var_clas = Bindings.map (fun c -> match c with Defined ids | Clobbered ids when IdentSet.mem iv ids -> Clobbered ids | _ -> c) st.var_clas in + let st = Seq.fold_left (fun st (ii,c) -> match c with + | Defined ids + | Clobbered ids when IdentSet.mem ii ids -> {st with cond_clobbered = (add_cond ii cond st.cond_clobbered)} + | _ -> st + ) st (Bindings.to_seq var_clas) in + { st with var_clas } + ) st ids - let merge_st (cond: Transforms.BDDSimp.abs) a b = - let ctx = a.ctx in - let unpack x = match x with - | Transforms.BDDSimp.Val [a] -> Some a - | Transforms.BDDSimp.Val (h::tl) -> failwith "why?" - | _ -> None - in - let merged_bdd a b = Bindings.merge (fun (k:ident) (a) (b) -> match a,b with - | Some a, Some b -> (unpack (Transforms.BDDSimp.join_abs cond (Val [a]) (Val [b]))) - | Some a, None -> Some a - | None, Some a -> Some a - | None, None -> None) a b in - let cond_clobbered = merged_bdd a.cond_clobbered b.cond_clobbered in - let cond_read_after_clobber = merged_bdd a.cond_read_after_clobber b.cond_read_after_clobber in + + let get_var v st = Bindings.find_opt v st.var_clas + + let merge_st (ts:MLBDD.t) (fs:MLBDD.t) (joined: Transforms.BDDSimp.state) xa xb = + let merge_cond a b = (MLBDD.dor (MLBDD.dand ts a) (MLBDD.dand fs b)) in + let merged_bdd = Bindings.merge (fun (k:ident) a b -> match a,b with + | Some a, Some b -> Some (merge_cond a b) + | Some a, None -> Some (MLBDD.dand ts a) + | None, Some a -> Some (MLBDD.dand fs a) + | None, None -> None) in + let cond_clobbered = merged_bdd xa.cond_clobbered xb.cond_clobbered in + let cond_read = merged_bdd xa.cond_read xb.cond_read in let cond_dep = Bindings.merge (fun k a b -> match a,b with - | Some (isa, a), Some (isb, b) -> Option.map (fun x -> x, IdentSet.union a b) (unpack (Transforms.BDDSimp.join_abs cond (Val [isa]) (Val [isb]))) - | Some a, None -> Some a - | None, Some a -> Some a + | Some (isa, a), Some (isb, b) -> Option.map (fun x -> x, IdentSet.union a b) (Some (merge_cond isa isb)) + | Some (isa, a), None -> Some (MLBDD.dand ts isa, a) + | None, Some (isa, a) -> Some (MLBDD.dand fs isa, a) | _ -> None - ) a.cond_dep b.cond_dep in + ) xa.cond_dep xb.cond_dep in let var_clas = Bindings.merge (fun k a b -> match a, b with | Some a, Some b -> Some (merge_clas a b) | Some a, None | None, Some a -> Some a - | None, None -> None) a.var_clas b.var_clas in - let bdd = Transforms.BDDSimp.join_state cond a.bdd b.bdd in - { bdd; var_clas ; ctx ; cond_clobbered; cond_read_after_clobber; cond_dep } + | None, None -> None) xa.var_clas xb.var_clas in + let st : state = {xa with bdd=joined; var_clas ; cond_clobbered=cond_clobbered; cond_read=cond_read; cond_dep=cond_dep } in + st let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; var_clas = Bindings.empty; ctx = []; cond_clobbered = Bindings.empty ; - cond_read_after_clobber = Bindings.empty ; + cond_read = Bindings.empty ; cond_dep = Bindings.empty} let push_context m st = { st with ctx = m::st.ctx } @@ -483,30 +505,40 @@ module RtCopyProp = struct type xform = | Prop - | PropCond of MLBDD.t (* copyprop not allowed , should copyprop *) + | PropCond of MLBDD.t (* encoding whether prop is allowed *) | No let read_var v (st,i) = + let st = {st with cond_read = (add_cond v (st.bdd.ctx) st.cond_read )} in match get_var v st with (* Reading undeclared generally means a value that is gradually constructed through partial updates *) - | Some (Declared) -> - (set_var v Essential st, i) + | Some (Declared) -> (set_var v Essential st, i) (* Reading clobbered implies we cannot reorder *) - | Some (Clobbered ids) -> ( - (* record read reachability *) - let clobbered = (Bindings.find v st.cond_clobbered) in - let read_after_clobber = MLBDD.dand clobbered (st.bdd.ctx) in - let st = {st with cond_read_after_clobber = (add_cond v read_after_clobber st.cond_read_after_clobber)} in - st, i ) + | Some (Clobbered deps) -> (st, IdentSet.union i deps) (*if (Transforms.BDDSimp.is_true clobbered st.bdd) then (set_var v Essential st, i) else st, i) *) (* Collect ids for transitive walk given a defined variable *) - | Some (Defined ids) -> - (st, IdentSet.union i ids) + | Some (Defined ids) -> (st, IdentSet.union i ids) | _ -> (st, i) + let write_var v (st,i) = + let st = if has_context st then (Printf.printf "rt branch dependent\n" ; set_var v Essential st) else st in + (* cannot copy-prop exprs dependent on a run-time branch*) + let st = clobber_var v st in + Printf.printf "PRE STORE(%s) : %s\n" (pprint_ident v) (pp_state st); + let st = {st with cond_clobbered = (add_cond v (st.bdd.ctx) st.cond_clobbered )} in + let (st,i) = match get_var v st with + | Some (Declared) -> (set_var v (Defined i) st, i) + | Some (Defined ids) -> ((set_var v (Clobbered i) st), i) + | Some (Clobbered deps) -> (st, i) + | Some Essential -> (st, i) + | None -> (Printf.printf "BEANLESS\n"); (st, i) + in Printf.printf "POST STORE: %s\n" (pp_state st); (st,i) + + let impure_ident = Ident "CopyProp_impure" let read_vars (vs: IdentSet.t) (st: state): state = + Printf.printf "READ "; IdentSet.iter (fun i -> Printf.printf "%s " (pprint_ident i)) vs ; Printf.printf "\n"; let read_set s st = IdentSet.fold read_var s (st,IdentSet.empty) in (* If impure is in the readset, the reads are not pure. Clobber any impure dependencies now. *) let st = if IdentSet.mem impure_ident vs then clobber_var impure_ident st else st in @@ -521,7 +553,7 @@ module RtCopyProp = struct (* TODO: Updating, check if this has some context dependence *) let update_deps v deps st = - if has_context st then set_var v Essential st (* cannot copy-prop exprs dependent on a run-time branch*) + if has_context st then (Printf.printf "rt branch dependent\n" ; set_var v Essential st) (* cannot copy-prop exprs dependent on a run-time branch*) else match get_var v st with | Some (Declared) -> @@ -566,11 +598,6 @@ module RtCopyProp = struct let _ = Asl_visitor.visit_expr v e in v#get_deps - let pp_state st = - pp_bindings pp_clas st.var_clas - - let pp_essential st = - pp_bindings pp_clas (Bindings.filter (fun f v -> v = Essential) st.var_clas) @@ -578,6 +605,7 @@ module RtCopyProp = struct match s with (* Var decl *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> + Printf.printf "decl %s\n" (pprint_ident v); decl_var v st (* Var assign *) @@ -586,9 +614,10 @@ module RtCopyProp = struct let deps = get_deps e in let st = read_vars deps st in (* Clobber anything dependent on v *) - let st = clobber_var v st in + let st,deps = write_var v (st,deps) in (* Update deps for v *) - update_deps v deps st + st + (*update_deps v deps st*) (* Array assign *) | Stmt_TCall(f, [], [Expr_Var a; i; e], loc) when is_array_store f -> @@ -596,7 +625,8 @@ module RtCopyProp = struct let deps = get_deps e in let st = read_vars deps st in (* Clobber anything dependent on a *) - clobber_var a st + let st,deps = write_var a (st,deps) in + st (* Assert *) | Stmt_TCall(f, [], [e], loc) when is_assert f -> @@ -605,8 +635,11 @@ module RtCopyProp = struct read_vars deps st (* LiftTime branch *) - | Stmt_If(c, t, [], f, loc) -> st (* handled by caller splitting, walking children, and joining *) + | Stmt_If(c, t, [], f, loc) -> (* merge in the bdds as well *) + let deps = get_deps c in + read_vars deps st + (* branches handled by caller splitting, walking children, and joining *) (* let cond = Transforms.BDDSimp.eval_expr c st.bdd in @@ -653,12 +686,6 @@ module RtCopyProp = struct and walk_stmts s st : state = List.fold_left (fun st s -> walk_stmt s st) st s - let candidate_var v st = - match get_var v st with - | Some Essential -> false - | None -> false - | _ -> true - (* To change this, you'd need to know : - The condition under which its safe to copy prop @@ -679,23 +706,6 @@ module RtCopyProp = struct statement s is the only definition of x reaching u
on every path from s to u there are no assignments to y
 *) - class copyprop_transform st = object - inherit Asl_visitor.nopAslVisitor - method! vexpr = function - (* Transform loads into direct variable accesses *) - | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f && candidate_var v st -> - ChangeTo (Expr_Var v) - | _ -> DoChildren - method! vstmt = function - (* Transform runtime variable decls into expression decls *) - | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f && candidate_var v st -> - ChangeDoChildrenPost([Stmt_VarDeclsNoInit(Offline_transform.rt_expr_ty, [v], loc)], fun e -> e) - (* Transform stores into assigns *) - | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f && candidate_var v st -> - ChangeDoChildrenPost([Stmt_Assign(LExpr_Var v, e, loc)], fun e -> e) - | _ -> DoChildren - end - (* @@ -705,22 +715,29 @@ statement s is the only definition of x reaching u
on every path from s to u t match get_var v st with | Some Essential -> No | Some Clobbered deps -> - let c = Bindings.find_opt v st.cond_read_after_clobber in - (match c with - | Some x -> (if (Transforms.BDDSimp.is_true (Val [x]) rtst) then ( - (* we don't need to generate a condition at read if we know statically *) - Printf.printf "Condcopyprop: var %s BDD %s simplifies to TRUE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [x])); - No) - else if (Transforms.BDDSimp.is_false (Val [x]) rtst) then ( - Printf.printf "Condcopyprop: var %s BDD %s simplifies to FALSE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [x])) ; + let c = Bindings.find_opt v st.cond_read in + let b = Bindings.find_opt v st.cond_clobbered in + (match c,b with + | Some read,Some clob -> + let cond = (MLBDD.dand read (MLBDD.dnot clob)) in + (if (Transforms.BDDSimp.is_true (Val [cond]) rtst) then + ( + Printf.printf "Condcopyprop prop var %s read => clobbered %s simplifies to FALSE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [MLBDD.dand read (MLBDD.dnot clob)])) ; Prop - ) - else PropCond (MLBDD.dnot x)) - | None -> Printf.printf "Condcopyprop: Clobbered variable missing cond read %s\n" (pprint_ident v); + ) + else + if (Transforms.BDDSimp.is_false (Val [cond]) rtst) then + ( + (* we don't need to generate a condition at read if we know statically *) + Printf.printf "Condcopyprop noprop var %s read => clobbered %s simplifies to TRUE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [cond])); + No) + else PropCond (cond)) + | Some _, None -> Printf.printf "UNCONCD PROP\n" ; Prop + | _,_ -> Printf.printf "Condcopyprop: Clobbered variable missing cond read %s\n" (pprint_ident v); No) (* TODO: clobbered but not subsequently read? *) - | Some Defined _ -> Prop - | Some Declared -> No - | None -> Printf.printf "Unexpected variable with no candidate decision status %s\n" (pprint_ident v); No + | Some Defined _ -> Printf.printf "Condcopyprop ONLY DEFINED %s\n" (pprint_ident v); Prop + | Some Declared -> No + | None -> No @@ -732,13 +749,6 @@ statement s is the only definition of x reaching u
on every path from s to u t typ: ty } - class copyprop_vis icpst = object(self) - inherit Asl_visitor.nopAslVisitor - val mutable cpst = icpst - - method xfer_stmt s = cpst <- walk_stmt s cpst - method join cond os = cpst <- merge_st cond cpst os - end class cond_copyprop_transform cpst = object(self) @@ -775,28 +785,28 @@ statement s is the only definition of x reaching u
on every path from s to u t | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> candidates <- Bindings.add v {typ=t} candidates; (match (cond_candidate v cpst (Option.get rtst)) with - (* essential, leave as-is *) | No -> Printf.printf "Condcopyprop: NOT PROP at DEFINITION of var %s\n " (pprint_ident v); [s] - (* move run-time to lift-time *) | Prop -> - Printf.printf "Condcopyprop: UNCOND prop at DEFINITION of var %s\n " (pprint_ident v); + (* move run-time to lift-time *) + (*Printf.printf "Condcopyprop: UNCOND prop at DEFINITION of var %s\n " (pprint_ident v); *) [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [snd (cp_idents v)], Unknown)] - | PropCond cond -> let ncp,cp = cp_idents v in - Printf.printf "Condcopyprop: CONDITIONAL prop at DEFINITION : %s\n " (Transforms.BDDSimp.pp_abs (Val [cond])); - let c = cp_cond cond in - (Printf.printf("Successfully simplified bdd cond to %s on stmt %s \n") (pp_expr c) (pp_stmt s) ; + | PropCond cond -> + let ncp,cp = cp_idents v in + (* if (cond) lift-time else run-time *) + Printf.printf "Condcopyprop: CONDITIONAL prop at DEFINITION %s: %s\n " (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [cond])); + (*let c = cp_cond cond in *) (* lift-time conditionally generates the copy-propagated or non-propagated form *) [ Stmt_ConstDecl (Offline_transform.rt_expr_ty, ncp, Expr_TApply(f, [], args), Unknown); Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], Unknown); - ]) + ] ) (* Transform stores into assigns *) | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> (match (cond_candidate v cpst (Option.get rtst)) with - | No -> (Printf.printf "Condcopyprop: UNCOND DISABLE PROP on STORE of var %s\n " (pprint_ident v)); [s] + | No -> (*(Printf.printf "Condcopyprop: UNCOND DISABLE PROP on STORE of var %s\n " (pprint_ident v));*) [s] | Prop -> (Printf.printf "Condcopyprop: UNCOND RT PROP on STORE of var %s\n " (pprint_ident v); [(Stmt_Assign (LExpr_Var (snd (cp_idents v)), e, loc))]) @@ -835,14 +845,25 @@ statement s is the only definition of x reaching u
on every path from s to u t | _ -> e end - module AnalysisLat = struct type rt = state type olt = Transforms.BDDSimp.state let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = (*Printf.printf "%s ::\n%s\n" (pp_stmt s) (Transforms.BDDSimp.pp_state l);*) (walk_stmt s r,[s]) - let join (ol:olt) (rta: rt) (rtb: rt) = merge_st (Val[ol.ctx]) rta rtb + let join (ts:olt) (fs:olt) (js:olt) (rta: rt) (rtb: rt) = Printf.printf "ts %s fs %s" + (Transforms.BDDSimp.pp_abs (Val [ts.ctx])) + (Transforms.BDDSimp.pp_abs (Val [fs.ctx])) + ; + Printf.printf "\n--------------\n"; + let p s rta = Printf.printf "%s: %s\n" s (pp_state rta) in + p "\nTRUE BRANCH: " rta; p "\nFALSE BRANCH: " rtb ; + + let j = merge_st ts.ctx fs.ctx (js:olt) rta rtb in + p "\nJOIN STATE: " j; + Printf.printf "\n==============\n"; + j + let init s = init_state s end @@ -851,7 +872,7 @@ statement s is the only definition of x reaching u
on every path from s to u t type rt = {cpst: cond_copyprop_transform} type olt = Transforms.BDDSimp.state let xfer_stmt ol ss s = ss,ss.cpst#xf_stmt s ol - let join r a b = if (a != b) then (failwith "not allowed") else a (* only have one instance of the object so should be fine *) + let join t f j a b = if (a != b) then (failwith "not allowed") else a (* only have one instance of the object so should be fine *) let init st = {cpst = new cond_copyprop_transform st} end diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index c029fb0a..b869caa7 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -365,7 +365,7 @@ let run include_pc iset pat env = 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 debug = true 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 @@ -392,10 +392,10 @@ let run include_pc iset pat env = (* Perform offline PE *) Printf.printf "Stages 7-8: Offline Transform\n"; 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.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 = false in + let use_rt_copyprop = true in let freachable k = let k = match k with @@ -405,6 +405,7 @@ let run include_pc iset pat env = 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 + Transforms.BDDSimp.print_unknown_prims (); let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 76e6922d..fdb9c68c 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -2113,7 +2113,7 @@ module type RTAnalysisLattice = sig type rt (* RT lattice type *) type olt (* LT lattice type *) val xfer_stmt : olt -> rt -> stmt -> rt*stmt list - val join: olt -> rt -> rt -> rt + val join: olt -> olt -> olt -> rt -> rt -> rt end module BDDSimp = struct @@ -2136,7 +2136,7 @@ module BDDSimp = struct type rt = unit type olt = state let xfer_stmt o r s = r,[s] - let join o r ro = () + let join o c j r ro = () let init _ = () end @@ -2379,6 +2379,9 @@ module BDDSimp = struct (* https://cs.nyu.edu/pipermail/smt-lib/2007/000182.html *) + let unknown_prims = ref Bindings.empty + let print_unknown_prims (c:unit) = Bindings.to_seq !unknown_prims |> List.of_seq |> List.sort (fun a b -> compare (snd a) (snd b)) + |> List.iter (fun (id,c) -> Printf.printf "%d \t : %s\n" c (pprint_ident id)) let eq_bit a b = MLBDD.dnot (MLBDD.xor a b) @@ -2472,7 +2475,8 @@ module BDDSimp = struct *) | _, _, _ -> - Printf.printf "unknown prim %s\n" f; + unknown_prims := (Bindings.find_opt (Ident f) !unknown_prims) |> (function Some x -> x + 1 | None -> 0) + |> (fun x -> Bindings.add (Ident f) x !unknown_prims) ; Top let rec eval_expr e st = @@ -2627,7 +2631,7 @@ module BDDSimp = struct let tst,xsa = eval_stmts xs tstmts (restrict_ctx cond {st with stmts = []}) in let fst,xsb = eval_stmts xs fstmts (restrict_ctx ncond {st with stmts = []}) in let st' = join_state cond tst fst in - let xs = Xf.join st' xsa xsb in + let xs = Xf.join tst fst st' xsa xsb in let st' = writeall st.stmts st' in let st' = write (Stmt_If (c, tst.stmts, [], fst.stmts, loc)) st' in From 6ec52950a7f3f452e753206b59213daa9669067d Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 22 May 2024 18:56:08 +1000 Subject: [PATCH 19/19] possibly working --- libASL/offline_opt.ml | 22 +++++++++------------- libASL/symbolic_lifter.ml | 2 +- 2 files changed, 10 insertions(+), 14 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index aae2ac29..3ef7a2bd 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -432,7 +432,7 @@ module RtCopyProp = struct match c with | Defined ids | Clobbered ids when IdentSet.mem v ids - -> {st with cond_clobbered = (add_cond v (st.bdd.ctx) st.cond_clobbered)} + -> {st with cond_clobbered = (add_cond i (st.bdd.ctx) st.cond_clobbered)} | _ -> st ) st (Bindings.to_seq var_clas) in { st with var_clas } @@ -521,24 +521,21 @@ module RtCopyProp = struct | _ -> (st, i) let write_var v (st,i) = - let st = if has_context st then (Printf.printf "rt branch dependent\n" ; set_var v Essential st) else st in + let st = if has_context st then (set_var v Essential st) else st in (* cannot copy-prop exprs dependent on a run-time branch*) let st = clobber_var v st in - Printf.printf "PRE STORE(%s) : %s\n" (pprint_ident v) (pp_state st); - let st = {st with cond_clobbered = (add_cond v (st.bdd.ctx) st.cond_clobbered )} in let (st,i) = match get_var v st with | Some (Declared) -> (set_var v (Defined i) st, i) | Some (Defined ids) -> ((set_var v (Clobbered i) st), i) | Some (Clobbered deps) -> (st, i) | Some Essential -> (st, i) - | None -> (Printf.printf "BEANLESS\n"); (st, i) - in Printf.printf "POST STORE: %s\n" (pp_state st); (st,i) + | None -> (st, i) + in (st,i) let impure_ident = Ident "CopyProp_impure" let read_vars (vs: IdentSet.t) (st: state): state = - Printf.printf "READ "; IdentSet.iter (fun i -> Printf.printf "%s " (pprint_ident i)) vs ; Printf.printf "\n"; let read_set s st = IdentSet.fold read_var s (st,IdentSet.empty) in (* If impure is in the readset, the reads are not pure. Clobber any impure dependencies now. *) let st = if IdentSet.mem impure_ident vs then clobber_var impure_ident st else st in @@ -553,7 +550,7 @@ module RtCopyProp = struct (* TODO: Updating, check if this has some context dependence *) let update_deps v deps st = - if has_context st then (Printf.printf "rt branch dependent\n" ; set_var v Essential st) (* cannot copy-prop exprs dependent on a run-time branch*) + if has_context st then (set_var v Essential st) (* cannot copy-prop exprs dependent on a run-time branch*) else match get_var v st with | Some (Declared) -> @@ -605,7 +602,6 @@ module RtCopyProp = struct match s with (* Var decl *) | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> - Printf.printf "decl %s\n" (pprint_ident v); decl_var v st (* Var assign *) @@ -722,20 +718,20 @@ statement s is the only definition of x reaching u
on every path from s to u t let cond = (MLBDD.dand read (MLBDD.dnot clob)) in (if (Transforms.BDDSimp.is_true (Val [cond]) rtst) then ( - Printf.printf "Condcopyprop prop var %s read => clobbered %s simplifies to FALSE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [MLBDD.dand read (MLBDD.dnot clob)])) ; + (*Printf.printf "Condcopyprop prop var %s read => clobbered %s simplifies to FALSE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [MLBDD.dand read (MLBDD.dnot clob)])) ; *) Prop ) else if (Transforms.BDDSimp.is_false (Val [cond]) rtst) then ( (* we don't need to generate a condition at read if we know statically *) - Printf.printf "Condcopyprop noprop var %s read => clobbered %s simplifies to TRUE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [cond])); + (*Printf.printf "Condcopyprop noprop var %s read => clobbered %s simplifies to TRUE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [cond])); *) No) else PropCond (cond)) | Some _, None -> Printf.printf "UNCONCD PROP\n" ; Prop - | _,_ -> Printf.printf "Condcopyprop: Clobbered variable missing cond read %s\n" (pprint_ident v); + | _,_ -> (*Printf.printf "Condcopyprop: Clobbered variable missing cond read %s\n" (pprint_ident v); *) No) (* TODO: clobbered but not subsequently read? *) - | Some Defined _ -> Printf.printf "Condcopyprop ONLY DEFINED %s\n" (pprint_ident v); Prop + | Some Defined _ -> (*Printf.printf "Condcopyprop ONLY DEFINED %s\n" (pprint_ident v);*) Prop | Some Declared -> No | None -> No diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index b869caa7..cd3a7e03 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -365,7 +365,7 @@ let run include_pc iset pat env = 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 = true in + 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