summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/InterpreterBorrows.ml9
-rw-r--r--compiler/InterpreterStatements.ml4
-rw-r--r--compiler/PrintPure.ml25
-rw-r--r--compiler/Pure.ml8
-rw-r--r--compiler/PureMicroPasses.ml81
-rw-r--r--compiler/PureUtils.ml18
-rw-r--r--compiler/SymbolicAst.ml3
-rw-r--r--compiler/SymbolicToPure.ml68
-rw-r--r--compiler/SynthesizeSymbolic.ml6
9 files changed, 196 insertions, 26 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 03b2b045..17810705 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -935,7 +935,11 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
(* Give back the value *)
let ctx = give_back config l bc ctx in
(* Do a sanity check and continue *)
- cf_check cf ctx
+ let cc = cf_check in
+ (* Save a snapshot of the environment for the name generation *)
+ let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in
+ (* Compose *)
+ cc cf ctx
and end_borrows_aux (config : config) (chain : borrow_or_abs_ids)
(allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun =
@@ -1041,6 +1045,9 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
(* Sanity check: ending an abstraction must preserve the invariants *)
let cc = comp cc Invariants.cf_check_invariants in
+ (* Save a snapshot of the environment for the name generation *)
+ let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in
+
(* Apply the continuation *)
cc cf ctx
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 95a2956b..6b9f47ce 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -931,9 +931,11 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
^ statement_to_string_with_tab ctx st
^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
+ (* Take a snapshot of the current context for the purpose of generating pretty names *)
+ let cc = S.cf_save_snapshot in
(* Expand the symbolic values if necessary - we need to do that before
* checking the invariants *)
- let cc = greedy_expand_symbolic_values config in
+ let cc = comp cc (greedy_expand_symbolic_values config) in
(* Sanity check *)
let cc = comp cc Invariants.cf_check_invariants in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index a401594d..00a431a0 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -585,7 +585,7 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string)
let meta_s = emeta_to_string env meta in
let e = texpression_to_string env inside indent indent_incr e in
match meta with
- | Assignment _ | SymbolicAssignment _ | Tag _ ->
+ | Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ ->
let e = meta_s ^ "\n" ^ indent ^ e in
if inside then "(" ^ e ^ ")" else e
| MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
@@ -717,10 +717,25 @@ and emeta_to_string (env : fmt_env) (meta : emeta) : string =
"@assign(" ^ mplace_to_string env lp ^ " := "
^ texpression_to_string env false "" "" rv
^ rp ^ ")"
- | SymbolicAssignment (var_id, rv) ->
- "@symb_assign(" ^ VarId.to_string var_id ^ " := "
- ^ texpression_to_string env false "" "" rv
- ^ ")"
+ | SymbolicAssignments info ->
+ let infos =
+ List.map
+ (fun (var_id, rv) ->
+ VarId.to_string var_id ^ " == "
+ ^ texpression_to_string env false "" "" rv)
+ info
+ in
+ let infos = String.concat ", " infos in
+ "@symb_assign(" ^ infos ^ ")"
+ | SymbolicPlaces info ->
+ let infos =
+ List.map
+ (fun (var_id, name) ->
+ VarId.to_string var_id ^ " == \"" ^ name ^ "\"")
+ info
+ in
+ let infos = String.concat ", " infos in
+ "@symb_places(" ^ infos ^ ")"
| MPlace mp -> "@mplace=" ^ mplace_to_string env mp
| Tag msg -> "@tag \"" ^ msg ^ "\""
in
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index cf6710aa..7de7e0f4 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -807,12 +807,18 @@ and emeta =
The mvalue stores the value which is put in the destination
The second (optional) mplace stores the origin.
*)
- | SymbolicAssignment of (var_id[@opaque]) * mvalue
+ | SymbolicAssignments of ((var_id[@opaque]) * mvalue) list
(** Informationg linking a variable (from the pure AST) to an
expression.
We use this to guide the heuristics which derive pretty names.
*)
+ | SymbolicPlaces of ((var_id[@opaque]) * string) list
+ (** Informationg linking a variable (from the pure AST) to a name.
+
+ We generate this information by exploring the context, and use it
+ to derive pretty names.
+ *)
| MPlace of mplace (** Meta-information about the origin of a value *)
| Tag of string (** A tag - typically used for debugging *)
[@@deriving
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1820b86a..a1f6ce33 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -334,6 +334,15 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let ctx1 = obj#visit_typed_pattern () lv () in
merge_ctxs ctx ctx1
in
+ (* If we have [x = y] where x and y are variables, add a constraint linking
+ the names of x and y *)
+ let add_eq_var_constraint (lv : typed_pattern) (re : texpression)
+ (ctx : pn_ctx) : pn_ctx =
+ match (lv.value, re.e) with
+ | PatVar (lv, _), Var rv when Option.is_some lv.basename ->
+ add_pure_var_constraint rv (Option.get lv.basename) ctx
+ | _ -> ctx
+ in
(* This is used to propagate constraint information about places in case of
* variable reassignments: we try to propagate the information from the
@@ -428,6 +437,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let ctx, re = update_texpression re ctx in
let ctx, e = update_texpression e ctx in
let lv = update_typed_pattern ctx lv in
+ let ctx = add_eq_var_constraint lv re ctx in
(ctx, Let (monadic, lv, re, e))
(* *)
and update_switch_body (scrut : texpression) (body : switch_body)
@@ -524,8 +534,15 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| _ -> ctx
in
ctx
- | SymbolicAssignment (var_id, rvalue) ->
- add_pure_var_value_constraint var_id rvalue ctx
+ | SymbolicAssignments infos ->
+ List.fold_left
+ (fun ctx (var_id, rvalue) ->
+ add_pure_var_value_constraint var_id rvalue ctx)
+ ctx infos
+ | SymbolicPlaces infos ->
+ List.fold_left
+ (fun ctx (var_id, name) -> add_pure_var_constraint var_id name ctx)
+ ctx infos
| MPlace mp -> add_right_constraint mp e ctx
| Tag _ -> ctx
in
@@ -1075,6 +1092,33 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
]}
*)
let simplify_let_then_return _ctx def =
+ (* Match a pattern and an expression: evaluates to [true] if the expression
+ is actually exactly the pattern *)
+ let rec match_pattern_and_expr (pat : typed_pattern) (e : texpression) : bool
+ =
+ match (pat.value, e.e) with
+ | PatConstant plit, Const lit -> plit = lit
+ | PatVar (pv, _), Var vid -> pv.id = vid
+ | PatDummy, _ ->
+ (* It is ok only if we ignore the unit value *)
+ pat.ty = mk_unit_ty && e = mk_unit_rvalue
+ | PatAdt padt, _ -> (
+ let qualif, args = destruct_apps e in
+ match qualif.e with
+ | Qualif { id = AdtCons cons_id; generics = _ } ->
+ if
+ pat.ty = e.ty
+ && padt.variant_id = cons_id.variant_id
+ && List.length padt.field_values = List.length args
+ then
+ List.for_all
+ (fun (p, e) -> match_pattern_and_expr p e)
+ (List.combine padt.field_values args)
+ else false
+ | _ -> false)
+ | _ -> false
+ in
+
let expr_visitor =
object (self)
inherit [_] map_expression
@@ -1090,13 +1134,24 @@ let simplify_let_then_return _ctx def =
(* Small shortcut to avoid doing the check on every let-binding *)
not_simpl_e
| _ -> (
- match typed_pattern_to_texpression lv with
- | None -> not_simpl_e
- | Some lv_v ->
- let lv_v =
- if monadic then mk_result_return_texpression lv_v else lv_v
- in
- if lv_v = next_e then rv.e else not_simpl_e)
+ if (* Do the check *)
+ monadic then
+ (* The first let-binding is monadic *)
+ match opt_destruct_ret next_e with
+ | Some e ->
+ if match_pattern_and_expr lv e then rv.e else not_simpl_e
+ | None -> not_simpl_e
+ else
+ (* The first let-binding is not monadic *)
+ match opt_destruct_ret next_e with
+ | Some e ->
+ if match_pattern_and_expr lv e then
+ (* We need to wrap the right-value in a ret *)
+ (mk_result_return_texpression rv).e
+ else not_simpl_e
+ | None ->
+ if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
+ )
end
in
@@ -1824,6 +1879,14 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
("inline_useless_var_assignments (pass 2):\n\n"
^ fun_decl_to_string ctx def ^ "\n"));
+ (* Simplify the let-then return again (the lambda simplification may have
+ unlocked more simplifications here) *)
+ let def = simplify_let_then_return ctx def in
+ log#ldebug
+ (lazy
+ ("simplify_let_then_return (pass 2):\n\n" ^ fun_decl_to_string ctx def
+ ^ "\n"));
+
(* Decompose the monadic let-bindings - used by Coq *)
let def =
if !Config.decompose_monadic_let_bindings then (
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 80bf3c42..81e3fbe1 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -752,3 +752,21 @@ let opt_dest_struct_pattern (pat : typed_pattern) : typed_pattern list option =
match pat.value with
| PatAdt { variant_id = None; field_values } -> Some field_values
| _ -> None
+
+(** Destruct a [ret ...] expression *)
+let opt_destruct_ret (e : texpression) : texpression option =
+ match e.e with
+ | App
+ ( {
+ e =
+ Qualif
+ {
+ id = AdtCons { adt_id = TAssumed TResult; variant_id };
+ generics = _;
+ };
+ ty = _;
+ },
+ arg )
+ when variant_id = Some result_return_id ->
+ Some arg
+ | _ -> None
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index cc74a16b..e164fd49 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -65,6 +65,9 @@ type call = {
type emeta =
| Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option
(** We generated an assignment (destination, assigned value, src) *)
+ | Snapshot of Contexts.eval_ctx
+ (** Remember an environment snapshot - this is useful to check where the
+ symbolic values are, to compute proper names for instance *)
[@@deriving show]
type variant_id = VariantId.id [@@deriving show]
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 58fb6d04..3fa550cc 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1873,10 +1873,48 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
(** Add meta-information to an expression *)
let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
(e : texpression) : texpression =
- let var_values = List.combine vars values in
- List.fold_right
- (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e)
- var_values e
+ let var_values = List.combine (List.map var_get_id vars) values in
+ if var_values <> [] then mk_emeta (SymbolicAssignments var_values) e else e
+
+(** Derive naming information from a context.
+
+ We explore the context and look in which bindings the symbolic values appear:
+ we use this information to derive naming information. *)
+let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
+ (ectx : Contexts.eval_ctx) : (VarId.id * string) list =
+ let info : (VarId.id * string) list ref = ref [] in
+ let push_info name sv = info := (name, sv) :: !info in
+ let visitor =
+ object (self)
+ inherit [_] Contexts.iter_eval_ctx
+
+ method! visit_env_elem _ ee =
+ match ee with
+ | EBinding (BVar { index = _; name = Some name }, v) ->
+ self#visit_typed_value name v
+ | _ -> () (* Ignore *)
+
+ method! visit_value name v =
+ match v with
+ | VLiteral _ | VBottom -> ()
+ | VBorrow (VMutBorrow (_, v)) | VLoan (VSharedLoan (_, v)) ->
+ self#visit_typed_value name v
+ | VSymbolic sv ->
+ (* Translate the type *)
+ let ty = ctx_translate_fwd_ty ctx sv.sv_ty in
+ (* If the type is unit, do nothing *)
+ if ty_is_unit ty then ()
+ else
+ (* Otherwise lookup the variable *)
+ let var = lookup_var_for_symbolic_value sv ctx in
+ push_info var.id name
+ | _ -> ()
+ end
+ in
+ (* Visit the context *)
+ visitor#visit_eval_ctx "x" ectx;
+ (* Return the computed information *)
+ !info
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
match e with
@@ -3528,11 +3566,23 @@ and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) :
let lp = translate_mplace lp in
let rv = typed_value_to_texpression ctx ectx rv in
let rp = translate_opt_mplace rp in
- Assignment (lp, rv, rp)
- in
- let e = Meta (meta, next_e) in
- let ty = next_e.ty in
- { e; ty }
+ Some (Assignment (lp, rv, rp))
+ | S.Snapshot ectx ->
+ let infos = eval_ctx_to_symbolic_assignments_info ctx ectx in
+ if infos <> [] then
+ (* If often happens that the next expression contains exactly the
+ same meta information *)
+ match next_e.e with
+ | Meta (SymbolicPlaces infos1, _) when infos1 = infos -> None
+ | _ -> Some (SymbolicPlaces infos)
+ else None
+ in
+ match meta with
+ | Some meta ->
+ let e = Meta (meta, next_e) in
+ let ty = next_e.ty in
+ { e; ty }
+ | None -> next_e
(** Wrap a function body in a match over the fuel to control termination. *)
let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression)
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index a42c43ac..ad34c48e 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -189,3 +189,9 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
meta;
})
| _ -> raise (Failure "Unreachable")
+
+let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) :
+ expression option =
+ match e with None -> None | Some e -> Some (Meta (Snapshot ctx, e))
+
+let cf_save_snapshot : Cps.cm_fun = fun cf ctx -> save_snapshot ctx (cf ctx)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:22:54 +0000