summaryrefslogtreecommitdiff
path: root/src/monomorphise.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/monomorphise.ml')
-rw-r--r--src/monomorphise.ml164
1 files changed, 119 insertions, 45 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index adc4d6d2..ab6d9e2d 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3167,13 +3167,15 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
| None -> r
| Some (tenv,typ,_) ->
let typ = Env.base_typ_of tenv typ in
- let env, typ =
+ let env, tenv, typ =
match destruct_exist tenv typ with
- | None -> env, typ
+ | None -> env, tenv, typ
| Some (kids, nc, typ) ->
{ env with kid_deps =
List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids },
- typ
+ Env.add_constraint nc
+ (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids),
+ typ
in
if is_bitvector_typ typ then
let size,_,_ = vector_typ_args_of typ in
@@ -3644,6 +3646,14 @@ let is_constant_vec_typ env typ =
let rewrite_app env typ (id,args) =
let is_append = is_id env (Id "append") in
+ let try_cast_to_typ (E_aux (e,_) as exp) =
+ let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
+ match size with
+ | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp)
+ | _ -> match solve env size with
+ | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp)
+ | None -> e
+ in
if is_append id then
let is_subrange = is_id env (Id "vector_subrange") in
let is_slice = is_id env (Id "slice") in
@@ -3661,14 +3671,23 @@ let rewrite_app env typ (id,args) =
not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
- let midsize = nminus size size1 in
- let midtyp = vector_typ midsize order bittyp in
- E_app (append,
- [e1;
- E_aux (E_cast (midtyp,
- E_aux (E_app (mk_id "subrange_subrange_concat",
- [vector1; start1; end1; vector2; start2; end2]),
- (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+ let midsize = nminus size size1 in begin
+ match solve env midsize with
+ | Some c ->
+ let midtyp = vector_typ (nconstant c) order bittyp in
+ E_app (append,
+ [e1;
+ E_aux (E_cast (midtyp,
+ E_aux (E_app (mk_id "subrange_subrange_concat",
+ [vector1; start1; end1; vector2; start2; end2]),
+ (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+ | _ ->
+ E_app (append,
+ [e1;
+ E_aux (E_app (mk_id "subrange_subrange_concat",
+ [vector1; start1; end1; vector2; start2; end2]),
+ (Unknown,empty_tannot))])
+ end
| [E_aux (E_app (append,
[e1;
E_aux (E_app (slice1,
@@ -3680,14 +3699,23 @@ let rewrite_app env typ (id,args) =
not (is_constant length1 || is_constant length2) ->
let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
- let midsize = nminus size size1 in
- let midtyp = vector_typ midsize order bittyp in
- E_app (append,
- [e1;
- E_aux (E_cast (midtyp,
- E_aux (E_app (mk_id "slice_slice_concat",
- [vector1; start1; length1; vector2; start2; length2]),
- (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+ let midsize = nminus size size1 in begin
+ match solve env midsize with
+ | Some c ->
+ let midtyp = vector_typ (nconstant c) order bittyp in
+ E_app (append,
+ [e1;
+ E_aux (E_cast (midtyp,
+ E_aux (E_app (mk_id "slice_slice_concat",
+ [vector1; start1; length1; vector2; start2; length2]),
+ (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+ | _ ->
+ E_app (append,
+ [e1;
+ E_aux (E_app (mk_id "slice_slice_concat",
+ [vector1; start1; length1; vector2; start2; length2]),
+ (Unknown,empty_tannot))])
+ end
(* variable-range @ variable-range *)
| [E_aux (E_app (subrange1,
@@ -3696,10 +3724,10 @@ let rewrite_app env typ (id,args) =
[vector2; start2; end2]),_)]
when is_subrange subrange1 && is_subrange subrange2 &&
not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
- E_cast (typ,
- E_aux (E_app (mk_id "subrange_subrange_concat",
- [vector1; start1; end1; vector2; start2; end2]),
- (Unknown,empty_tannot)))
+ try_cast_to_typ
+ (E_aux (E_app (mk_id "subrange_subrange_concat",
+ [vector1; start1; end1; vector2; start2; end2]),
+ (Unknown,empty_tannot)))
(* variable-slice @ variable-slice *)
| [E_aux (E_app (slice1,
@@ -3708,9 +3736,9 @@ let rewrite_app env typ (id,args) =
[vector2; start2; length2]),_)]
when is_slice slice1 && is_slice slice2 &&
not (is_constant length1 || is_constant length2) ->
- E_cast (typ,
- E_aux (E_app (mk_id "slice_slice_concat",
- [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
+ try_cast_to_typ
+ (E_aux (E_app (mk_id "slice_slice_concat",
+ [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
| [E_aux (E_app (append1,
[e1;
@@ -3721,16 +3749,25 @@ let rewrite_app env typ (id,args) =
not (is_constant length1 || is_constant length2) ->
let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
- let midsize = nminus size size1 in
- let midtyp = vector_typ midsize order bittyp in
- E_cast (typ,
- E_aux (E_app (mk_id "append",
+ let midsize = nminus size size1 in begin
+ match solve env midsize with
+ | Some c ->
+ let midtyp = vector_typ (nconstant c) order bittyp in
+ try_cast_to_typ
+ (E_aux (E_app (mk_id "append",
[e1;
E_aux (E_cast (midtyp,
E_aux (E_app (mk_id "slice_zeros_concat",
[vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]),
(Unknown,empty_tannot)))
-
+ | _ ->
+ try_cast_to_typ
+ (E_aux (E_app (mk_id "append",
+ [e1;
+ E_aux (E_app (mk_id "slice_zeros_concat",
+ [vector1; start1; length1; length2]),(Unknown,empty_tannot))]),
+ (Unknown,empty_tannot)))
+ end
| _ -> E_app (id,args)
else if is_id env (Id "eq_vec") id then
@@ -3875,7 +3912,7 @@ let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) =
(* These functions add cast functions across case splits, so that when a
bitvector size becomes known in sail, the generated Lem code contains a
function call to change mword 'n to (say) mword ty16, and vice versa. *)
-let make_bitvector_cast_fns env quant_kids src_typ target_typ =
+let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ =
let genunk = Generated Unknown in
let fresh =
let counter = ref 0 in
@@ -3908,7 +3945,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
P_aux (P_id var,(Generated src_l,src_ann)),
E_aux
(E_cast (tar_typ',
- E_aux (E_app (Id_aux (Id "bitvector_cast", genunk),
+ E_aux (E_app (Id_aux (Id cast_name, genunk),
[E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))),
(genunk, tar_ann))
| _ ->
@@ -3934,12 +3971,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
(fun var exp ->
let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in
E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)),
- E_aux (E_app (Id_aux (Id "bitvector_cast",genunk),
+ E_aux (E_app (Id_aux (Id cast_name,genunk),
[E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)),
exp),(genunk,exp_ann))),
(fun (E_aux (_,(exp_l,exp_ann)) as exp) ->
E_aux (E_cast (one_target_typ,
- E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [exp]), (Generated exp_l,tar_ann))),
+ E_aux (E_app (Id_aux (Id cast_name, genunk), [exp]), (Generated exp_l,tar_ann))),
(Generated exp_l,tar_ann)))
| _ ->
(fun var exp ->
@@ -3954,12 +3991,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
(* TODO: bound vars *)
let make_bitvector_env_casts env quant_kids (kid,i) exp =
- let mk_cast var typ exp = (fst (make_bitvector_cast_fns env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
+ let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
let locals = Env.get_locals env in
Bindings.fold (fun var (mut,typ) exp ->
if mut = Immutable then mk_cast var typ exp else exp) locals exp
-let make_bitvector_cast_exp env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns env quant_kids typ target_typ)) exp
+let make_bitvector_cast_exp cast_name env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns cast_name env quant_kids typ target_typ)) exp
let rec extract_value_from_guard var (E_aux (e,_)) =
match e with
@@ -3986,6 +4023,12 @@ let fill_in_type env typ =
subst_src_typ subst typ
(* TODO: top-level patterns *)
+(* TODO: proper environment tracking for variables. Currently we pretend that
+ we can print the type of a variable in the top-level environment, but in
+ practice they might be below a case split. Note that we'd also need to
+ provide some way for the Lem pretty printer to know what to use; currently
+ we just use two names for the cast, bitvector_cast_in and bitvector_cast_out,
+ to let the pretty printer know whether to use the top-level environment. *)
let add_bitvector_casts (Defs defs) =
let rewrite_body id quant_kids top_env ret_typ exp =
let rewrite_aux (e,ann) =
@@ -4002,13 +4045,13 @@ let add_bitvector_casts (Defs defs) =
let body = match pat, guard with
| P_aux (P_lit (L_aux (L_num i,_)),_), _ ->
let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in
- make_bitvector_cast_exp env quant_kids src_typ result_typ
+ make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ
(make_bitvector_env_casts env quant_kids (kid,i) body)
| P_aux (P_id var,_), Some guard ->
(match extract_value_from_guard var guard with
| Some i ->
let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in
- make_bitvector_cast_exp env quant_kids src_typ result_typ
+ make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ
(make_bitvector_env_casts env quant_kids (kid,i) body)
| None -> body)
| _ ->
@@ -4019,15 +4062,46 @@ let add_bitvector_casts (Defs defs) =
E_aux (E_case (exp', List.map map_case cases),ann)
| _ -> E_aux (e,ann)
end
+ | E_if (e1,e2,e3) ->
+ let env = env_of_annot ann in
+ let result_typ = Env.base_typ_of env (typ_of_annot ann) in
+ let rec extract (E_aux (e,_)) =
+ match e with
+ | E_app (op,
+ ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] |
+ [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)]))
+ when string_of_id op = "eq_atom" ->
+ (match destruct_atom_nexp (env_of y) (typ_of y) with
+ | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)]
+ | _ -> [])
+ | E_app (op, [x;y]) when string_of_id op = "and_bool" ->
+ extract x @ extract y
+ | _ -> []
+ in
+ let insts = extract e1 in
+ let e2' = List.fold_left (fun body inst ->
+ make_bitvector_env_casts env quant_kids inst body) e2 insts in
+ let insts = List.fold_left (fun insts (kid,i) ->
+ KBindings.add kid (nconstant i) insts) KBindings.empty insts in
+ let src_typ = subst_src_typ insts result_typ in
+ let e2' = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ e2' in
+ E_aux (E_if (e1,e2',e3), ann)
| E_return e' ->
- E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
- (* TODO: (env_of_annot ann) isn't suitable, because it contains
- constraints revealing the case splits involved; needs a more
- subtle approach *)
+ E_aux (E_return (make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
| E_assign (LEXP_aux (lexp,lexp_annot),e') ->
E_aux (E_assign (LEXP_aux (lexp,lexp_annot),
- make_bitvector_cast_exp (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e'))
+ make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e'))
(typ_of_annot lexp_annot) e'),ann)
+ | E_id id -> begin
+ let env = env_of_annot ann in
+ match Env.lookup_id id env with
+ | Local (Mutable, vtyp) ->
+ make_bitvector_cast_exp "bitvector_cast_in" top_env quant_kids
+ (fill_in_type (env_of_annot ann) (typ_of_annot ann))
+ vtyp
+ (E_aux (e,ann))
+ | _ -> E_aux (e,ann)
+ end
| _ -> E_aux (e,ann)
in
let open Rewriter in
@@ -4052,7 +4126,7 @@ let add_bitvector_casts (Defs defs) =
let body = rewrite_body id quant_kids body_env ret_typ body in
(* Also add a cast around the entire function clause body, if necessary *)
let body =
- make_bitvector_cast_exp fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body
+ make_bitvector_cast_exp "bitvector_cast_out" fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body
in
let pexp = construct_pexp (pat,guard,body,annot) in
FCL_aux (FCL_Funcl (id,pexp),fcl_ann)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 04:04:23 +0000