diff options
| -rw-r--r-- | lib/mono_rewrites.sail | 2 | ||||
| -rw-r--r-- | src/monomorphise.ml | 7 | ||||
| -rw-r--r-- | test/mono/pass/rewrites | 1 | ||||
| -rw-r--r-- | test/mono/rewrites.sail | 26 |
4 files changed, 34 insertions, 2 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 3efc028a..b24bb152 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -165,7 +165,7 @@ val place_subrange_signed : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), bits('n), int, int, int) -> bits('m) effect pure function place_subrange_signed(m,xs,i,j,shift) = { - place_slice_signed(m, xs, i, i-j+1, shift) + place_slice_signed(m, xs, j, i-j+1, shift) } /* This has different names in the aarch64 prelude (UInt) and the other diff --git a/src/monomorphise.ml b/src/monomorphise.ml index f4d0aa56..9bb47774 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2910,6 +2910,11 @@ let rec rewrite_app env typ (id,args) = is_id env (Id "zero_extend") id || is_id env (Id "sail_zero_extend") id || is_id env (Id "mips_zero_extend") id || is_id env (Id "EXTZ") id in + let is_sign_extend = + is_id env (Id "SignExtend") id || + is_id env (Id "sign_extend") id || is_id env (Id "sail_sign_extend") id || + is_id env (Id "mips_sign_extend") id || is_id env (Id "EXTS") id + in let is_truncate = is_id env (Id "truncate") id in let mk_exp e = E_aux (e, (Unknown, empty_tannot)) in let rec is_zeros_exp e = match unaux_exp e with @@ -3244,7 +3249,7 @@ let rec rewrite_app env typ (id,args) = | _ -> E_app (id,args) - else if is_id env (Id "SignExtend") id || is_id env (Id "sign_extend") id then + else if is_sign_extend then let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in match List.filter (fun arg -> not (is_number (typ_of arg))) args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] diff --git a/test/mono/pass/rewrites b/test/mono/pass/rewrites new file mode 100644 index 00000000..10272fed --- /dev/null +++ b/test/mono/pass/rewrites @@ -0,0 +1 @@ +rewrites.sail -mono_rewrites diff --git a/test/mono/rewrites.sail b/test/mono/rewrites.sail new file mode 100644 index 00000000..b08af90f --- /dev/null +++ b/test/mono/rewrites.sail @@ -0,0 +1,26 @@ +// Tests for -mono_rewrites + +default Order dec +$include <prelude.sail> +$include <mono_rewrites.sail> + +// The preconditions for this rewrite require a non-constant size somewhere, so +// pull the example out into a separate function. +val sign_ext_fun : forall 'z 'n, 'z >= 0 & 'n >= 4 + 'z. (bits(12), int('z), int('n)) -> bits('n) +function sign_ext_fun(y, z, n) = { + sail_sign_extend(y[7..4] @ sail_zeros(z), n) +} + +val run : unit -> unit effect {escape} + +function run() = { + let x : bits(12) = 0x123; + let y : bits(12) = 0x987; + let 'i = 7; + let 'j = 4; + let 'z = 8; + assert(sail_zero_extend(x[7..4] @ sail_zeros(8), 32) == 0x00000200); + assert(sign_ext_fun(x, z, 32) == 0x00000200); + assert(sail_zero_extend(y[7..4] @ sail_zeros(8), 32) == 0x00000800); + assert(sign_ext_fun(y, z, 32) == 0xfffff800); +} |