diff options
| -rw-r--r-- | lib/arith.sail | 10 | ||||
| -rw-r--r-- | lib/mono_rewrites.sail | 9 | ||||
| -rw-r--r-- | src/monomorphise.ml | 11 |
3 files changed, 25 insertions, 5 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 6b064433..53775166 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -56,19 +56,21 @@ A common idiom in asl is to take two bits of an opcode and convert in into a var let elsize = shl_int(8, UInt(size)) ``` THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` + +Similarly, we define shifts of 32 and 1 (i.e., powers of two). */ val _shl8 = {c: "shl_mach_int", coq: "shl_int_8", _: "shl_int"} : forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)} -/*! -Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` -*/ val _shl32 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} : forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)} +val _shl1 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} : + forall 'n, 0 <= 'n <= 3. (int(1), int('n)) -> {'m, 'm in {1, 2, 4, 8}. int('m)} + val _shl_int = "shl_int" : (int, int) -> int -overload shl_int = {_shl8, _shl32, _shl_int} +overload shl_int = {_shl1, _shl8, _shl32, _shl_int} val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 59359927..0702b374 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -224,4 +224,13 @@ function vector_update_subrange_from_subrange(n,v1,s1,e1,v2,s2,e2) = { xs | ys } +val vector_update_subrange_from_integer_subrange : forall 'n1 's1 'e1 's2 'e2, + 0 <= 'e1 <= 's1 < 'n1 & 0 <= 'e2 <= 's2 & 's1 - 'e1 == 's2 - 'e2. + (implicit('n1), bits('n1), int('s1), int('e1), int, int('s2), int('e2)) -> bits('n1) + +function vector_update_subrange_from_integer_subrange(n1, v1, s1, e1, i, s2, e2) = { + let v2 : bits('n1) = get_slice_int(n1, i, e2) in + vector_update_subrange_from_subrange(n1, v1, s1, e1, v2, s2 - e2, 0) +} + $endif diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 1c6d0fd3..9efacb7a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -232,6 +232,10 @@ and contains_exist_arg (A_aux (arg,_)) = -> false | A_typ typ -> contains_exist typ +let is_number typ = match destruct_numeric typ with + | Some _ -> true + | None -> false + let rec size_nvars_nexp (Nexp_aux (ne,_)) = match ne with | Nexp_var v -> [v] @@ -3171,8 +3175,13 @@ let rewrite_aux = function annot when is_id (env_of_annot annot) (Id "vector_subrange") subrange2 && not (is_constant_range (start1, end1)) -> + let typ2 = Env.base_typ_of (env_of_annot annot) (typ_of vector2) in + let op = + if is_number typ2 then "vector_update_subrange_from_integer_subrange" else + "vector_update_subrange_from_subrange" + in E_aux (E_assign (LEXP_aux (LEXP_id id1,(l_id1,empty_tannot)), - E_aux (E_app (mk_id "vector_update_subrange_from_subrange", [ + E_aux (E_app (mk_id op, [ E_aux (E_id id1,(Generated l_id1,empty_tannot)); start1; end1; vector2; start2; end2]),(Unknown,empty_tannot))), |