summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml4
-rw-r--r--src/InterpreterBorrows.ml30
-rw-r--r--src/InterpreterExpressions.ml29
-rw-r--r--src/InterpreterPaths.ml1
-rw-r--r--src/InterpreterStatements.ml20
-rw-r--r--src/SymbolicAst.ml14
-rw-r--r--src/Synthesis.ml84
-rw-r--r--src/SynthesizeSymbolic.ml40
8 files changed, 99 insertions, 123 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index dcdf6026..2c4d86d2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -77,8 +77,10 @@ module Test = struct
inst_sg.inputs
in
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+ let call_id = C.fresh_fun_call_id () in
+ assert (call_id = V.FunCallId.zero);
let empty_absl =
- create_empty_abstractions_from_abs_region_groups V.Synth
+ create_empty_abstractions_from_abs_region_groups call_id V.Synth
inst_sg.A.regions_hierarchy
in
(* Add the avalues to the abstractions and insert them in the context *)
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 8aafff30..442fe620 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -3,6 +3,7 @@ module V = Values
module C = Contexts
module Subst = Substitute
module L = Logging
+module S = SynthesizeSymbolic
open Cps
open ValuesUtils
open TypesUtils
@@ -996,7 +997,8 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
in
(* Remove all the references to the id of the current abstraction, and remove
- * the abstraction itself *)
+ * the abstraction itself.
+ * **Rk.**: this is where we synthesize the updated symbolic AST *)
let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
(* Debugging *)
@@ -1214,19 +1216,27 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
and end_abstraction_remove_from_context (_config : C.config)
(abs_id : V.AbstractionId.id) : cm_fun =
fun cf ctx ->
- let map_env_elem (ev : C.env_elem) : C.env_elem option =
- match ev with
- | C.Var (_, _) | C.Frame -> Some ev
- | C.Abs abs ->
- if abs.abs_id = abs_id then None
+ let rec remove_from_env (env : C.env) : C.env * V.abs option =
+ match env with
+ | [] -> failwith "Unreachable"
+ | C.Frame :: _ -> (env, None)
+ | Var (bv, v) :: env ->
+ let env, abs_opt = remove_from_env env in
+ (Var (bv, v) :: env, abs_opt)
+ | C.Abs abs :: env ->
+ if abs.abs_id = abs_id then (env, Some abs)
else
+ let env, abs_opt = remove_from_env env in
let parents = V.AbstractionId.Set.remove abs_id abs.parents in
- Some (C.Abs { abs with V.parents })
+ (C.Abs { abs with V.parents } :: env, abs_opt)
in
- let env = List.filter_map map_env_elem ctx.C.env in
+ let env, abs = remove_from_env ctx.C.env in
let ctx = { ctx with C.env } in
- (* Continue *)
- cf ctx
+ let abs = Option.get abs in
+ (* Apply the continuation *)
+ let expr = cf ctx in
+ (* Synthesize the symbolic AST *)
+ S.synthesize_end_abstraction abs expr
(** End a proj_loan over a symbolic value by ending the proj_borrows which
intersect this proj_loans.
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 808ad8c9..3ebce9bf 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -9,7 +9,7 @@ module L = Logging
open TypesUtils
open ValuesUtils
module Inv = Invariants
-module S = Synthesis
+module S = SynthesizeSymbolic
open Cps
open InterpreterUtils
open InterpreterExpansion
@@ -276,6 +276,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
let eval_op = eval_operand config op in
(* Generate a fresh symbolic value to store the result *)
let apply cf (v : V.typed_value) : m_fun =
+ fun ctx ->
let res_sv_id = C.fresh_symbolic_value_id () in
let res_sv_ty =
match (unop, v.V.ty) with
@@ -286,10 +287,10 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
let res_sv =
{ V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
in
- (* Synthesize *)
- S.synthesize_unary_op unop v res_sv;
(* Call the continuation *)
- cf (Ok (mk_typed_value_from_symbolic_value res_sv))
+ let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
+ (* Synthesize the symbolic AST *)
+ S.synthesize_unary_op unop v res_sv expr
in
(* Compose and apply *)
comp eval_op apply cf ctx
@@ -393,6 +394,7 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
let eval_ops = eval_two_operands config op1 op2 in
(* Compute the result of applying the binop *)
let compute cf ((v1, v2) : V.typed_value * V.typed_value) : m_fun =
+ fun ctx ->
(* Generate a fresh symbolic value to store the result *)
let res_sv_id = C.fresh_symbolic_value_id () in
let res_sv_ty =
@@ -421,11 +423,11 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
let res_sv =
{ V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
in
- (* Synthesize *)
- S.synthesize_binary_op binop v1 v2 res_sv;
(* Call the continuattion *)
let v = mk_typed_value_from_symbolic_value res_sv in
- cf (Ok v)
+ let expr = cf (Ok v) ctx in
+ (* Synthesize the symbolic AST *)
+ S.synthesize_binary_op binop v1 v2 res_sv expr
in
(* Compose and apply *)
comp eval_ops compute cf ctx
@@ -565,7 +567,6 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
let eval_rvalue_aggregate (config : C.config)
(aggregate_kind : E.aggregate_kind) (ops : E.operand list)
(cf : V.typed_value -> m_fun) : m_fun =
- S.synthesize_eval_rvalue_aggregate aggregate_kind ops;
(* Evaluate the operands *)
let eval_ops = eval_operands config ops in
(* Compute the value *)
@@ -578,7 +579,11 @@ let eval_rvalue_aggregate (config : C.config)
let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
let v = V.Adt { variant_id = None; field_values = values } in
let ty = T.Adt (T.Tuple, [], tys) in
- cf { V.value = v; ty } ctx
+ let aggregated : V.typed_value = { V.value = v; ty } in
+ (* Call the continuation *)
+ let expr = cf aggregated ctx in
+ (* Synthesize the symbolic AST *)
+ S.synthesize_aggregated_value aggregated expr
| E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
(* Sanity checks *)
let type_def = C.ctx_lookup_type_def ctx def_id in
@@ -595,7 +600,11 @@ let eval_rvalue_aggregate (config : C.config)
{ V.variant_id = opt_variant_id; V.field_values = values }
in
let aty = T.Adt (T.AdtId def_id, regions, types) in
- cf { V.value = Adt av; ty = aty } ctx
+ let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+ (* Call the continuation *)
+ let expr = cf aggregated ctx in
+ (* Synthesize the symbolic AST *)
+ S.synthesize_aggregated_value aggregated expr
in
(* Compose and apply *)
comp eval_ops compute cf
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index f364c386..e45dbb3a 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -4,7 +4,6 @@ module E = Expressions
module C = Contexts
module Subst = Substitute
module L = Logging
-module S = Synthesis
open Cps
open TypesUtils
open ValuesUtils
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 17fe700f..be0fb088 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -8,7 +8,7 @@ module L = Logging
open TypesUtils
open ValuesUtils
module Inv = Invariants
-module S = Synthesis
+module S = SynthesizeSymbolic
open Cps
open InterpreterUtils
open InterpreterProjectors
@@ -657,8 +657,8 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
Create abstractions (with no avalues, which have to be inserted afterwards)
from a list of abs region groups.
*)
-let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind)
- (rgl : A.abs_region_group list) : V.abs list =
+let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
+ (kind : V.abs_kind) (rgl : A.abs_region_group list) : V.abs list =
(* We use a reference to progressively create a map from abstraction ids
* to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id]
* returns the union of:
@@ -668,9 +668,6 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind)
let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref =
ref V.AbstractionId.Map.empty
in
- (* We generate *one* fresh call identifier for all the introduced abstractions
- * (it links them together) *)
- let call_id = C.fresh_fun_call_id () in
(* Auxiliary function to create one abstraction *)
let create_abs (back_id : V.BackwardFunctionId.id) (rg : A.abs_region_group) :
V.abs =
@@ -1032,8 +1029,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
args);
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+ let call_id = C.fresh_fun_call_id () in
let empty_absl =
- create_empty_abstractions_from_abs_region_groups V.FunCall
+ create_empty_abstractions_from_abs_region_groups call_id V.FunCall
inst_sg.A.regions_hierarchy
in
@@ -1058,11 +1056,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
in
let ctx = List.fold_left insert_abs ctx empty_absl in
- (* Synthesis *)
- S.synthesize_function_call fid region_params type_params args dest ret_spc;
+ (* Apply the continuation *)
+ let expr = cf ctx in
- (* Continue *)
- cf ctx
+ (* Synthesize the symbolic AST *)
+ S.synthesize_regular_function_call fid call_id type_params args ret_spc expr
in
let cc = comp cc cf_call in
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 6b66ada7..00431ebd 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -9,15 +9,14 @@ module V = Values
module E = Expressions
module A = CfimAst
-type fun_id =
- | Fun of A.fun_id
+type call_id =
+ | Fun of A.fun_id * V.FunCallId.id
(** A "regular" function (i.e., a function which is not a primitive operation) *)
| Unop of E.unop
| Binop of E.binop
type call = {
- call_id : V.FunCallId.id;
- func : A.fun_id;
+ call_id : call_id;
type_params : T.ety list;
args : V.typed_value list;
dest : V.symbolic_value;
@@ -29,6 +28,7 @@ type expression =
| FunCall of call * expression
| EndAbstraction of V.abs * expression
| Expansion of V.symbolic_value * expansion
+ | Meta of meta * expression (** Meta information *)
and expansion =
| ExpandNoBranch of V.symbolic_expansion * expression
@@ -45,3 +45,9 @@ and expansion =
T.integer_type * (V.scalar_value * expression) list * expression
(** An integer expansion (i.e, a switch over an integer). The last
expression is for the "otherwise" branch. *)
+
+(** Meta information, not necessary for synthesis but useful to guide it to
+ generate a pretty output.
+ *)
+
+and meta = Aggregate of V.typed_value (** We generated an aggregate value *)
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
deleted file mode 100644
index acecd517..00000000
--- a/src/Synthesis.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-module T = Types
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = CfimAst
-module L = Logging
-open Cps
-open InterpreterProjectors
-(* for symbolic_expansion definition *)
-
-(* TODO: the below functions have very "rough" signatures and do nothing: I
- * defined them so that the places where we should update the synthesized
- * program are clearly indicated in Interpreter.ml.
- * Also, some of those functions will probably be split, and their call site
- * will probably evolve.
- *
- * Small rk.: most functions should take an additional parameter for the
- * fresh symbolic value which stores the result of the computation.
- * For instance:
- * `synthesize_binary_op Add op1 op2 s`
- * should generate:
- * `s := op1 + op2`
- * *)
-
-(* TODO: error Panic *)
-
-(*
-type synth_function_res =
- (P.expression option, InterpreterExpressions.eval_error) result
-
-type synth_function = C.eval_ctx -> synth_function_res
-(** The synthesis functions (and thus the interpreter functions) are written
- in a continuation passing style. *)
-*)
-
-let synthesize_symbolic_expansion (_sv : V.symbolic_value)
- (resl : sexpr list option) : sexpr option =
- match resl with None -> None | Some resl -> Some (SList resl)
-
-(** Synthesize code for a symbolic expansion which doesn't lead to branching
- (i.e., applied on a value which is not an enumeration with several variants).
- *)
-let synthesize_symbolic_expansion_no_branching (_sv : V.symbolic_value)
- (_see : V.symbolic_expansion) : unit =
- ()
-
-(** Synthesize code for a symbolic enum expansion (which leads to branching)
- *)
-let synthesize_symbolic_expansion_enum_branching (_sv : V.symbolic_value)
- (_seel : V.symbolic_expansion list) : unit =
- ()
-
-let synthesize_symbolic_expansion_if_branching (_sv : V.symbolic_value) : unit =
- ()
-
-let synthesize_symbolic_expansion_switch_int_branching (_sv : V.symbolic_value)
- : unit =
- ()
-
-let synthesize_unary_op (_unop : E.unop) (_op : V.typed_value)
- (_dest : V.symbolic_value) : unit =
- ()
-
-let synthesize_binary_op (_binop : E.binop) (_op1 : V.typed_value)
- (_op2 : V.typed_value) (_dest : V.symbolic_value) : unit =
- ()
-
-(*
-let synthesize_eval_rvalue_ref (_p : E.place) (_bkind : E.borrow_kind) : unit =
- ()
-*)
-
-let synthesize_eval_rvalue_aggregate (_aggregate_kind : E.aggregate_kind)
- (_ops : E.operand list) : unit =
- ()
-
-let synthesize_function_call (_fid : A.fun_id)
- (_region_params : T.erased_region list) (_type_params : T.ety list)
- (_args : V.typed_value list) (_dest : E.place) (_res : V.symbolic_value) :
- unit =
- ()
-
-(*let synthesize_panic () : unit = ()*)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index b9bad7c9..1a30687c 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -49,7 +49,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
assert (otherwise_see = None);
(* Return *)
ExpandInt (int_ty, branches, otherwise)
- | T.Adt (adt_id, regions, types) -> (
+ | T.Adt (_, _, _) -> (
(* An ADT expansion can lead to branching: check if this is the case *)
match ls with
| [] -> failwith "Ill-formed ADT expansion"
@@ -72,7 +72,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
ls
in
ExpandEnum exp)
- | T.Ref (r, ty, rkind) -> (
+ | T.Ref (_, _, _) -> (
(* Reference expansion: there should be one branch *)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
@@ -87,3 +87,39 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
=
let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
synthesize_symbolic_expansion sv [ Some see ] exprl
+
+let synthesize_function_call (call_id : call_id) (type_params : T.ety list)
+ (args : V.typed_value list) (dest : V.symbolic_value)
+ (expr : expression option) : expression option =
+ match expr with
+ | None -> None
+ | Some expr ->
+ let call = { call_id; type_params; args; dest } in
+ Some (FunCall (call, expr))
+
+let synthesize_regular_function_call (fun_id : A.fun_id)
+ (call_id : V.FunCallId.id) (type_params : T.ety list)
+ (args : V.typed_value list) (dest : V.symbolic_value)
+ (expr : expression option) : expression option =
+ synthesize_function_call (Fun (fun_id, call_id)) type_params args dest expr
+
+let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
+ (dest : V.symbolic_value) (expr : expression option) : expression option =
+ synthesize_function_call (Unop unop) [] [ arg ] dest expr
+
+let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
+ (arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option)
+ : expression option =
+ synthesize_function_call (Binop binop) [] [ arg0; arg1 ] dest expr
+
+let synthesize_aggregated_value (aggr_v : V.typed_value)
+ (expr : expression option) : expression option =
+ match expr with
+ | None -> None
+ | Some expr -> Some (Meta (Aggregate aggr_v, expr))
+
+let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
+ expression option =
+ match expr with
+ | None -> None
+ | Some expr -> Some (EndAbstraction (abs, expr))