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/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/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/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 119825ef..a999a19c 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 -> @@ -920,3 +921,94 @@ 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); + 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 + 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..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 = @@ -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..53871865 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) -> @@ -1472,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); @@ -1488,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 pure_prims -> + | 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 @@ -1592,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 @@ -1708,28 +1716,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 [] @@ -3209,8 +3200,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/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 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"; 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 =