diff options
| -rw-r--r-- | src/Assumed.ml | 51 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 3 | ||||
| -rw-r--r-- | src/main.ml | 2 |
3 files changed, 54 insertions, 2 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml new file mode 100644 index 00000000..52e52b10 --- /dev/null +++ b/src/Assumed.ml @@ -0,0 +1,51 @@ +module T = Types +(** This module contains various utilities for the assumed functions *) + +module A = CfimAst +open TypesUtils + +(** `T -> Box<T>` *) +let box_new_sig : A.fun_sig = + let tvar_id_0 = T.TypeVarId.of_int 0 in + let tvar_0 = T.TypeVar tvar_id_0 in + { + region_params = []; + num_early_bound_regions = 0; + regions_hierarchy = []; + type_params = [ { index = tvar_id_0; name = "T" } ]; + inputs = [ tvar_0 (* T *) ]; + output = mk_box_ty tvar_0 (* Box<T> *); + } + +(** Helper for `Box::deref_shared` and `Box::deref_mut`. + Returns: + `&'a (mut) Box<T> -> &'a (mut) T` + *) +let box_deref_sig (is_mut : bool) : A.fun_sig = + let rvar_id_0 = T.RegionVarId.of_int 0 in + let rvar_0 = T.Var rvar_id_0 in + let rg_id_0 = T.RegionGroupId.of_int 0 in + let tvar_id_0 = T.TypeVarId.of_int 0 in + let tvar_0 = T.TypeVar tvar_id_0 in + let ref_kind = if is_mut then T.Mut else T.Shared in + (* The signature fields *) + let region_params = [ { T.index = rvar_id_0; name = Some "'a" } ] in + let regions_hierarchy = + [ { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } ] + (* <'a> *) + in + { + region_params; + num_early_bound_regions = 0; + regions_hierarchy; + type_params = [ { index = tvar_id_0; name = "T" } ] (* <T> *); + inputs = + [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) ref_kind (* &'a (mut) Box<T> *) ]; + output = mk_ref_ty rvar_0 tvar_0 ref_kind (* &'a (mut) T *); + } + +(** `&'a Box<T> -> &'a T` *) +let box_deref_shared_sig = box_deref_sig false + +(** `&'a mut Box<T> -> &'a mut T` *) +let box_deref_mut_sig = box_deref_sig true diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 83ad13fe..e1410ed3 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -15,6 +15,7 @@ open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +open Assumed (** The local logger *) let log = L.statements_log @@ -481,7 +482,7 @@ let eval_box_new_inst_sig (region_params : T.erased_region list) (type_params : T.ety list) : A.inst_fun_sig = (* The signature is: `T -> Box<T>` - where T is the type pram + where T is the type param *) match (region_params, type_params) with | [], [ ty_param ] -> diff --git a/src/main.ml b/src/main.ml index 2e1e552e..17821fea 100644 --- a/src/main.ml +++ b/src/main.ml @@ -76,5 +76,5 @@ let () = I.Test.test_unit_functions config m; (* Evaluate the symbolic interpreter on the functions *) - let synthesize = true in + let synthesize = false in I.Test.test_functions_symbolic config synthesize m |