From cfba6f5617ce62ba8830adf6bf8b425714848e10 Mon Sep 17 00:00:00 2001 From: Ekanshdeep Gupta Date: Wed, 4 Dec 2024 19:34:53 -0500 Subject: [PATCH] partial fix to bugs in skolem expression creation. revealed other bugs in type-checking. --- lib/frontend/rewrites/heapsExplicitTrnsl.ml | 8 +++++-- lib/frontend/typing.ml | 23 ++++++++++++++++--- .../templates/give-up-simplified.rav | 10 ++++---- 3 files changed, 31 insertions(+), 10 deletions(-) diff --git a/lib/frontend/rewrites/heapsExplicitTrnsl.ml b/lib/frontend/rewrites/heapsExplicitTrnsl.ml index 17ec604..eeac717 100644 --- a/lib/frontend/rewrites/heapsExplicitTrnsl.ml +++ b/lib/frontend/rewrites/heapsExplicitTrnsl.ml @@ -3305,6 +3305,8 @@ module TrnslExhale = struct List.fold var_decls_skolem_idents ~init:(Map.empty (module QualIdent)) ~f:( fun map (vd, skolem_id) -> ( let skolemized_expr = + let univ_args = List.map univ_vars.univ_vars ~f:(fun (_, vd) -> Expr.from_var_decl vd) + in let optn_args = begin match Map.find witness_args_conds_exprs_map vd.var_name with | None -> [] @@ -3314,7 +3316,7 @@ module TrnslExhale = struct List.map env_local_var_decls_exprs ~f:(fun (_vd, expr) -> expr) end in - Expr.mk_app ~loc ~typ:(vd.var_type) (Expr.Var (QualIdent.from_ident skolem_id)) optn_args + Expr.mk_app ~loc ~typ:(vd.var_type) (Expr.Var (QualIdent.from_ident skolem_id)) (univ_args @ optn_args) in @@ -3752,7 +3754,9 @@ module TrnslExhale = struct if QualIdent.(orig_name = Predefs.lib_auth_mod_qual_ident) then match given_expr with - | App (DataConstr constr_ident, exprs, _) -> + | App (DataConstr constr_ident, exprs, _) + | App (Var constr_ident, exprs, _) -> + (* #TODO: This exception is added to tackle the case of using AuthRA.auth() function, which is different from the AuthRA.auth_frag() data constructor. As such, this exception is not added in the explicit calculation which should ideally be fixed. *) if Ident.( QualIdent.unqualify constr_ident diff --git a/lib/frontend/typing.ml b/lib/frontend/typing.ml index d3ca009..1b8e59a 100644 --- a/lib/frontend/typing.ml +++ b/lib/frontend/typing.ml @@ -124,6 +124,18 @@ end let check_and_set (expr : expr) (given_typ_lb : type_expr) (given_typ_ub : type_expr) (expected_typ : type_expr) : expr Rewriter.t = let open Rewriter.Syntax in + + Logs.debug (fun m -> m "Frontend.typing.check_and_set: expr: %a; + given_typ_lb: %a + given_typ_ub: %a + expected_typ: %a" + Expr.pr expr + Type.pr given_typ_lb + Type.pr given_typ_ub + Type.pr expected_typ + ); + + let expected_ghost = Type.is_ghost expected_typ in let+ given_typ_lb = try ProcessTypeExpr.expand_type_expr given_typ_lb @@ -139,12 +151,13 @@ let check_and_set (expr : expr) (given_typ_lb : type_expr) in let typ = Type.meet given_typ_ub expected_typ |> Type.set_ghost expected_ghost in if Type.subtype_of given_typ_lb typ then Expr.set_type expr typ - else type_mismatch_error (Expr.to_loc expr) expected_typ given_typ_ub + else + (Logs.debug (fun m -> m "type_mismatch_error:0"); type_mismatch_error (Expr.to_loc expr) expected_typ given_typ_ub) (** Infer and check type of [expr] subject to typing environment [tbl] and expected type [expected_typ] *) let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t = - Logs.debug (fun m -> m !"process_expr: %{Expr} %b" expr (Type.is_ghost expected_typ)); + Logs.debug (fun m -> m !"process_expr: %{Expr}; isGhost: %b" expr (Type.is_ghost expected_typ)); let open Rewriter.Syntax in match expr with | App (constr, expr_list, expr_attr) -> ( @@ -988,6 +1001,7 @@ module ProcessCallable = struct }, disam_tbl ) | typ -> + Logs.debug (fun m -> m "type_mismatch_error:1"); type_mismatch_error (Expr.to_loc token) (Type.atomic_token (Ident.make Loc.dummy "?" 0 |> QualIdent.from_ident)) typ end | _ -> @@ -1016,6 +1030,7 @@ module ProcessCallable = struct }, disam_tbl ) | typ -> + Logs.debug (fun m -> m "type_mismatch_error:2"); type_mismatch_error (Expr.to_loc token) (Type.atomic_token (Ident.make Loc.dummy "?" 0 |> QualIdent.from_ident)) typ end | _ -> Error.type_error loc "commitAU takes at least one argument" @@ -1034,6 +1049,7 @@ module ProcessCallable = struct ( Stmt.AUAction { auaction_kind = AbortAU token }, disam_tbl ) | typ -> + Logs.debug (fun m -> m "type_mismatch_error:3"); type_mismatch_error (Expr.to_loc token) (Type.atomic_token (Ident.make Loc.dummy "?" 0 |> QualIdent.from_ident)) typ end | _ -> Error.type_error loc "abortAU takes exactly one argument" @@ -1566,7 +1582,8 @@ module ProcessCallable = struct (Stmt.New new_desc, disam_tbl) else - type_mismatch_error stmt_loc Type.ref var_decl.var_type + (Logs.debug (fun m -> m "type_mismatch_error:4"); + type_mismatch_error stmt_loc Type.ref var_decl.var_type) (* The following constructs are not expected here because the parser stores these commands as Assign stmts. The job of this function is to intercept the Assign stmts with the specific expressions on the RHS, and then transform them to the appropriate construct, ie Call, New, BindAU, OpenAU, AbortAU, CommitAU etc. diff --git a/test/concurrent/templates/give-up-simplified.rav b/test/concurrent/templates/give-up-simplified.rav index 030539e..37734f1 100644 --- a/test/concurrent/templates/give-up-simplified.rav +++ b/test/concurrent/templates/give-up-simplified.rav @@ -198,7 +198,7 @@ interface GiveUpTemplate[Node: NodeImpl] { atomic requires css(r, c) atomic ensures css(r, c) && nodePred(r, n, c_n, i_n) && inFP(r, n) { - ghost var phi: AtomicToken := bindAU(); + ghost var phi := bindAU(); ghost var g_i0: Flow_K; @@ -222,7 +222,7 @@ interface GiveUpTemplate[Node: NodeImpl] { atomic requires css(r, c) atomic ensures css(r, c) && inFP(r, n) { - ghost var phi: AtomicToken := bindAU(); + ghost var phi := bindAU(); ghost val c1: Set[K] := openAU(phi); unfold css(r, c1); cssInFp(r, n, c1); @@ -330,7 +330,7 @@ interface GiveUpTemplate[Node: NodeImpl] { lemma fpInStep(r: Ref, n: Ref, n1: Ref, k: K, c: Set[K], c_n: Set[K], i_n: Flow_K, implicit ghost g_i: Flow_K) requires cssR(r, c, g_i) requires nodePred(r, n, c_n, i_n) -f requires k in outset(i_n, n1) + requires k in outset(i_n, n1) requires n in g_i.dom ensures cssR(r, c, g_i) ensures nodePred(r, n, c_n, i_n) @@ -361,7 +361,7 @@ f requires k in outset(i_n, n1) ensures inFP(r, nn) ensures k in keyset(i_nn) { - ghost val phi: AtomicToken := bindAU(); + ghost val phi := bindAU(); ghost var c_n: Set[K]; ghost var i_n: Flow_K; @@ -473,7 +473,7 @@ f requires k in outset(i_n, n1) atomic requires css(r, c) atomic ensures css(r, cc) && opSpec(dop, k, c) == ((cc, res)) { - ghost val phi: AtomicToken := bindAU(); + ghost val phi := bindAU(); var n: Ref; var c_n: Set[K];