summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-26 16:17:08 +0100
committerSon Ho2022-01-26 16:17:08 +0100
commitc0fa50dc807a1edb39738cb16530018aa892fac4 (patch)
tree2a05aa6898bc8a33c2838705fc8c9fa2858cbbab
parentac2d7f421b8511c67614eb238865961e239486c2 (diff)
Start working on signatures for the assumed functions
-rw-r--r--src/Assumed.ml51
-rw-r--r--src/InterpreterStatements.ml3
-rw-r--r--src/main.ml2
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