From 391419864f8d6550b12f31b413d5862599c5c178 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 20 Dec 2024 08:29:59 +1000 Subject: [PATCH 1/5] Fix take/drop list utils --- libASL/utils.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/libASL/utils.ml b/libASL/utils.ml index b0e08dcb..dc6a4382 100644 --- a/libASL/utils.ml +++ b/libASL/utils.ml @@ -37,14 +37,14 @@ let to_string (d: PPrint.document): string = let rec take (n: int) (xs: 'a list) = match xs with | _ when n < 0 -> failwith "take: negative" - | [] when n = 0 -> [] + | l when n = 0 -> [] | [] -> failwith "take: list too short" | x::rest -> x :: take (n-1) rest let rec drop (n: int) (xs: 'a list) = match xs with | _ when n < 0 -> failwith "drop: negative" - | [] when n = 0 -> [] + | l when n = 0 -> l | [] -> failwith "drop: list too short" | _::rest -> drop (n-1) rest From 45e116e388be8ce040fd464567bdcdf05327ef9e Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 20 Dec 2024 11:12:43 +1000 Subject: [PATCH 2/5] Stop dead code removal from removing impure operations * Central config for a notion of operation purity * Introduce additional checks for purity in RemoveUnused --- libASL/dis.ml | 64 +-------------------------- libASL/offline_opt.ml | 2 +- libASL/offline_transform.ml | 18 ++------ libASL/symbolic.ml | 87 +++++++++++++++++++++++++++++++++++++ libASL/symbolic_lifter.ml | 9 ++-- libASL/transforms.ml | 46 +++++--------------- 6 files changed, 108 insertions(+), 118 deletions(-) diff --git a/libASL/dis.ml b/libASL/dis.ml index f6351acb..930e32d2 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -67,60 +67,6 @@ let () = Printexc.register_printer Some ("LibASL.Value.EvalError(\"" ^ e ^ "\") at " ^ pp_loc loc) | _ -> None) -(* Don't inline these functions, as we assume their behaviours conform to some spec *) -let no_inline = [ - "FPConvert",0; - "FPRoundInt",0; - "FPRoundIntN",0; - "FPToFixed",0; - "FixedToFP",0; - "FPCompare",0; - "FPCompareEQ",0; - "FPCompareGE",0; - "FPCompareGT",0; - "FPToFixedJS_impl",0; - "FPSqrt",0; - "FPAdd",0; - "FPMul",0; - "FPDiv",0; - "FPMulAdd",0; - "FPMulAddH",0; - "FPMulX",0; - "FPMax",0; - "FPMin",0; - "FPMaxNum",0; - "FPMinNum",0; - "FPSub",0; - "FPRecpX",0; - "FPRecipStepFused",0; - "FPRSqrtStepFused",0; - "FPRoundBase",0; - "FPConvertBF",0; - "BFRound",0; - "BFAdd",0; - "BFMul",0; - "FPRecipEstimate",0; - "Mem.read",0; - "Mem.set",0; - "AtomicStart",0; - "AtomicEnd",0; - "AArch64.MemTag.read",0; - "AArch64.MemTag.set",0; -] - -let no_inline_pure () = [ - "LSL",0; - "LSR",0; - "ASR",0; - "SignExtend",0; - "ZeroExtend",0; -] @ (if !Symbolic.use_vectoriser then [ - "Elem.set",0; - "Elem.read",0; -] else []) - - - (** A variable's stack level and original identifier name. The "stack level" is how many scopes deep it is. For example, globals are level 0 and this increases @@ -942,15 +888,9 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws = | Expr_LitString(s) -> DisEnv.pure (Val (from_stringLit s)) ) -and no_inline_pure_ids () = List.map (fun (x,y) -> FIdent(x,y)) - (no_inline_pure ()) - -and no_inline_ids = List.map (fun (x,y) -> FIdent (x,y)) - no_inline - (** Disassemble call to function *) and dis_funcall (loc: l) (f: ident) (tvs: sym list) (vs: sym list): sym rws = - if List.mem f (no_inline_pure_ids ()) && + if List.mem f (Symbolic.prims_pure ()) && ((List.exists (function Exp _ -> true | _ -> false) tvs) || (List.exists (function Exp _ -> true | _ -> false) vs)) then let expr = Exp (Expr_TApply (f, List.map sym_expr tvs, List.map sym_expr vs)) in @@ -979,7 +919,7 @@ and dis_call (loc: l) (f: ident) (tes: sym list) (es: sym list): sym option rws and dis_call' (loc: l) (f: ident) (tes: sym list) (es: sym list): sym option rws = let@ fn = DisEnv.getFun loc f in (match fn with - | Some (rty, _, targs, _, _, _) when List.mem f no_inline_ids -> + | Some (rty, _, targs, _, _, _) when List.mem f (Symbolic.prims_impure ()) -> (* impure functions are not visited. *) (match sym_prim_simplify (name_of_FIdent f) tes es with | Some x -> DisEnv.pure (Some x) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 477f6f80..bd8c8bdb 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -37,7 +37,7 @@ let is_pure_expr f = match f with | FIdent(f, 0) when String.starts_with ~prefix f -> let f' = String.sub f 4 (String.length f - 4) in - List.mem f' Offline_transform.pure_prims + List.mem (FIdent(f',0)) Offline_transform.pure_prims | _ -> false let is_var_decl f = diff --git a/libASL/offline_transform.ml b/libASL/offline_transform.ml index 046dea21..b92503dd 100644 --- a/libASL/offline_transform.ml +++ b/libASL/offline_transform.ml @@ -172,24 +172,14 @@ let join_state (a: state) (b: state): state = } (* Produce a runtime value if any arg is runtime *) -let pure_prims = - Value.prims_pure @ - (List.map fst (Dis.no_inline_pure ())) @ [ - "lsr_bits"; - "sle_bits"; - "lsl_bits"; - "asr_bits"; - "slt_bits"; - "sdiv_bits"; - ] +let pure_prims = Symbolic.prims_pure () (* Prims that will always produce runtime *) -let impure_prims = - List.map fst Dis.no_inline +let impure_prims = Symbolic.prims_impure () let prim_ops (f: ident) (targs: taint list) (args: taint list): taint option = - if List.mem (name_of_FIdent f) pure_prims then Some (join_taint_l (targs @ args)) - else if List.mem (name_of_FIdent f) impure_prims then Some RunTime + if List.mem f pure_prims then Some (join_taint_l (targs @ args)) + else if List.mem f impure_prims then Some RunTime else None (* Transfer function for a call, pulling a primop def or looking up registered fn signature. diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index 119825ef..f7b6703a 100644 --- a/libASL/symbolic.ml +++ b/libASL/symbolic.ml @@ -920,3 +920,90 @@ let rec expr_access_chain (x: expr) (a: access_chain list): expr = | (Index i)::a -> expr_access_chain (Expr_Array(x,val_expr i)) a | (SymIndex e)::a -> expr_access_chain (Expr_Array(x,e)) a | [] -> x) + +(****************************************************************) +(** {2 Function and Expression Purity} *) +(****************************************************************) + +(** Primitives that can be evaluated, reordered, duplicated and eliminated. + Semantically, should have no influence on the evaluation trace. *) +let prims_pure () = + (List.map (fun f -> FIdent(f,0)) Value.prims_pure) @ + [ + FIdent("LSL",0); + FIdent("LSR",0); + FIdent("ASR",0); + FIdent("SignExtend",0); + FIdent("ZeroExtend",0); + FIdent("asr_bits",0); + FIdent("lsr_bits",0); + FIdent("lsl_bits",0); + FIdent("slt_bits",0); + FIdent("sle_bits",0); + FIdent("sdiv_bits",0); + ] @ (if !use_vectoriser then [ + FIdent("Elem.set",0); + FIdent("Elem.read",0); + ] else []) + +(** Primitives that are placed into the evaluation trace. They must be + preserved in the output, retaining their ordering with respect to each other + and any accesses to global state. *) +let prims_impure () = + (List.map (fun f -> FIdent(f,0)) Value.prims_impure) @ + [ + FIdent("FPConvert",0); + FIdent("FPRoundInt",0); + FIdent("FPRoundIntN",0); + FIdent("FPToFixed",0); + FIdent("FixedToFP",0); + FIdent("FPCompare",0); + FIdent("FPCompareEQ",0); + FIdent("FPCompareGE",0); + FIdent("FPCompareGT",0); + FIdent("FPToFixedJS_impl",0); + FIdent("FPSqrt",0); + FIdent("FPAdd",0); + FIdent("FPMul",0); + FIdent("FPDiv",0); + FIdent("FPMulAdd",0); + FIdent("FPMulAddH",0); + FIdent("FPMulX",0); + FIdent("FPMax",0); + FIdent("FPMin",0); + FIdent("FPMaxNum",0); + FIdent("FPMinNum",0); + FIdent("FPSub",0); + FIdent("FPRecpX",0); + FIdent("FPRecipStepFused",0); + FIdent("FPRSqrtStepFused",0); + FIdent("FPRoundBase",0); + FIdent("FPConvertBF",0); + FIdent("BFRound",0); + FIdent("BFAdd",0); + FIdent("BFMul",0); + FIdent("FPRecipEstimate",0); + FIdent("Mem.read",0); + FIdent("Mem.set",0); + FIdent("AtomicStart",0); + FIdent("AtomicEnd",0); + FIdent("AArch64.MemTag.read",0); + FIdent("AArch64.MemTag.set",0); + ] + +(** Test if an expression is only over constants, variables and pure operations. Does not + determine whether a variable access can be considered pure. *) +let rec is_pure e = + match e with + | Expr_Var _ -> true + | Expr_LitBits _ -> true + | Expr_LitInt _ -> true + | Expr_Slices(e, [Slice_LoWd(lo, wd)]) -> + is_pure e && is_pure lo && is_pure wd + | Expr_TApply(f, tes, es) -> + List.mem f (prims_pure ()) && + List.for_all is_pure tes && + List.for_all is_pure es + | Expr_Field(e,_) -> is_pure e + | Expr_Array(e,i) -> is_pure e && is_pure i + | _ -> false diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 636a946f..86dd03b4 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -152,13 +152,10 @@ let unsupported f = IdentSet.mem f unsupported_set let get_inlining_frontier = (* Collect all functions dis will not inline *) - let l1 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) Dis.no_inline) in - let l2 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) (Dis.no_inline_pure ())) in - (* Collect all prims *) - let l3 = IdentSet.of_list (List.map (fun f -> FIdent (f,0)) Value.prims_pure) in - let l4 = IdentSet.of_list (List.map (fun f -> FIdent (f,0)) Value.prims_impure) in + let l1 = IdentSet.of_list (Symbolic.prims_impure ()) in + let l2 = IdentSet.of_list (Symbolic.prims_pure ()) in (* Union with the unsupported function set *) - IdentSet.union l1 (IdentSet.union l2 (IdentSet.union l3 (IdentSet.union l4 unsupported_set))) + IdentSet.union l1 l2 (* Count individual stmts present after disassembly *) let rec stmt_count s = diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 544b1996..67e5481f 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -7,18 +7,6 @@ open Symbolic open Value (* TODO: Central definition of prims in result + sanity test pass *) -let pure_prims = - (List.map (fun f -> FIdent(f,0)) Value.prims_pure) @ - [ - FIdent("SignExtend",0); - FIdent("ZeroExtend",0); - FIdent("asr_bits",0); - FIdent("lsr_bits",0); - FIdent("lsl_bits",0); - FIdent("slt_bits",0); - FIdent("sle_bits",0); - ] - let infer_type (e: expr): ty option = match e with | Expr_LitBits bv -> (Some(Type_Bits(Expr_LitInt (string_of_int (String.length bv))))) @@ -134,6 +122,10 @@ module RemoveUnused = struct | Expr_TApply (FIdent ("or_bool", 0), [], [a;b]) -> is_true a || is_true b | _ -> false + let pure_fns () = IdentSet.of_list (Symbolic.prims_pure ()) + let contains_impure s = not (IdentSet.subset (calls_of_stmts [s]) (pure_fns ())) + let expr_contains_impure e = not (IdentSet.subset (calls_of_expr e) (pure_fns ())) + let rec remove_unused (globals: IdentSet.t) xs = fst (remove_unused' globals IdentSet.empty xs) and remove_unused' globals (used: IdentSet.t) (xs: stmt list): (stmt list * IdentSet.t) = @@ -151,16 +143,17 @@ module RemoveUnused = struct | [] -> pass | _ -> emit (Stmt_VarDeclsNoInit(ty, vs', loc))) | Stmt_VarDecl(ty, v, i, loc) -> - if IdentSet.mem v used + if IdentSet.mem v used || contains_impure stmt then emit stmt else pass | Stmt_ConstDecl(ty, v, i, loc) -> - if IdentSet.mem v used + if IdentSet.mem v used || contains_impure stmt then emit stmt else pass | Stmt_Assign(le, r, loc) -> let lvs = assigned_vars_of_stmts [stmt] in - if not (IdentSet.disjoint lvs used) || not (IdentSet.disjoint lvs globals) + if not (IdentSet.disjoint lvs used) || not (IdentSet.disjoint lvs globals) || + contains_impure stmt then emit stmt else pass @@ -185,7 +178,7 @@ module RemoveUnused = struct let used = List.fold_right (fun (_,u) -> IdentSet.union u) elsif' (IdentSet.union tused fused) in let used = IdentSet.union used (fv_expr c) in (match (tstmts',fstmts',elsif') with - | [], [], [] -> pass + | [], [], [] when not (expr_contains_impure c) -> pass | _, _, _ -> (Stmt_If(c, tstmts', List.map fst elsif', fstmts', loc)::acc,used)) | Stmt_For(var, start, dir, stop, body, loc) -> @@ -1488,7 +1481,7 @@ module CommonSubExprElim = struct let () = match e with (* For now, only gather TApply's that we've seen more than once See eval_prim in value.ml for the list of what that covers. *) - | Expr_TApply(f,_,_) when List.mem f pure_prims -> + | Expr_TApply(f,_,_) when List.mem f (Symbolic.prims_pure ()) -> (match infer_type e with | Some (Type_Bits _) -> if (List.mem e cand_exprs) && not (List.mem e exprs) then @@ -1708,28 +1701,11 @@ module BitITESimp = struct let one = Expr_LitInt "1" let type_bit = Type_Bits one - (* Test if we can freely perform the operation, even if it wouldn't - have been performed in the original branching version *) - let rec is_pure e = - match e with - | Expr_Var _ -> true - | Expr_LitBits _ -> true - | Expr_LitInt _ -> true - | Expr_Slices(e, [Slice_LoWd(lo, wd)]) -> - is_pure e && is_pure lo && is_pure wd - | Expr_TApply(f, tes, es) -> - List.mem f pure_prims && - List.for_all is_pure tes && - List.for_all is_pure es - | Expr_Field(e,_) -> is_pure e - | Expr_Array(e,i) -> is_pure e && is_pure i - | _ -> false - (* Walk both branches in sync, collect necessary information *) let rec match_body t f = match t, f with | Stmt_Assign(ti,te,loc)::ts, Stmt_Assign(fi,fe,_)::fs - when ti = fi && is_pure te && is_pure fe && + when ti = fi && Symbolic.is_pure te && Symbolic.is_pure fe && infer_type te = Some type_bit -> Option.map (fun rest -> ((ti,te,fe,loc)::rest)) (match_body ts fs) | [], [] -> Some [] From f549e99bc96d792db0d27e63ea64f95668e9ef53 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 20 Dec 2024 11:51:41 +1000 Subject: [PATCH 3/5] Remove sdiv_int Somehow got added to the code base, should just be zdiv_int. --- libASL/dis_tc.ml | 1 - libASL/symbolic.ml | 15 ++++++++------- libASL/transforms.ml | 2 -- libASL/value.ml | 2 +- 4 files changed, 9 insertions(+), 11 deletions(-) diff --git a/libASL/dis_tc.ml b/libASL/dis_tc.ml index 39609f15..a3658ee1 100644 --- a/libASL/dis_tc.ml +++ b/libASL/dis_tc.ml @@ -54,7 +54,6 @@ let prim_type fi targs = | ("mul_int", [ ]) -> Some (Value.type_integer ) | ("zdiv_int", [ ]) -> Some (Value.type_integer ) | ("zrem_int", [ ]) -> Some (Value.type_integer ) - | ("sdiv_int", [ ]) -> Some (Value.type_integer ) | ("fdiv_int", [ ]) -> Some (Value.type_integer ) | ("frem_int", [ ]) -> Some (Value.type_integer ) | ("mod_pow2_int", [ ]) -> Some (Value.type_integer ) diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index f7b6703a..a904fcfb 100644 --- a/libASL/symbolic.ml +++ b/libASL/symbolic.ml @@ -377,6 +377,13 @@ let rec sym_mul_int (loc: l) (x: sym) (y: sym) = sym_add_int loc base offset | _ -> Exp (Expr_TApply (FIdent ("mul_int", 0), [], [sym_expr x; sym_expr y])) +let sym_zdiv_int (loc: l) (x: sym) (y: sym) = + match x, y with + | Val x, Val y -> Val (VInt (prim_zdiv_int (to_integer loc x) (to_integer loc y))) + (* x / 1 = x *) + | _, Val (VInt i) when i = Z.one -> x + | _ -> Exp (Expr_TApply (FIdent ("zdiv_int", 0), [], [sym_expr x; sym_expr y])) + (*** Symbolic Boolean Operations ***) let sym_not_bool loc (x: sym) = @@ -643,12 +650,6 @@ let sym_lsl_bits loc w x y = | _ -> sym_prim (FIdent ("LSL", 0)) [sym_of_int w] [x;y] -let zdiv_int x y = - match x, y with - | Val (VInt i), Val (VInt j) -> Val (VInt (Z.div i j)) - | _, Val (VInt i) when i = Z.one -> x - | _ -> Exp (Expr_TApply (FIdent ("sdiv_int", 0), [], [sym_expr x; sym_expr y])) - (** Overwrite bits from position lo up to (lo+wd) exclusive of old with the value v. Needs to know the widths of both old and v to perform the operation. Assumes width of v is equal to wd. @@ -668,7 +669,7 @@ let sym_insert_bits loc (old_width: int) (old: sym) (lo: sym) (wd: sym) (v: sym) (sym_append_bits loc wd lo v (sym_slice loc old 0 lo)) | (_, _, Val wd', _) when Primops.prim_zrem_int (Z.of_int old_width) (to_integer Unknown wd') = Z.zero && !use_vectoriser -> (* Elem.set *) - let pos = zdiv_int lo wd in + let pos = sym_zdiv_int loc lo wd in Exp ( Expr_TApply (FIdent("Elem.set", 0), [expr_of_int old_width ; sym_expr wd], List.map sym_expr [old ; pos ; wd ; v]) ) | (_, Val (VInt l), _, _) when l = Z.zero && !use_vectoriser -> diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 67e5481f..e4ccfff5 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -3185,8 +3185,6 @@ module LoopClassify = struct | "mul_int", 0, [], [Index (base,mul);Constant offset] | "mul_int", 0, [], [Constant offset;Index (base,mul)] -> Index (mul_int base offset, mul_int mul offset) - | "sdiv_int", 0, [], [Index(base,mul);Constant div] -> - Index (div_int base div, div_int mul div) (* Supported operations over BVIndex TODO: These don't really handle overflow properly *) | "cvt_bits_sint", 0, [Constant w], [BVIndex(b,m,_)] -> diff --git a/libASL/value.ml b/libASL/value.ml index f67e0073..1e7e6232 100644 --- a/libASL/value.ml +++ b/libASL/value.ml @@ -387,7 +387,7 @@ let eval_prim (f: string) (tvs: value list) (vs: value list): value option = let prims_pure = [ "eq_enum"; "eq_enum"; "ne_enum"; "ne_enum"; "eq_bool"; "ne_bool"; "equiv_bool"; "not_bool"; "eq_int"; "ne_int"; "le_int"; "lt_int"; "ge_int"; "gt_int"; "is_pow2_int"; "neg_int"; "add_int"; "sub_int"; "shl_int"; "shr_int"; "mul_int"; "zdiv_int"; - "zrem_int"; "sdiv_int"; "fdiv_int"; "frem_int"; "mod_pow2_int"; "align_int"; "pow2_int"; "pow_int_int"; "cvt_int_real"; "eq_real"; + "zrem_int"; "fdiv_int"; "frem_int"; "mod_pow2_int"; "align_int"; "pow2_int"; "pow_int_int"; "cvt_int_real"; "eq_real"; "ne_real"; "le_real"; "lt_real"; "ge_real"; "gt_real"; "add_real"; "neg_real"; "sub_real"; "mul_real"; "divide_real"; "pow2_real"; "round_tozero_real"; "round_down_real"; "round_up_real"; "sqrt_real"; "cvt_int_bits"; "cvt_bits_sint"; "cvt_bits_uint"; "in_mask"; "notin_mask"; "eq_bits"; "ne_bits"; "add_bits"; "sub_bits"; "mul_bits"; "and_bits"; "or_bits"; From ca497c61c898e06c5d25308941609f74a675f842 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 20 Dec 2024 11:59:24 +1000 Subject: [PATCH 4/5] Limit CSE to pure expressions over constant variables CSE performs some aggressive code motion, as it moves commoned expressions up to the start of the code snippet. To simplify reasoning, limit it to cases for which code motion is trivial. --- libASL/transforms.ml | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/libASL/transforms.ml b/libASL/transforms.ml index e4ccfff5..53871865 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -1465,7 +1465,19 @@ module CommonSubExprElim = struct *) exception CSEError of string - class gather_expressions = object + class gather_consts = object + inherit nopAslVisitor + val mutable consts : IdentSet.t = IdentSet.empty + method! vstmt s = + (match s with + | Stmt_ConstDecl(_, n, _, _) -> + consts <- IdentSet.add n consts; + SkipChildren + | _ -> DoChildren) + method get_info = consts + end + + class gather_expressions consts = object inherit Asl_visitor.nopAslVisitor val mutable exprs: expr list = ([]: expr list); @@ -1481,7 +1493,7 @@ module CommonSubExprElim = struct let () = match e with (* For now, only gather TApply's that we've seen more than once See eval_prim in value.ml for the list of what that covers. *) - | Expr_TApply(f,_,_) when List.mem f (Symbolic.prims_pure ()) -> + | Expr_TApply(f,_,_) when Symbolic.is_pure e && IdentSet.subset (fv_expr e) consts -> (match infer_type e with | Some (Type_Bits _) -> if (List.mem e cand_exprs) && not (List.mem e exprs) then @@ -1585,7 +1597,10 @@ module CommonSubExprElim = struct ) let do_transform (xs: stmt list): stmt list = - let expression_visitor = new gather_expressions in + let const_visitor = new gather_consts in + let _ = visit_stmts const_visitor xs in + + let expression_visitor = new gather_expressions (const_visitor#get_info) in let expression_replacer = new replace_all_instances in let xs = visit_stmts expression_visitor xs in From 89669f35b6e783c94b271fa906ae34166743b3c3 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Tue, 24 Dec 2024 08:54:31 +1000 Subject: [PATCH 5/5] Offline fixes for new reachable code Calls without bodies are left in the partial eval result. This is a little unexpected, leading to offline issues. Also fix some sanity tests to handle failure consistently. --- libASL/scala_backend.ml | 2 +- libASL/symbolic.ml | 4 ++++ libASL/symbolic_lifter.ml | 6 +++--- .../aslp-lifter-llvm/include/aslp/llvm_interface.hpp | 1 + .../subprojects/aslp-lifter/include/aslp/interface.hpp | 1 + offlineASL-scala/lifter/src/interface.scala | 1 + offlineASL-scala/main/src/NoneLifter.scala | 1 + offlineASL/offline_utils.ml | 2 ++ 8 files changed, 14 insertions(+), 4 deletions(-) diff --git a/libASL/scala_backend.ml b/libASL/scala_backend.ml index 981316b2..4aac7eba 100644 --- a/libASL/scala_backend.ml +++ b/libASL/scala_backend.ml @@ -60,7 +60,7 @@ module StringSet = Set.Make(String) "f_gen_lsr_bits"; "f_gen_mul_bits"; "f_gen_ne_bits"; "f_gen_not_bits"; "f_gen_not_bool"; "f_gen_or_bits"; "f_gen_or_bool"; "f_gen_sdiv_bits"; "f_gen_sle_bits"; "f_gen_slt_bits"; "f_gen_sub_bits"; - "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice"; + "f_gen_AArch64_MemTag_read"; "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice"; "f_gen_replicate_bits"; "f_gen_append_bits"; "f_gen_array_load"; "f_gen_array_store"; "f_gen_Mem_set"; "f_gen_assert"; "f_switch_context"; "f_true_branch"; "f_false_branch"; "f_merge_branch"]) diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index a904fcfb..a999a19c 100644 --- a/libASL/symbolic.ml +++ b/libASL/symbolic.ml @@ -990,6 +990,10 @@ let prims_impure () = FIdent("AtomicEnd",0); FIdent("AArch64.MemTag.read",0); FIdent("AArch64.MemTag.set",0); + FIdent("SetTagCheckedInstruction",0); + FIdent("SpeculativeStoreBypassBarrierToPA",0); + FIdent("SpeculationBarrier",0); + FIdent("SpeculativeStoreBypassBarrierToVA",0); ] (** Test if an expression is only over constants, variables and pure operations. Does not diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 86dd03b4..4a37306c 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -135,9 +135,9 @@ module RemoveUnsupported = struct | Stmt_Dep_ImpDef (_, loc) | Stmt_See (_, loc) | Stmt_Throw (_, loc) - | Stmt_DecodeExecute (_, _, loc) -> ChangeTo (assert_false loc) - - | _ -> failwith @@ "Unknown stmt: " ^ (pp_stmt e)) + | Stmt_DecodeExecute (_, _, loc) + | Stmt_Try (_, _, _, _, loc) + | Stmt_Repeat (_, _, loc) -> ChangeTo (assert_false loc)) end let run unsupported env body = diff --git a/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp index 526454b2..13401a78 100644 --- a/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp +++ b/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp @@ -340,6 +340,7 @@ class llvm_run_time_interface : virtual public lifter_interfaceCreateLoad(intty(int_expr(width)), ptr); } void f_gen_AArch64_MemTag_set(rt_expr address, rt_expr acctype, rt_expr value) override { assert(0); } + rt_expr f_gen_AArch64_MemTag_read(rt_expr address, rt_expr acctype) override { assert(0); } void f_AtomicStart() override { assert(0); } void f_AtomicEnd() override { assert(0); } diff --git a/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp index b8593419..e93410c2 100644 --- a/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp +++ b/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp @@ -111,6 +111,7 @@ template class lifter_interface : public Traits { rt_expr acctype) = 0; virtual void f_gen_AArch64_MemTag_set(rt_expr address, rt_expr acctype, rt_expr value) = 0; + virtual rt_expr f_gen_AArch64_MemTag_read(rt_expr address, rt_expr acctype) = 0; virtual void f_AtomicStart() = 0; virtual void f_AtomicEnd() = 0; diff --git a/offlineASL-scala/lifter/src/interface.scala b/offlineASL-scala/lifter/src/interface.scala index 5a363fa2..006cacd2 100644 --- a/offlineASL-scala/lifter/src/interface.scala +++ b/offlineASL-scala/lifter/src/interface.scala @@ -95,6 +95,7 @@ trait LiftState[RTSym, RTLabel, BV <: RTSym] { def f_gen_slt_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym def f_gen_sub_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym def f_gen_AArch64_MemTag_set(arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym + def f_gen_AArch64_MemTag_read(arg0: RTSym, arg1: RTSym): RTSym def f_gen_Mem_read(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym def f_gen_slice(e: RTSym, lo: BigInt, wd: BigInt): RTSym def f_gen_replicate_bits(targ0: BigInt, targ1: BigInt, arg0: RTSym, arg1: BV): RTSym diff --git a/offlineASL-scala/main/src/NoneLifter.scala b/offlineASL-scala/main/src/NoneLifter.scala index 1b2f61af..30b47a15 100644 --- a/offlineASL-scala/main/src/NoneLifter.scala +++ b/offlineASL-scala/main/src/NoneLifter.scala @@ -106,6 +106,7 @@ class NotImplementedLifter extends LiftState[RExpr, String, BitVec] { def f_gen_slt_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_sub_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_AArch64_MemTag_set(arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym = throw NotImplementedError() + def f_gen_AArch64_MemTag_read(arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_Mem_read(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym = throw NotImplementedError() def f_gen_slice(e: RTSym, lo: BigInt, wd: BigInt): RTSym = throw NotImplementedError() def f_gen_replicate_bits(targ0: BigInt, targ1: BigInt, arg0: RTSym, arg1: BV): RTSym = throw NotImplementedError() diff --git a/offlineASL/offline_utils.ml b/offlineASL/offline_utils.ml index 74e84992..0130a5d7 100644 --- a/offlineASL/offline_utils.ml +++ b/offlineASL/offline_utils.ml @@ -191,6 +191,8 @@ let f_AtomicEnd () = push_stmt (Stmt_TCall (FIdent ("AtomicEnd", 0), [], [], Unknown)) let f_gen_AArch64_MemTag_set x y z: unit = failwith "MemTag_set unsupported" +let f_gen_AArch64_MemTag_read x y = + failwith "MemTag_read unsupported" (* Prim bool ops *) let f_gen_and_bool e1 e2 =