diff options
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 30 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 29 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 20 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 14 | ||||
| -rw-r--r-- | src/Synthesis.ml | 84 | ||||
| -rw-r--r-- | src/SynthesizeSymbolic.ml | 40 |
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)) |