Coverage fixes for vector ops

libASL/dis.ml

@@ -352,7 +352,11 @@ module DisEnv = struct
         try
             Eval.mk_uninitialized Unknown config.eval_env t
         with
-            e -> unsupported Unknown @@
+            e ->
+              (* Support bit widths we don't know *)
+              match t with
+              | Type_Bits _ -> VUninitialized t
+              | _ -> unsupported Unknown @@
                 "mkUninit: failed to evaluate type " ^ pp_type t ^ " due to " ^
                 Printexc.to_string e
 

libASL/symbolic.ml

@@ -620,7 +620,12 @@ let sym_insert_bits loc (old_width: int) (old: sym) (lo: sym) (wd: sym) (v: sym)
   | (_, _, Val wd', _) when Primops.prim_zrem_int (Z.of_int old_width) (to_integer Unknown wd') = Z.zero ->
       (* Elem.set *)
       let pos = zdiv_int 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]) )
+      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 ->
+      Exp (Expr_TApply (FIdent ("Elem.set", 0), [expr_of_int old_width ; sym_expr wd],
+          List.map sym_expr [old ; lo ; wd ; v]))
+
   | (_, _, Val wd', _) ->
       (* Build an insert out of bitvector masking operations *)
       let wd = to_int loc wd' in

libASL/transforms.ml

@@ -503,9 +503,9 @@ module StatefulIntToBits = struct
       let e' = match e with
       (* Slice may take bitvector or integer as first argument, allow for failure in bv case *)
       (* TODO: Would prefer to type check x, rather than allowing for failure *)
-      | Expr_Slices(x, [Slice_LoWd(Expr_LitInt l,w)]) ->
+      | Expr_Slices(x, [Slice_LoWd(Expr_LitInt l,Expr_LitInt w)]) ->
           let l = int_of_expr (Expr_LitInt l) in
-          let w = int_of_expr w in
+          let w = int_of_expr (Expr_LitInt w) in
           (match bv_of_int_expr_opt st x with
           | Some (e,a) ->
               if width a = l + w && l = 0 then sym_expr e else
@@ -669,7 +669,9 @@ module StatefulIntToBits = struct
     else match ty with
     | Type_Constructor i ->
         (match enum_types i with
-        | Some w -> Some (Some w)
+        | Some w ->
+            let w = next_pow_of_2 w in
+            Some (Some w)
         | None -> None)
     | _ -> None
 
@@ -2477,16 +2479,21 @@ module LoopClassify = struct
         Expr_TApply(FIdent("slt_vec", 0),  [iters; w], vec_args [x; y])
     | "eq_bits", 0, [w], [x;y] ->
         Expr_TApply(FIdent("eq_vec", 0),   [iters; w], vec_args [x; y])
+
     | "asr_bits", 0, [w;w'], [x;y] when w = w' ->
         Expr_TApply(FIdent("asr_vec", 0),  [iters; w], vec_args [x;y])
-    | "asr_bits", 0, [w;w'], [x;y] ->
+    | "asr_bits", 0, [Expr_LitInt w;Expr_LitInt w'], [x;y] when Z.gt (Z.of_string w) (Z.of_string w') ->
+        let w = Expr_LitInt w and w' = Expr_LitInt w' in
         let y = Expr_TApply(FIdent("scast_vec", 0), [iters; w; w'], (vec_args [y]) @ [w]) in
         Expr_TApply(FIdent("asr_vec", 0),  [iters; w], [build_vec_expr st x;y;iters])
+
     | "lsl_bits", 0, [w;w'], [x;y] when w = w' ->
         Expr_TApply(FIdent("lsl_vec", 0),  [iters; w], vec_args [x;y])
-    | "lsl_bits", 0, [w;w'], [x;y] ->
+    | "lsl_bits", 0, [Expr_LitInt w;Expr_LitInt w'], [x;y] when Z.gt (Z.of_string w) (Z.of_string w') ->
+        let w = Expr_LitInt w and w' = Expr_LitInt w' in
         let y = Expr_TApply(FIdent("scast_vec", 0), [iters; w; w'], (vec_args [y]) @ [w]) in
         Expr_TApply(FIdent("lsl_vec", 0),  [iters; w], [build_vec_expr st x;y;iters])
+
     | "ite", 0, [w], [c;x;y] ->
         Expr_TApply(FIdent("ite_vec", 0), [iters; w], vec_args [c;x;y])
 

tests/override.asl

@@ -39,7 +39,9 @@ bits(N) sdiv_bits(bits(N) x, bits(N) y)
 
 bits(N1) lsl_bits(bits(N1) x, bits(N2) y)
     integer yn = SInt(y);
-    return LSL(x, yn);
+    // LSL will assert if yn is negative, but we assume this
+    // operation is pure. Wrap it to be identity in this case.
+    return if yn < 0 then x else LSL(x, yn);
 
 bits(N1) lsr_bits(bits(N1) x, bits(N2) y)
     integer yn = SInt(y);
@@ -325,6 +327,8 @@ integer LowestSetBit(bits(N) x)
     else
         return N;
 
+bits(W) ite(boolean c, bits(W) x, bits(W) y)
+  return if c then x else y;
 
 // Vector Operations
 
@@ -346,6 +350,12 @@ bits(W * N) mul_vec(bits(W * N) x, bits(W * N) y, integer N)
     Elem[result, i, W] = Elem[x, i, W] * Elem[y, i, W];
   return result;
 
+bits(W * N) sdiv_vec(bits(W * N) x, bits(W * N) y, integer N)
+  bits(W * N) result;
+  for i = 0 to (N - 1)
+    Elem[result, i, W] = sdiv_bits(Elem[x, i, W], Elem[y, i, W]);
+  return result;
+
 bits(W * N) lsr_vec(bits(W * N) x, bits(W * N) y, integer N)
   bits(W * N) result;
   for i = 0 to (N - 1)