diff options
| -rw-r--r-- | src/InterpreterStatements.ml | 19 | ||||
| -rw-r--r-- | src/PrintPure.ml | 21 | ||||
| -rw-r--r-- | src/Pure.ml | 6 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 20 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 20 |
5 files changed, 69 insertions, 17 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index e31a2152..09f13240 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -730,11 +730,22 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = let cf_assign cf (res : (V.typed_value, eval_error) result) ctx = match res with | Error EPanic -> cf Panic ctx - | Ok rvalue -> - let expr = assign_to_place config rvalue p (cf Unit) ctx in - (* Update the synthesized AST - here we store meta-information *) - S.synthesize_assignment (S.mk_mplace p ctx) rvalue expr + | Ok rv -> ( + let expr = assign_to_place config rv p (cf Unit) ctx in + (* Update the synthesized AST - here we store meta-information. + * We do it only in specific cases (it is not always useful, and + * also it can lead to issues - for instance, if we borrow an + * inactivated borrow, we later can't translate it to pure values...) *) + match rvalue with + | E.Use _ + | E.Ref (_, (E.Shared | E.Mut)) + | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ -> + S.synthesize_assignment (S.mk_mplace p ctx) rv expr + | E.Ref (_, E.TwoPhaseMut) -> + (* Two-phase borrow: don't synthesize meta-information *) + expr) in + (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx | A.FakeRead p -> diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 6f56c379..5223fb21 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -333,6 +333,23 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string = | Binop (binop, int_ty) -> binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">" +let mplace_to_string (fmt : ast_formatter) (p : mplace) : string = + let name = match p.name with None -> "_" | Some name -> name in + projection_to_string fmt name p.projection + +let meta_to_string (fmt : ast_formatter) (meta : meta) : string = + let meta = + match meta with + | Aggregate (p, rv) -> + let p = match p with None -> "_" | Some p -> mplace_to_string fmt p in + "@aggregate(" ^ p ^ " := " ^ typed_rvalue_to_string fmt rv ^ ")" + | Assignment (p, rv) -> + "@assign(" ^ mplace_to_string fmt p ^ " := " + ^ typed_rvalue_to_string fmt rv + ^ ")" + in + "@meta[" ^ meta ^ "]" + let rec expression_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (e : expression) : string = match e with @@ -341,6 +358,10 @@ let rec expression_to_string (fmt : ast_formatter) (indent : string) | Let (lb, e) -> let_to_string fmt indent indent_incr lb e | Switch (scrutinee, _, body) -> switch_to_string fmt indent indent_incr scrutinee body + | Meta (meta, e) -> + let meta = meta_to_string fmt meta in + let e = expression_to_string fmt indent indent_incr e in + indent ^ meta ^ "\n" ^ e and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (lb : let_bindings) (e : expression) : string = diff --git a/src/Pure.ml b/src/Pure.ml index ba0c9837..89748bdd 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -200,6 +200,11 @@ type let_bindings = code if we detect there is exactly one variant?... *) +(** Meta-information stored in the AST *) +type meta = + | Aggregate of mplace option * typed_rvalue + | Assignment of mplace * typed_rvalue + (** **Rk.:** here, [expression] is not at all equivalent to the expressions used in CFIM. They are lambda-calculus expressions, and are thus actually more general than the CFIM statements, in a sense. @@ -215,6 +220,7 @@ type expression = | Let of let_bindings * expression (** Let bindings include the let-bindings introduced because of function calls *) | Switch of typed_rvalue * mplace option * switch_body + | Meta of meta * expression (** Meta-information *) and switch_body = | If of expression * expression diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index 3148f833..07afd914 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -45,6 +45,16 @@ type call = { dest_place : mplace option; (** Meta information *) } +(** Meta information, not necessary for synthesis but useful to guide it to + generate a pretty output. + *) + +type meta = + | Aggregate of mplace option * V.typed_value + (** We generated an aggregate value *) + | Assignment of mplace * V.typed_value + (** We generated an assignment (destination, assigned value) *) + (** **Rk.:** here, [expression] is not at all equivalent to the expressions used in CFIM: they are a first step towards lambda-calculus expressions. *) @@ -87,13 +97,3 @@ 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 mplace option * V.typed_value - (** We generated an aggregate value *) - | Assignment of mplace * V.typed_value - (** We generated an assignment (destination, assigned value) *) diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 63d0df1d..4fa8e54c 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -879,9 +879,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx - | Meta (_, e) -> - (* We ignore the meta information *) - translate_expression e ctx + | Meta (meta, e) -> translate_meta meta e ctx and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : expression = @@ -1243,6 +1241,22 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) Switch (scrutinee, scrutinee_mplace, SwitchInt (int_ty, branches, otherwise)) +and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) : + expression = + let e = translate_expression e ctx in + let meta = + match meta with + | S.Aggregate (p, rv) -> + let p = translate_opt_mplace p in + let rv = typed_value_to_rvalue ctx rv in + Aggregate (p, rv) + | S.Assignment (p, rv) -> + let p = translate_mplace p in + let rv = typed_value_to_rvalue ctx rv in + Assignment (p, rv) + in + Meta (meta, e) + let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def = let def = ctx.fun_def in let bid = ctx.bid in |