From 39e4fb34313b2c7cec6abe036367591e3db938bd Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Tue, 9 Jul 2024 17:35:40 +1000 Subject: [PATCH] Coverage fixes for vector ops --- libASL/dis.ml | 6 +++++- libASL/symbolic.ml | 7 ++++++- libASL/transforms.ml | 17 ++++++++++++----- tests/override.asl | 12 +++++++++++- 4 files changed, 34 insertions(+), 8 deletions(-) diff --git a/libASL/dis.ml b/libASL/dis.ml index ca6de1d9..92c5bda6 100644 --- a/libASL/dis.ml +++ b/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 diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index b9f7d79b..e576b998 100644 --- a/libASL/symbolic.ml +++ b/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 diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 1777af46..ebb7c507 100644 --- a/libASL/transforms.ml +++ b/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]) diff --git a/tests/override.asl b/tests/override.asl index 5662de53..21205aad 100644 --- a/tests/override.asl +++ b/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)