Init vectors in coverage, fix resulting errors

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/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/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'

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;