From da423483fdd6cf56f5f8d08a03e4ac3fd4673307 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 17 Jan 2025 11:34:20 +1000 Subject: [PATCH 1/3] Init vectors in coverage, fix resulting errors --- bin/asli.ml | 6 ++---- bin/offline_coverage.ml | 3 +-- libASL/eval.ml | 24 +++++++++++++++++++++--- libASL/primops.ml | 14 +++++++++++++- libASL/symbolic.ml | 2 ++ libASL/testing.ml | 3 +-- libASL/value.ml | 7 ++++++- tests/test_asl.ml | 3 +-- 8 files changed, 47 insertions(+), 15 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index c0e9d5af..f36f16cd 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -74,8 +74,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 | [":init"; "globals"] -> Eval.initializeGlobals cpu.env; | [":init"; "regs"] -> - let vals = (List.init 64 (fun _ -> Z.of_int64 (Random.int64 Int64.max_int))) in - Eval.initializeRegistersAndMemory cpu.env vals; + Eval.randomRegistersAndMemory cpu.env | ":enumerate" :: iset :: tail -> let (start,stop,fname) = (match tail with | [start;stop;fname] -> (int_of_string start, int_of_string stop, fname) @@ -110,8 +109,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 (* Set up our environments *) let initEnv = Eval.Env.copy cpu.env in (* Obtain and set random initial values for _R registers. *) - let vals = (List.init 64 (fun _ -> Z.of_int64 (Random.int64 Int64.max_int))) in - Eval.initializeRegistersAndMemory initEnv vals; + Eval.randomRegistersAndMemory initEnv; (* Replace remaining VUninitialized with default zero values. *) Eval.initializeGlobals initEnv; diff --git a/bin/offline_coverage.ml b/bin/offline_coverage.ml index 595b8e7a..a69e581d 100644 --- a/bin/offline_coverage.ml +++ b/bin/offline_coverage.ml @@ -22,8 +22,7 @@ let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult = let initenv = Env.copy env in Random.self_init (); - let vals = (List.init 64 (fun _ -> Z.of_int64 (Random.int64 Int64.max_int))) in - Eval.initializeRegistersAndMemory initenv vals; + Eval.randomRegistersAndMemory initenv; Eval.initializeGlobals initenv; let initenv = Env.freeze initenv in diff --git a/libASL/eval.ml b/libASL/eval.ml index ffca6e57..fbc4e201 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -493,19 +493,37 @@ let initializeGlobals (env: Env.t): unit = let g = Env.getGlobals env in g.bs <- Bindings.map (eval_uninitialized_to_defaults env) g.bs -let initializeRegistersAndMemory (env: Env.t) (xs: bigint list): unit = +let initializeRegistersAndMemory (env: Env.t) (regs: bitvector list) (vecs: bitvector list): unit = let d = VBits {n=64; v=Z.zero} in - let vals = List.mapi (fun i v -> (i, VBits {n=64; v})) xs in + + let vals = List.mapi (fun i v -> (i, VBits v)) regs in let arr = List.fold_left (fun a (k,v) -> ImmutableArray.add k v a) ImmutableArray.empty vals in Env.setVar Unknown env (Ident "_R") (VArray (arr, d)); + + let vals = List.mapi (fun i v -> (i, VBits v)) vecs in + let arr = List.fold_left + (fun a (k,v) -> ImmutableArray.add k v a) + ImmutableArray.empty + vals + in + Env.setVar Unknown env (Ident "_Z") (VArray (arr, d)); + + (* Init memory *) let ram = Primops.init_ram (char_of_int 0) in ram.default <- None; Env.setVar Unknown env (Ident "__Memory") (VRAM ram) +let randomRegistersAndMemory (env: Env.t): unit = + let rnd n = Primops.({ n ; v = Z.random_bits n }) in + (* Init register array, should be 31 elements, each 64 bits wide *) + let regs = List.init 31 (fun i -> (rnd 64)) in + (* Init vector array, should be 32 elements, each 128 bits wide *) + let vecs = List.init 32 (fun i -> (rnd 128)) in + initializeRegistersAndMemory env regs vecs let isGlobalConst (env: Env.t) (id: AST.ident): bool = match Env.getGlobalConst env id with @@ -811,7 +829,7 @@ and eval_lexpr (loc: l) (env: Env.t) (x: AST.lexpr) (r: value): unit = | (s :: ss) -> let (i, w) = eval_slice loc env s in let v = extract_bits'' loc r o w in - eval (eval_add_int loc o w) ss (insert_bits loc prev i w v) + eval (eval_add_int loc o w) ss (insert_bits'' loc prev i w v) ) in eval_lexpr_modify loc env l (eval (VInt Z.zero) (List.rev ss)) diff --git a/libASL/primops.ml b/libASL/primops.ml index 890f8aa3..17b052ba 100644 --- a/libASL/primops.ml +++ b/libASL/primops.ml @@ -104,7 +104,9 @@ let prim_round_up_real (x: real): bigint = Z.add Z.one (Q.to_bigint x) end -let prim_sqrt_real (x: real): real = failwith "prim_sqrt_real" +(* Can't necessarily represent this as a rational. *) +let prim_sqrt_real (x: real): real = + Q.make (Z.sqrt (Q.num x)) (Z.sqrt (Q.den x)) (****************************************************************) @@ -213,6 +215,16 @@ let prim_insert (x: bitvector) (i: bigint) (w: bigint) (y: bitvector): bitvector let y' = Z.shift_left (z_extract y.v 0 w') i' in mkBits x.n (Z.logor (Z.logand nmsk x.v) (Z.logand msk y')) +let prim_insert_int (x: Z.t) (i: bigint) (w: bigint) (y: bitvector): Z.t = + let i' = Z.to_int i in + let w' = Z.to_int w in + assert (0 <= i'); + assert (0 <= w'); + assert (w' = y.n); + let msk = (Z.sub (Z.shift_left Z.one (i'+w')) (Z.shift_left Z.one i')) in + let nmsk = Z.lognot msk in + let y' = Z.shift_left (z_extract y.v 0 w') i' in + (Z.logor (Z.logand nmsk x) (Z.logand msk y')) (****************************************************************) (** {2 Mask primops} *) diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index a999a19c..a994c951 100644 --- a/libASL/symbolic.ml +++ b/libASL/symbolic.ml @@ -984,6 +984,8 @@ let prims_impure () = FIdent("BFAdd",0); FIdent("BFMul",0); FIdent("FPRecipEstimate",0); + FIdent("UnsignedRSqrtEstimate",0); + FIdent("FPRSqrtEstimate",0); FIdent("Mem.read",0); FIdent("Mem.set",0); FIdent("AtomicStart",0); diff --git a/libASL/testing.ml b/libASL/testing.ml index 7843a37b..53b69420 100644 --- a/libASL/testing.ml +++ b/libASL/testing.ml @@ -404,8 +404,7 @@ let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult = let initenv = Env.copy env in Random.self_init (); - let vals = (List.init 64 (fun _ -> Z.of_int64 (Random.int64 Int64.max_int))) in - Eval.initializeRegistersAndMemory initenv vals; + Eval.randomRegistersAndMemory initenv; Eval.initializeGlobals initenv; let initenv = Env.freeze initenv in diff --git a/libASL/value.ml b/libASL/value.ml index 1e7e6232..8fd89fa1 100644 --- a/libASL/value.ml +++ b/libASL/value.ml @@ -307,7 +307,7 @@ let eval_prim (f: string) (tvs: value list) (vs: value list): value option = | ("round_tozero_real", [ ], [VReal x ]) -> Some (VInt (prim_round_tozero_real x)) | ("round_down_real", [ ], [VReal x ]) -> Some (VInt (prim_round_down_real x)) | ("round_up_real", [ ], [VReal x ]) -> Some (VInt (prim_round_up_real x)) - | ("sqrt_real", [ ], [VReal x; VReal y ]) -> Some (VReal (prim_sqrt_real x)) + | ("sqrt_real", [ ], [VReal x ]) -> Some (VReal (prim_sqrt_real x)) | ("cvt_int_bits", [_ ], [VInt x; VInt n ]) -> Some (VBits (prim_cvt_int_bits n x)) | ("cvt_bits_sint", [VInt n], [VBits x ]) -> Some (VInt (prim_cvt_bits_sint x)) | ("cvt_bits_uint", [VInt n], [VBits x ]) -> Some (VInt (prim_cvt_bits_uint x)) @@ -425,6 +425,11 @@ let insert_bits (loc: AST.l) (x: value) (i: value) (w: value) (y: value): value let insert_bits' (loc: AST.l) (x: value) (i: int) (w: int) (y: value): value = VBits (prim_insert (to_bits loc x) (Z.of_int i) (Z.of_int w) (to_bits loc y)) +let insert_bits'' (loc: AST.l) (x: value) (i: value) (w: value) (y: value): value = + (match x with + | VInt(x') -> VInt (prim_insert_int x' (to_integer loc i) (to_integer loc w) (to_bits loc y)) + | _ -> insert_bits loc x i w y) + let rec eval_eq (loc: AST.l) (x: value) (y: value): bool = (match (x, y) with | (VBool x', VBool y') -> prim_eq_bool x' y' diff --git a/tests/test_asl.ml b/tests/test_asl.ml index d6449f6a..1c1fdbbb 100644 --- a/tests/test_asl.ml +++ b/tests/test_asl.ml @@ -61,8 +61,7 @@ let test_compare env () : unit = let initEnv = Eval.Env.copy env in (* Obtain and set random initial values for _R registers. *) Random.self_init (); - let vals = (List.init 64 (fun _ -> Z.of_int64 (Random.int64 Int64.max_int))) in - Eval.initializeRegistersAndMemory initEnv vals; + Eval.randomRegistersAndMemory initEnv; (* Replace remaining VUninitialized with default zero values. *) Eval.initializeGlobals initEnv; From c6c51f0322592bacb711b061f31a185e5d20ea04 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 17 Jan 2025 12:29:39 +1000 Subject: [PATCH 2/3] Extend offline for new prims --- .../aslp-lifter-llvm/include/aslp/llvm_interface.hpp | 2 ++ .../subprojects/aslp-lifter/include/aslp/interface.hpp | 2 ++ offlineASL-scala/lifter/src/interface.scala | 2 ++ offlineASL-scala/main/src/NoneLifter.scala | 2 ++ offlineASL/offline_utils.ml | 4 ++++ 5 files changed, 12 insertions(+) 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 13401a78..03358cb7 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 @@ -489,6 +489,8 @@ class llvm_run_time_interface : virtual public lifter_interface class lifter_interface : public Traits { virtual rt_expr f_gen_FPRecpX(rt_expr x, rt_expr fpcr) = 0; virtual rt_expr f_gen_FPSqrt(rt_expr x, rt_expr fpcr) = 0; virtual rt_expr f_gen_FPRecipEstimate(rt_expr x, rt_expr fpcr) = 0; + virtual rt_expr f_gen_UnsignedRSqrtEstimate(rt_expr x) = 0; + virtual rt_expr f_gen_FPRSqrtEstimate(rt_expr x, rt_expr fpcr) = 0; virtual rt_expr f_gen_BFAdd(rt_expr x, rt_expr y) = 0; virtual rt_expr f_gen_BFMul(rt_expr x, rt_expr y) = 0; virtual rt_expr f_gen_FPConvertBF(rt_expr x, rt_expr fpcr, diff --git a/offlineASL-scala/lifter/src/interface.scala b/offlineASL-scala/lifter/src/interface.scala index 006cacd2..077a36f6 100644 --- a/offlineASL-scala/lifter/src/interface.scala +++ b/offlineASL-scala/lifter/src/interface.scala @@ -55,6 +55,8 @@ trait LiftState[RTSym, RTLabel, BV <: RTSym] { def f_gen_FPMulX(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym def f_gen_FPRSqrtStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym def f_gen_FPRecipEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym + def f_gen_UnsignedRSqrtEstimate(targ0: BigInt, arg0: RTSym): RTSym + def f_gen_FPRSqrtEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym def f_gen_FPRecipStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym def f_gen_FPRecpX(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym def f_gen_FPRoundInt(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym, arg3: RTSym): RTSym diff --git a/offlineASL-scala/main/src/NoneLifter.scala b/offlineASL-scala/main/src/NoneLifter.scala index 30b47a15..e82d471d 100644 --- a/offlineASL-scala/main/src/NoneLifter.scala +++ b/offlineASL-scala/main/src/NoneLifter.scala @@ -66,6 +66,8 @@ class NotImplementedLifter extends LiftState[RExpr, String, BitVec] { def f_gen_FPMulX(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym = throw NotImplementedError() def f_gen_FPRSqrtStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_FPRecipEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() + def f_gen_UnsignedRSqrtEstimate(targ0: BigInt, arg0: RTSym): RTSym = throw NotImplementedError() + def f_gen_FPRSqrtEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_FPRecipStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_FPRecpX(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError() def f_gen_FPRoundInt(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym, arg3: RTSym): RTSym = throw NotImplementedError() diff --git a/offlineASL/offline_utils.ml b/offlineASL/offline_utils.ml index 0130a5d7..d0755924 100644 --- a/offlineASL/offline_utils.ml +++ b/offlineASL/offline_utils.ml @@ -290,6 +290,10 @@ let f_gen_FPSqrt w x t = Expr_TApply (FIdent ("FPSqrt", 0), [expr_of_z w], [x; t]) let f_gen_FPRecipEstimate w x r = Expr_TApply (FIdent ("FPRecipEstimate", 0), [expr_of_z w], [x; r]) +let f_gen_UnsignedRSqrtEstimate w x = + Expr_TApply (FIdent ("UnsignedRSqrtEstimate", 0), [expr_of_z w], [x]) +let f_gen_FPRSqrtEstimate w x r = + Expr_TApply (FIdent ("FPRSqrtEstimate", 0), [expr_of_z w], [x; r]) let f_gen_BFAdd x y = Expr_TApply (FIdent ("BFAdd", 0), [], [x; y]) From 14b24fe46f1d09cb9e6894c5767cde9745bfb1a3 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 17 Jan 2025 14:39:01 +1000 Subject: [PATCH 3/3] Add prims to scala backend, fix impure issue with rt copyprop --- libASL/offline_opt.ml | 8 +++++--- libASL/scala_backend.ml | 1 + 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index bd8c8bdb..6682e243 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -522,9 +522,13 @@ module RtCopyProp = struct | Some (Defined ids) -> (st, IdentSet.union i ids) | _ -> (st, i) + let impure_ident = Ident "CopyProp_impure" + let write_var v (st,i) = - 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 = if has_context st then (set_var v Essential st) else st in + (* cannot copy-prop impure exprs *) + let st = if IdentSet.mem impure_ident i then (set_var v Essential st) else st in let st = clobber_var v st in let (st,i) = match get_var v st with | Some (Declared) -> (set_var v (Defined i) st, i) @@ -535,8 +539,6 @@ module RtCopyProp = struct in (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. *) diff --git a/libASL/scala_backend.ml b/libASL/scala_backend.ml index 4aac7eba..06b69819 100644 --- a/libASL/scala_backend.ml +++ b/libASL/scala_backend.ml @@ -52,6 +52,7 @@ module StringSet = Set.Make(String) "f_gen_FPRecipEstimate"; "f_gen_FPRecipStepFused"; "f_gen_FPRecpX"; "f_gen_FPRoundInt"; "f_gen_FPRoundIntN"; "f_gen_FPSqrt"; "f_gen_FPSub"; "f_gen_FPToFixed"; "f_gen_FPToFixedJS_impl"; "f_gen_FixedToFP"; + "f_gen_FPRSqrtEstimate"; "f_gen_UnsignedRSqrtEstimate"; "f_gen_bit_lit"; "f_gen_bool_lit"; "f_gen_branch"; "f_cvt_bits_uint"; "f_gen_cvt_bits_uint"; "f_gen_cvt_bool_bv"; "f_gen_eor_bits"; "f_gen_eq_bits"; "f_gen_eq_enum"; "f_gen_int_lit"; "f_gen_store";