Skip to content

Commit

Permalink
Fixed long-standing "order-of-exhales" witness computation bug
Browse files Browse the repository at this point in the history
  • Loading branch information
@EkanshdeepGupta
EkanshdeepGupta committed Oct 28, 2024
1 parent f110cb6 commit 41f66a5
Show file tree
Hide file tree
Showing 2 changed files with 150 additions and 52 deletions.
32 changes: 26 additions & 6 deletions lib/ast/rewriter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -202,17 +202,37 @@ let introduce_symbol symbol s =
},
() )

(* `f` represents a typechecking function that will be used to type-check
* `symbol` once the state has been set in the correct scope.
* This function is almost always intended to be `Typing.process_symbol` function.
* However, this cannot be set statically since
* that creates a recursive dependency between `module Rewriter` and `module Typing`. *)
let introduce_typecheck_symbol ~loc
~(f : AstDef.Module.symbol -> AstDef.Module.symbol t)
(symbol : Module.symbol) (s : 'a state) : 'a state * qual_ident =
(* f represents a typechecking function that will be used to type-check symbol in once the state has been set in the correct scope. Typically, this function will be the Typing.process_symbol function. However, this cannot be set statically since it will create a recursive dependency between Rewriter and Typing. *)

(* Logs.debug (fun m -> m "Rewriter.introduce_typecheck_symbol: symbol = %a" AstDef.Ident.pr (AstDef.Symbol.to_name symbol)); *)
(*Logs.debug (fun m ->
m "Rewriter.introduce_typecheck_symbol: symbol = %a" Symbol.pr symbol);*)

Logs.debug (fun m -> m
"Rewriter.introduce_typecheck_symbol: symbol = %a"
AstDef.Ident.pr (AstDef.Symbol.to_name symbol)
);
Logs.debug (fun m -> m
"Rewriter.introduce_typecheck_symbol: symbol = %a"
Symbol.pr symbol
);

let current_scope = s.state_table.tbl_curr.scope_id in
let qual_ident = QualIdent.append current_scope (Symbol.to_name symbol) in

Logs.debug (fun m -> m
"
Rewriter.introduce_typecheck_symbol: current_scope = %a \n \
Rewriter.introduce_typecheck_symbol: qual_ident = %a \n \
"
QualIdent.pr current_scope
QualIdent.pr qual_ident
);

let (s, _), already_defined =
try (declare_symbol symbol s, false) with _ -> ((s, ()), true)
in
Expand Down Expand Up @@ -258,8 +278,8 @@ let introduce_typecheck_symbol ~loc
else (f symbol s, qual_ident)
in

(*Logs.debug (fun m ->
m "Rewriter.introduce_typecheck_symbol end: symbol = %a" Symbol.pr symbol);*)
Logs.debug (fun m ->
m "Rewriter.introduce_typecheck_symbol end: symbol = %a" Symbol.pr symbol);

( {
s with
Expand Down
170 changes: 124 additions & 46 deletions lib/frontend/rewrites/heapsExplicitTrnsl.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2762,32 +2762,40 @@ module TrnslExhale = struct
~f:rewriter_user_annot_elim_exists_from_exhales

module WitnessComputation = struct
let rec find_witnesses_elim_exists (expr : expr) : expr Rewriter.t =
let rec find_witnesses_elim_exists (expr : expr) : (expr * expr list) Rewriter.t =
elim_a { univ_vars = []; triggers = [] } [] expr

and elim_a (universal_quants : universal_quants) (conds : conditions)
(expr : expr) : expr Rewriter.t =
(expr : expr) : (expr * expr list) Rewriter.t =
let open Rewriter.Syntax in
if%bind Rewriter.ProgUtils.is_expr_pure expr then Rewriter.return expr
if%bind Rewriter.ProgUtils.is_expr_pure expr then Rewriter.return (expr, [])
else
match expr with
| App (Ite, [ c; e1; e2 ], expr_attr) ->
let* e1 = elim_a universal_quants (c :: conds) e1 in
let* (e1, wtns_specs1) = elim_a universal_quants (c :: conds) e1 in

let not_c = Expr.mk_not ~loc:(Expr.to_loc c) c in
let* e2 = elim_a universal_quants (not_c :: conds) e2 in
let* (e2, wtns_specs2) = elim_a universal_quants (not_c :: conds) e2 in

Rewriter.return (Expr.App (Ite, [ c; e1; e2 ], expr_attr))
Rewriter.return (
(Expr.App (Ite, [ c; e1; e2 ], expr_attr)),
wtns_specs1 @ wtns_specs2
)
| App (Impl, [ c; e2 ], expr_attr) ->
let+ e2 = elim_a universal_quants (c :: conds) e2 in
Expr.App (Impl, [ c; e2 ], expr_attr)
let+ e2, wtns_specs = elim_a universal_quants (c :: conds) e2 in
Expr.App (Impl, [ c; e2 ], expr_attr), wtns_specs
| App (And, e_list, expr_attr) ->
let* e_list =
let* e_wtns_specs_list =
Rewriter.List.map e_list ~f:(fun e ->
elim_a universal_quants conds e)
in

Rewriter.return (Expr.App (And, e_list, expr_attr))
let e_list, wtns_specs = List.unzip e_wtns_specs_list in

Rewriter.return (
(Expr.App (And, e_list, expr_attr)),
(List.concat wtns_specs)
)
| Binder (Forall, var_decls, trgs, e, expr_attr) ->
let universal_quants =
let new_quants =
Expand All @@ -2805,14 +2813,16 @@ module TrnslExhale = struct
}
in

let* e = elim_a universal_quants conds e in
let* e, wtns_specs = elim_a universal_quants conds e in

Rewriter.return
(Expr.Binder (Forall, var_decls, trgs, e, expr_attr))
Rewriter.return (
(Expr.Binder (Forall, var_decls, trgs, e, expr_attr)),
wtns_specs
)
| _ -> elim_a1 universal_quants conds expr

and elim_a1 (univ_vars : universal_quants) (univ_conds : conditions)
(expr : expr) : expr Rewriter.t =
(expr : expr) : (expr * expr list) Rewriter.t =
let open Rewriter.Syntax in
match expr with
| Binder (Exists, var_decls, trgs, e, expr_attr) ->
Expand Down Expand Up @@ -3064,55 +3074,91 @@ module TrnslExhale = struct
expr)
in

let* temp_skolem_var_var_decls =
let* temp_skolem_var_decls__wtns_specs_list : (var_decl * expr) list =
Rewriter.List.map (List.zip_exn var_decls skolemized_exprs)
~f:(fun (var_decl, skolem_expr) ->
let skolem_wtns_var_tp =
if (List.is_empty univ_vars.univ_vars) then
var_decl.var_type
else
Type.mk_map loc (
Type.mk_prod loc
(List.map univ_vars.univ_vars ~f:(fun (_, vd) -> vd.var_type))
)
(* ~~~> *)
var_decl.var_type
in

let temp_skolem_var_decl = {
var_decl with
var_name = Ident.fresh loc @@
"$skolem_expr_placeholder$$" ^ (Ident.to_string var_decl.var_name);
var_type = skolem_wtns_var_tp

}
in

let skolem_placeholder_var_def = (Module.VarDef { var_decl = temp_skolem_var_decl; var_init = Some skolem_expr})
let skolem_placeholder_var_def = (Module.VarDef { var_decl = temp_skolem_var_decl; var_init = None})

in
in

let+ _ =
(* ************************************* *)
(* None of the following function calls:
*)
(* a. *)
Rewriter.introduce_typecheck_symbol ~loc ~f:Typing.process_symbol skolem_placeholder_var_def
(* nor
b. *)
(* Rewriter.introduce_symbol skolem_placeholder_var_def *)
(* nor
c. *)
(* Rewriter.add_locals [temp_skolem_var_decl] *)
(*
seem to work.
`$skolem_expr_placeholder$$` does not get added to
p().call_decl_locals
*)
(* ************************************* *)

Rewriter.introduce_typecheck_symbol ~loc ~f:Typing.process_symbol skolem_placeholder_var_def
in

let wtns_constraint_expr = match univ_vars.univ_vars with
| [] ->
Expr.mk_eq ~loc
(Expr.from_var_decl temp_skolem_var_decl)
skolem_expr

| _ ->
Expr.mk_binder ~loc
Forall (
List.map univ_vars.univ_vars ~f:(fun (_, vd) -> vd)
(* TODO: ^^^ Check if SMTLIB requires univ_vars need to be renamed when used in quantifiers. *)
) (* :: *) (
Expr.mk_eq ~loc
(* skolem_var[ univ_vars ] *)
(Expr.mk_maplookup
(Expr.from_var_decl temp_skolem_var_decl)
(Expr.mk_tuple
(List.map univ_vars.univ_vars ~f:(fun (_, vd) -> (Expr.from_var_decl vd)))
)
)
(* == *)
skolem_expr
)
in

temp_skolem_var_decl
temp_skolem_var_decl, wtns_constraint_expr
)
in

let temp_skolem_var_var_decls, wtns_specs_exprs = List.unzip temp_skolem_var_decls__wtns_specs_list
in

let renaming_map =
List.fold2_exn var_decls temp_skolem_var_var_decls
~init:(Map.empty (module QualIdent))
~f:(fun map var_decl temp_skolem_var_decl ->
Map.set map
~key:(QualIdent.from_ident var_decl.var_name)
~data:(Expr.from_var_decl temp_skolem_var_decl))
~data:(
match univ_vars.univ_vars with
| [] -> Expr.from_var_decl temp_skolem_var_decl
| _ ->
Expr.mk_maplookup
(Expr.from_var_decl temp_skolem_var_decl)
(* [ *)
(Expr.mk_tuple
(List.map univ_vars.univ_vars ~f:(
fun (_, vd) -> Expr.from_var_decl vd
))
)
(* ] *)
)
)
in

Logs.debug (fun m ->
Expand All @@ -3138,12 +3184,12 @@ module TrnslExhale = struct
in

let e = Expr.alpha_renaming e renaming_map_sanitized in
let* e = elim_a univ_vars univ_conds e in
let* e, wtns_specs = elim_a univ_vars univ_conds e in

Rewriter.return e
Rewriter.return (e, wtns_specs_exprs @ wtns_specs)
| _ ->
(* No existentials found *)
Rewriter.return expr
Rewriter.return (expr, [])

and elim_a0 (univ_vars : universal_quants) (exist_vars : var_decl list)
((univ_conds, exist_conds) : conditions * conditions) (expr : expr)
Expand Down Expand Up @@ -3533,25 +3579,57 @@ module TrnslExhale = struct
let rec rewriter_find_witness_elim_exists_from_exhale (stmt : Stmt.t) :
Stmt.t Rewriter.t =
let open Rewriter.Syntax in
let loc = Stmt.to_loc stmt in
match stmt.stmt_desc with
| Basic (Spec (Exhale, spec)) ->
let exhale_expr = spec.spec_form in
let* elim_expr =
let* elim_expr, wtns_specs =
WitnessComputation.find_witnesses_elim_exists exhale_expr
in

Logs.debug (fun m -> m
"WitnessComputation.rewriter_find_witness_elim_exists_from_exhale: \n \
init exhale_expr: %a \n \
elim exhale_expr: %a
"
Expr.pr exhale_expr
Expr.pr elim_expr
);

let spec = { spec with spec_form = elim_expr } in
let exhale_stmt = { stmt with stmt_desc = Basic (Spec (Exhale, spec)) } in

let wtns_specs_stmts = List.map wtns_specs ~f:(
fun spec_expr ->
Stmt.mk_assume_expr ~loc spec_expr
~cmnt:("Witness binding `assume`, for existentials during exhale.")
)
in

Rewriter.return (
Stmt.mk_block_stmt ~loc (wtns_specs_stmts @ [exhale_stmt])
)

Rewriter.return { stmt with stmt_desc = Basic (Spec (Exhale, spec)) }
| Basic (Spec (Assert, spec)) ->
let assert_expr = spec.spec_form in
let* elim_expr =
let* elim_expr, wtns_specs =
WitnessComputation.find_witnesses_elim_exists assert_expr
in

let spec = { spec with spec_form = elim_expr } in
let assert_stmt = { stmt with stmt_desc = Basic (Spec (Assert, spec)) } in

let wtns_specs_stmts = List.map wtns_specs ~f:(
fun spec_expr ->
Stmt.mk_assume_expr ~loc spec_expr
~cmnt:("Witness binding `assume`, for existentials during assert.")
)
in

Rewriter.return (
Stmt.mk_block_stmt ~loc (wtns_specs_stmts @ [assert_stmt])
)

Rewriter.return { stmt with stmt_desc = Basic (Spec (Assert, spec)) }
| _ ->
Rewriter.Stmt.descend stmt
~f:rewriter_find_witness_elim_exists_from_exhale
Expand Down

0 comments on commit 41f66a5

Please sign in to comment.