diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 3 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 3 | ||||
| -rw-r--r-- | src/monomorphise.ml | 17 |
3 files changed, 21 insertions, 2 deletions
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index 132ea84f..b0a29b5e 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -32,6 +32,9 @@ let exts_vec = exts_bv val zero_extend : list bitU -> integer -> list bitU let zero_extend bits len = extz_bits len bits +val sign_extend : list bitU -> integer -> list bitU +let sign_extend bits len = exts_bits len bits + val vector_truncate : list bitU -> integer -> list bitU let vector_truncate bs len = extz_bv len bs diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 55e6ff51..8bcc0319 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -73,6 +73,9 @@ let exts_vec _ w = Machine_word.signExtend w val zero_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b let zero_extend w _ = Machine_word.zeroExtend w +val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let sign_extend w _ = Machine_word.signExtend w + val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b let vector_truncate w _ = Machine_word.zeroExtend w diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8448fc4e..75b82da2 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3666,7 +3666,7 @@ let rewrite_app env typ (id,args) = [vector1; start1; end1]) | _ -> E_app (id,args) - else if is_id env (Id "Extend") id || is_id env (Id "ZeroExtend") id then + else if is_id env (Id "Extend") id || is_id env (Id "ZeroExtend") id || is_id env (Id "zero_extend") id then let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in let is_zeros = is_id env (Id "Zeros") in @@ -3703,13 +3703,26 @@ let rewrite_app env typ (id,args) = | _ -> E_app (id,args) - else if is_id env (Id "SignExtend") id then + else if is_id env (Id "SignExtend") id || is_id env (Id "sign_extend") id then let is_slice = is_id env (Id "slice") in match args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] when is_slice slice1 && not (is_constant length1) -> E_app (mk_id "sext_slice", [vector1; start1; length1]) + (* If the original had a length, keep it *) + | [E_aux (E_app (slice1, [vector1; start1; length1]),_);length2] + when is_slice slice1 && not (is_constant length1) -> + begin + match Type_check.destruct_atom_nexp (env_of length2) (typ_of length2) with + | None -> E_app (mk_id "sext_slice", [vector1; start1; length1]) + | Some nlen -> + let (_,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + E_cast (vector_typ nlen order bittyp, + E_aux (E_app (mk_id "sext_slice", [vector1; start1; length1]), + (Unknown,None))) + end + | _ -> E_app (id,args) else if is_id env (Id "UInt") id || is_id env (Id "unsigned") id then |