Init vector state in coverage tester

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;
 

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

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))

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. *)

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}                                            *)

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";

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);

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

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'

offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp

@@ -489,6 +489,8 @@ class llvm_run_time_interface : virtual public lifter_interface<llvm_lifter_trai
   rt_expr f_gen_FPRecpX(rt_expr x, rt_expr fpcr) override { assert(0); }
   rt_expr f_gen_FPSqrt(rt_expr x, rt_expr fpcr) override { assert(0); }
   rt_expr f_gen_FPRecipEstimate(rt_expr x, rt_expr fpcr) override { assert(0); }
+  rt_expr f_gen_UnsignedRSqrtEstimate(rt_expr x) override { assert(0); }
+  rt_expr f_gen_FPRSqrtEstimate(rt_expr x, rt_expr fpcr) override { assert(0); }
   rt_expr f_gen_BFAdd(rt_expr x, rt_expr y) override { assert(0); }
   rt_expr f_gen_BFMul(rt_expr x, rt_expr y) override { assert(0); }
   rt_expr f_gen_FPConvertBF(rt_expr x, rt_expr fpcr, rt_expr rounding) override { assert(0); }

offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp

@@ -168,6 +168,8 @@ template <typename Traits> 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,

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

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()

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])

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;