summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Pure.ml53
-rw-r--r--src/SymbolicToPure.ml94
2 files changed, 91 insertions, 56 deletions
diff --git a/src/Pure.ml b/src/Pure.ml
index 869729a1..504f2c11 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -15,9 +15,6 @@ module SynthPhaseId = IdGen ()
(** We give an identifier to every phase of the synthesis (forward, backward
for group of regions 0, etc.) *)
-module BackwardFunId = IdGen ()
-(** Every backward function has its identifier *)
-
module VarId = IdGen ()
(** Pay attention to the fact that we also define a [VarId] module in Values *)
@@ -66,7 +63,7 @@ type symbolic_value = {
symbolic value was introduced.
*)
}
-(** TODO: remove? *)
+(** TODO: remove *)
type value = Concrete of constant_value | Adt of adt_value
@@ -83,11 +80,14 @@ type var = { id : VarId.id; ty : ty }
itself
*)
-(** Sometimes, when introducing several variables in an assignment (because
- deconstructing a tuple) we can ignore some of the values: in such situation
- we introduce dummy variables (extracted to "_").
- *)
-type var_or_dummy = Var of var | Dummy
+type var_or_dummy = Var of var | Dummy (** Ignored value: `_` *)
+
+(** A left value (which appears on the left of assignments *)
+type lvalue =
+ | LvVar of var_or_dummy
+ | LvTuple of lvalue list (** Rk.: for now we don't support general ADTs *)
+
+and typed_lvalue = { value : lvalue; ty : ty }
type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
@@ -95,34 +95,41 @@ type projection = projection_elem list
type place = { var : VarId.id; projection : projection }
-(* TODO: this doesn't make sense: value can contain variables... *)
-type operand = Value of typed_value | Place of place
+type rvalue =
+ | RvPlace of place
+ | RvConcrete of constant_value
+ | RvAdt of adt_rvalue
-(* type assertion = { cond : operand; expected : bool } *)
+and adt_rvalue = {
+ variant_id : (VariantId.id option[@opaque]);
+ field_values : typed_rvalue list;
+}
+
+and typed_rvalue = { value : rvalue; ty : ty }
+(** In most situations we won't use the type in [typed_rvalue].
+ Note that it is still necessary to have some useful informations
+ about ADTs, though.
+ *)
type fun_id =
- | Local of A.FunDefId.id * BackwardFunId.id option
+ | Regular of A.fun_id * T.RegionGroupId.id option
(** Backward id: `Some` if the function is a backward function, `None`
if it is a forward function *)
- | Assumed of A.assumed_fun_id
| Unop of E.unop
| Binop of E.binop
-type call = { func : fun_id; type_params : ty list; args : operand list }
+type call = { func : fun_id; type_params : ty list; args : typed_rvalue list }
type left_value = unit
(** TODO: assignment left value *)
-type lvalue = typed_value
-(* TODO: define that *)
-
type let_bindings =
- | Call of lvalue list * call
+ | Call of typed_lvalue list * call
(** The called function and the tuple of returned values. *)
- | Assignment of var * operand
+ | Assignment of var * typed_rvalue
(** Variable assignment: the introduced variable and the place we read *)
| Deconstruct of
- var_or_dummy list * (TypeDefId.id * VariantId.id) option * operand
+ var_or_dummy list * (TypeDefId.id * VariantId.id) option * typed_rvalue
(** This is used in two cases.
1. When deconstructing a tuple:
@@ -159,11 +166,11 @@ type let_bindings =
more general than the CFIM statements, in a sense.
*)
type expression =
- | Return of operand
+ | Return of typed_rvalue
| Panic
| Let of let_bindings * expression
(** Let bindings include the let-bindings introduced because of function calls *)
- | Switch of operand * switch_body
+ | Switch of typed_rvalue * switch_body
and switch_body =
| If of expression * expression
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 97d9baf1..a8e5be0d 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -97,6 +97,24 @@ let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) :
(** Generates a name for a type (simply reuses the name in the definition) *)
let translate_type_name (def : T.type_def) : Id.name = def.T.name
+(* TODO: move *)
+let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
+
+let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
+ let value = RvPlace (mk_place_from_var v) in
+ let ty = v.ty in
+ { value; ty }
+
+(* TODO: move *)
+let type_def_is_enum (def : T.type_def) : bool =
+ match def.kind with T.Struct _ -> false | Enum _ -> true
+
+(* TODO: move *)
+let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
+ let value = LvVar (Var v) in
+ let ty = v.ty in
+ { value; ty }
+
type type_context = {
types_infos : TA.type_infos;
cfim_type_defs : T.type_def TypeDefId.Map.t;
@@ -154,7 +172,8 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
let calls = V.FunCallId.Map.add call_id info calls in
{ ctx with calls }
-let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx =
+let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx * fun_id
+ =
(* Insert the abstraction in the call informations *)
let back_id = Option.get abs.back_id in
let info = V.FunCallId.Map.find abs.call_id ctx.calls in
@@ -166,8 +185,14 @@ let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx =
let abstractions = ctx.abstractions in
assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
let abstractions = V.AbstractionId.Map.add abs.abs_id abs abstractions in
- (* Update the context *)
- { ctx with calls; abstractions }
+ (* Retrieve the fun_id *)
+ let fun_id =
+ match info.forward.call_id with
+ | S.Fun (fid, _) -> Regular (fid, Some (Option.get abs.back_id))
+ | S.Unop _ | S.Binop _ -> failwith "Unreachable"
+ in
+ (* Update the context and return *)
+ ({ ctx with calls; abstractions }, fun_id)
let rec translate_sty (ty : T.sty) : ty =
let translate = translate_sty in
@@ -447,7 +472,8 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def)
- end abstraction
- return
*)
-let translate_typed_value (ctx : bs_ctx) (v : V.typed_value) : typed_value =
+let translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
+ typed_rvalue =
raise Unimplemented
let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) :
@@ -461,25 +487,19 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx)
let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
raise Unimplemented
-(* TODO: move *)
-let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
-
-(* TODO: move *)
-let type_def_is_enum (def : T.type_def) : bool =
- match def.kind with T.Struct _ -> false | Enum _ -> true
-
let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
- typed_value option =
+ typed_rvalue option =
raise Unimplemented
-let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_value list =
+let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
let typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
- bs_ctx * lvalue option =
+ bs_ctx * typed_lvalue option =
raise Unimplemented
-let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * lvalue list =
+let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_lvalue list
+ =
let ctx, values =
List.fold_left_map
(fun ctx av -> typed_avalue_to_given_back av ctx)
@@ -501,8 +521,8 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression =
match e with
| S.Return v ->
- let v = translate_typed_value ctx v in
- Return (Value v)
+ let v = translate_typed_value_to_rvalue ctx v in
+ Return v
| Panic -> Panic
| FunCall (call, e) -> translate_function_call call e ctx
| EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
@@ -515,8 +535,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
expression =
(* Translate the function call *)
let type_params = List.map (translate_fwd_ty ctx) call.type_params in
- let args = List.map (translate_typed_value ctx) call.args in
- let args = List.map (fun v -> Value v) args in
+ let args = List.map (translate_typed_value_to_rvalue ctx) call.args in
let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
(* Retrieve the function id, and register the function call in the context
* if necessary *)
@@ -524,11 +543,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
match call.call_id with
| S.Fun (fid, call_id) ->
let ctx = bs_ctx_register_forward_call call_id call ctx in
- let func =
- match fid with
- | A.Local fid -> Local (fid, None)
- | A.Assumed fid -> Assumed fid
- in
+ let func = Regular (fid, None) in
(ctx, func)
| S.Unop unop -> (ctx, Unop unop)
| S.Binop binop -> (ctx, Binop binop)
@@ -537,7 +552,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
(* Translate the next expression *)
let e = translate_expression e ctx in
(* Put together *)
- Let (Call ([ Var dest ], call), e)
+ Let (Call ([ mk_typed_lvalue_from_var dest ], call), e)
and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
expression =
@@ -546,24 +561,32 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
(* There are no nested borrows for now: we shouldn't get there *)
raise Unimplemented
| V.FunCall ->
+ let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
+ let call = call_info.forward in
+ let type_params = List.map (translate_fwd_ty ctx) call.type_params in
(* Retrive the orignal call and the parent abstractions *)
let forward, backwards = get_abs_ancestors ctx abs in
(* Retrieve the values consumed when we called the forward function and
* ended the parent backward functions: those give us part of the input
* values *)
- let fwd_inputs = List.map (translate_typed_value ctx) forward.args in
+ let fwd_inputs =
+ List.map (translate_typed_value_to_rvalue ctx) forward.args
+ in
let back_ancestors_inputs =
- List.concat (List.map abs_to_consumed backwards)
+ List.concat (List.map (abs_to_consumed ctx) backwards)
in
(* Retrieve the values consumed upon ending the loans inside this
* abstraction: those give us the remaining input values *)
- let back_inputs = abs_to_consumed abs in
+ let back_inputs = abs_to_consumed ctx abs in
let inputs =
List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs ]
in
(* Retrieve the values given back by this function: those are the output
* values *)
let ctx, outputs = abs_to_given_back abs ctx in
+ (* Retrieve the function id, and register the function call in the context
+ * if necessary *)
+ let ctx, func = bs_ctx_register_backward_call abs ctx in
(* Translate the next expression *)
let e = translate_expression e ctx in
(* Put everything together *)
@@ -577,7 +600,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
(ctx : bs_ctx) : expression =
(* Translate the scrutinee *)
let scrutinee_var = get_var_for_symbolic_value sv ctx in
- let scrutinee = Place (mk_place_from_var scrutinee_var) in
+ let scrutinee = mk_typed_rvalue_from_var scrutinee_var in
(* Translate the branches *)
match exp with
| ExpandNoBranch (sexp, e) -> (
@@ -617,18 +640,23 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
branch )
else
(* This is not an enumeration: introduce let-bindings for every
- * field *)
- let gen_field_proj (field_id : FieldId.id) : operand =
+ * field.
+ * We use the [dest] variable in order not to have to recompute
+ * the type of the result of the projection... *)
+ let gen_field_proj (field_id : FieldId.id) (dest : var) :
+ typed_rvalue =
let pkind = E.ProjAdt (adt_id, None) in
let pe : projection_elem = { pkind; field_id } in
let projection = [ pe ] in
let place = { var = scrutinee_var.id; projection } in
- Place place
+ let value = RvPlace place in
+ let ty = dest.ty in
+ { value; ty }
in
let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in
List.fold_right
(fun (fid, var) e ->
- let field_proj = gen_field_proj fid in
+ let field_proj = gen_field_proj fid var in
Let (Assignment (var, field_proj), e))
id_var_pairs branch
| T.Tuple ->