diff --git a/lib/ast/astDef.ml b/lib/ast/astDef.ml index aef14d1..c31e6b6 100644 --- a/lib/ast/astDef.ml +++ b/lib/ast/astDef.ml @@ -1197,7 +1197,11 @@ module Stmt = struct } type assign_desc = { assign_lhs : qual_ident list; assign_rhs : expr; assign_is_init : bool } - type bind_desc = { bind_lhs : qual_ident list; bind_rhs : expr } + + type bind_desc = { + bind_lhs : qual_ident list; + bind_rhs : spec; + } type field_read_desc = { field_read_lhs : qual_ident; @@ -1356,10 +1360,10 @@ module Stmt = struct astm.assign_rhs) | Bind bstm -> ( match bstm.bind_lhs with - | [] -> Expr.pr ppf bstm.bind_rhs + | [] -> Expr.pr ppf bstm.bind_rhs.spec_form | es -> fprintf ppf "@[<2>%a@ :|@ %a@]" QualIdent.pr_list es Expr.pr - bstm.bind_rhs) + bstm.bind_rhs.spec_form) | FieldRead fr -> fprintf ppf "@[<2>%a@ :=@ %a.%a@]" QualIdent.pr fr.field_read_lhs Expr.pr fr.field_read_ref QualIdent.pr fr.field_read_field | FieldWrite fw -> fprintf ppf "@[<2>%a.%a@ :=@ %a@]" Expr.pr fw.field_write_ref QualIdent.pr fw.field_write_field Expr.pr fw.field_write_val | Cas cs -> fprintf ppf "@[<2>%a@ :=@ cas(%a.%a, %a, %a)@]" QualIdent.pr cs.cas_lhs Expr.pr cs.cas_ref QualIdent.pr cs.cas_field Expr.pr cs.cas_old_val Expr.pr cs.cas_new_val @@ -1539,12 +1543,12 @@ module Stmt = struct (** Auxiliary functions *) - let mk_spec ?(atomic = false) ?cmnt ?(error = []) e = + let mk_spec ?(atomic = false) ?cmnt ?(spec_error = []) e = { spec_form = e; spec_atomic = atomic; spec_comment = cmnt; - spec_error = error; + spec_error; } let to_loc s = s.stmt_loc @@ -1588,7 +1592,7 @@ module Stmt = struct let accesses = List.fold bind_desc.bind_lhs ~init:accesses ~f:Set.add in - scan_expr_list accesses [bind_desc.bind_rhs] + scan_expr_list accesses [bind_desc.bind_rhs.spec_form] | FieldRead fr_desc -> let accesses = Set.add accesses fr_desc.field_read_lhs in @@ -1782,7 +1786,7 @@ module Stmt = struct Expr.expr_fields_accessed assign_desc.assign_rhs | Bind bind_desc -> - Expr.expr_fields_accessed bind_desc.bind_rhs + Expr.expr_fields_accessed bind_desc.bind_rhs.spec_form | FieldRead fr_desc -> [fr_desc.field_read_field] diff --git a/lib/ast/rewriter.ml b/lib/ast/rewriter.ml index bcb960f..7fe3de9 100644 --- a/lib/ast/rewriter.ml +++ b/lib/ast/rewriter.ml @@ -668,8 +668,9 @@ module Stmt = struct stmt_desc = Basic (Assign { assign with assign_rhs }); } | Bind bind_desc -> - let+ bind_rhs = f bind_desc.bind_rhs in - { stmt with stmt_desc = Basic (Bind { bind_desc with bind_rhs }) } + let+ spec_form = f bind_desc.bind_rhs.spec_form in + let bind_rhs = { bind_desc.bind_rhs with spec_form } in + { stmt with stmt_desc = Basic (Bind { bind_desc with bind_rhs }) } | FieldRead field_read_desc -> let field_read_lhs = field_read_desc.field_read_lhs in let field_read_field = field_read_desc.field_read_field in @@ -808,7 +809,8 @@ module Stmt = struct } | Bind bind_desc -> let bind_lhs = Base.List.map bind_desc.bind_lhs ~f in - let+ bind_rhs = Expr.rewrite_qual_idents ~f bind_desc.bind_rhs in + let+ spec_form = Expr.rewrite_qual_idents ~f bind_desc.bind_rhs.spec_form in + let bind_rhs = { bind_desc.bind_rhs with spec_form } in { stmt with stmt_desc = Basic (Bind { bind_lhs; bind_rhs }) } | FieldRead field_read_desc -> let field_read_lhs = f field_read_desc.field_read_lhs in diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly index f48f292..e0041aa 100644 --- a/lib/frontend/parser.mly +++ b/lib/frontend/parser.mly @@ -487,7 +487,7 @@ stmt_wo_trailing_substmt: in let bind = Stmt.{ bind_lhs = vs; - bind_rhs = e; + bind_rhs = mk_spec e; } in Stmt.(Basic (Bind bind)) @@ -498,8 +498,8 @@ stmt_wo_trailing_substmt: } (* assume / assert / inhale / exhale *) -| sk = SPEC; e = expr; mk_spec = with_clause { - mk_spec sk e +| sk = SPEC; e = expr; mk_spec_stmt = with_clause { + mk_spec_stmt sk e } (*| contract_mods ASSERT expr with_clause { $4 (fst $1) $3 (mk_position (if $1 <> (false, false) then 1 else 2) 4) None diff --git a/lib/frontend/rewrites/heapsExplicitTrnsl.ml b/lib/frontend/rewrites/heapsExplicitTrnsl.ml index 4b3cb2e..17ec604 100644 --- a/lib/frontend/rewrites/heapsExplicitTrnsl.ml +++ b/lib/frontend/rewrites/heapsExplicitTrnsl.ml @@ -377,7 +377,7 @@ let generate_inv_function ~loc (universal_quants : universal_quants) loc, "This iterated separating conjunction may not be injective on the quantified variable(s)") in - Stmt.mk_spec ~error:[fun _ -> error] spec_expr1 + Stmt.mk_spec ~spec_error:[fun _ -> error] spec_expr1 ) in let postcond2 = ( @@ -415,7 +415,7 @@ let generate_inv_function ~loc (universal_quants : universal_quants) loc, "This iterated separating conjunction may not be injective on the quantified variable(s)") in - Stmt.mk_spec ~error:[fun _ -> error] spec_expr2 + Stmt.mk_spec ~spec_error:[fun _ -> error] spec_expr2 ) in [], [postcond1; postcond2] @@ -1525,23 +1525,29 @@ let rec rewrite_binds (stmt : Stmt.t) : Stmt.t Rewriter.t = ~data:(Expr.from_var_decl e2)) in - let error = - ( Error.Verification, - Expr.to_loc bind_desc.bind_rhs, - "The right-hand side of this bind statement may not hold" ) + let spec_error = + match bind_desc.bind_rhs.spec_error with + | [] -> + let error = + ( Error.Verification, + Expr.to_loc bind_desc.bind_rhs.spec_form, + "The right-hand side of this bind statement may not hold" ) + in + [Stmt.mk_const_spec_error error] + | errors -> errors in let assert_stmt = Stmt.mk_assert_expr ~loc:stmt.stmt_loc ~cmnt:("Bind stmt: " ^ Stmt.to_string stmt) - ~spec_error:[ Stmt.mk_const_spec_error error ] + ~spec_error (Expr.mk_binder Exists ~loc:stmt.stmt_loc exis_vars - (Expr.alpha_renaming bind_desc.bind_rhs alpha_renaming_map)) + (Expr.alpha_renaming bind_desc.bind_rhs.spec_form alpha_renaming_map)) in let assume_stmt = Stmt.mk_assume_expr ~loc:stmt.stmt_loc ~cmnt:("Bind stmt: " ^ Stmt.to_string stmt) - bind_desc.bind_rhs + bind_desc.bind_rhs.spec_form in let new_stmt = @@ -1872,19 +1878,12 @@ module TrnslInhale = struct let* bind_lhs_var_decls = Rewriter.List.map bind_desc.bind_lhs ~f:(fun qual_ident -> - let* symbol = - Rewriter.find_and_reify qual_ident - in - match symbol with - | VarDef v -> Rewriter.return v.var_decl - | _ -> - Error.error - (Expr.to_loc bind_desc.bind_rhs) - "Expected a variable declaration") + let+ var_def = Rewriter.find_and_reify_var qual_ident in + var_def.var_decl) in match - match_up_expr bind_desc.bind_rhs prev_expr bind_lhs_var_decls + match_up_expr bind_desc.bind_rhs.spec_form prev_expr bind_lhs_var_decls with | None -> Logs.debug (fun m -> @@ -1904,14 +1903,14 @@ module TrnslInhale = struct let _, rhs = Map.find_exn var_map var_decl.var_name in Stmt.mk_assign - ~loc:(Expr.to_loc bind_desc.bind_rhs) + ~loc:(Expr.to_loc bind_desc.bind_rhs.spec_form) [ var_decl.var_name |> QualIdent.from_ident ] rhs) in Rewriter.return (Stmt.mk_block_stmt - ~loc:(Expr.to_loc bind_desc.bind_rhs) + ~loc:(Expr.to_loc bind_desc.bind_rhs.spec_form) assign_stmts))) | _ -> let* () = Rewriter.set_user_state None in diff --git a/lib/frontend/rewrites/rewrites.ml b/lib/frontend/rewrites/rewrites.ml index a59afbd..83706fd 100644 --- a/lib/frontend/rewrites/rewrites.ml +++ b/lib/frontend/rewrites/rewrites.ml @@ -1070,10 +1070,20 @@ let rec rewrite_fold_unfold_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t = let new_stmt = match use_desc.use_kind with | Fold -> + let spec_error = + let error = + ( Error.Verification, + stmt.stmt_loc, + "Failed to fold predicate. The body of the predicate may \ + not hold at this point" ) + in + [ Stmt.mk_const_spec_error error ] + in + let spec_form = Stmt.mk_spec ~spec_error new_body in let bind_stmt = Stmt.mk_bind ~loc:stmt.stmt_loc (List.map new_dropped_args ~f:(fun var_decl -> QualIdent.from_ident var_decl.var_name)) - new_body + spec_form in let inhale_stmt = @@ -1083,15 +1093,9 @@ let rec rewrite_fold_unfold_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t = in let exhale_stmt = - let error = - ( Error.Verification, - stmt.stmt_loc, - "Failed to fold predicate. The body of the predicate may \ - not hold at this point" ) - in Stmt.mk_exhale_expr ~loc ~cmnt:("fold : " ^ Expr.to_string pred_expr) - ~spec_error:[ Stmt.mk_const_spec_error error ] + ~spec_error body_fold_expr in (match new_dropped_args with @@ -1116,22 +1120,27 @@ let rec rewrite_fold_unfold_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t = Stmt.mk_block_stmt ~loc (usr_binds_havocs @ [pred_body_inhale_stmt]) in - let bind_stmt = - Stmt.mk_bind ~loc:stmt.stmt_loc - (List.map new_dropped_args ~f:(fun var_decl -> QualIdent.from_ident var_decl.var_name)) - pred_expr - in - - let exhale_stmt = + let spec_error = let error = ( Error.Verification, stmt.stmt_loc, "Failed to unfold predicate. The predicate may not hold at \ this point" ) in + [ Stmt.mk_const_spec_error error ] + in + + let bind_stmt = + Stmt.mk_bind ~loc:stmt.stmt_loc + (List.map new_dropped_args ~f:(fun var_decl -> QualIdent.from_ident var_decl.var_name)) + (Stmt.mk_spec pred_expr ~spec_error) + in + + let exhale_stmt = + Stmt.mk_exhale_expr ~loc ~cmnt:("unfold : " ^ Expr.to_string pred_expr) - ~spec_error:[ Stmt.mk_const_spec_error error ] + ~spec_error pred_expr in match new_dropped_args with @@ -1284,30 +1293,29 @@ let rec rewrite_call_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t = { spec with spec_form } in *) - let error = - ( Error.Verification, - stmt.stmt_loc, - "A precondition may not hold for this call" ) - in - - let assert_stmt = - Stmt.mk_assert_expr ~loc:stmt.stmt_loc - ~cmnt:("Assert stmt for Call: " ^ Stmt.to_string stmt) - ~spec_error:[ Stmt.mk_const_spec_error error ] - (* TODO: can we preserve the error messages for the individual preconditions here? *) - (Expr.mk_binder ~loc:stmt.stmt_loc Exists quant_dropped_args - (Expr.mk_and - (List.map call_decl.call_decl_precond ~f:(fun spec -> - Expr.alpha_renaming spec.spec_form quant_renaming_map)))) + let spec_error = + let error = + ( Error.Verification, + stmt.stmt_loc, + "A precondition may not hold for this call" ) + in + [ Stmt.mk_const_spec_error error ] in - - let bind_stmt = - Stmt.mk_bind ~loc:stmt.stmt_loc - (List.map new_dropped_args ~f:(fun var_decl -> QualIdent.from_ident var_decl.var_name)) + let spec_form = + Stmt.mk_spec + ~cmnt:("Bind stmt for Call: " ^ Stmt.to_string stmt) + ~spec_error (Expr.mk_and (List.map call_decl.call_decl_precond ~f:(fun spec -> Expr.alpha_renaming spec.spec_form new_renaming_map))) in + + let bind_stmt = + (* TODO: can we preserve the error messages for the individual preconditions here? *) + Stmt.mk_bind ~loc:stmt.stmt_loc + (List.map new_dropped_args ~f:(fun var_decl -> QualIdent.from_ident var_decl.var_name)) + spec_form + in let exhale_stmts = List.map call_decl.call_decl_precond ~f:(fun spec -> @@ -1317,7 +1325,7 @@ let rec rewrite_call_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t = in*) Stmt.mk_exhale_expr ~loc:stmt.stmt_loc ~cmnt:("Exhale stmt for Call: " ^ Stmt.to_string stmt) - ~spec_error:(Stmt.mk_const_spec_error error :: spec.spec_error) + ~spec_error:(spec_error @ spec.spec_error) (Expr.alpha_renaming spec.spec_form new_renaming_map)) in @@ -1345,9 +1353,9 @@ let rec rewrite_call_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t = | [], [] -> exhale_stmts @ [ inhale_stmt ] | [], _ -> exhale_stmts @ [ inhale_stmt; reassign_lhs_stmt ] | _, [] -> - (assert_stmt :: bind_stmt :: exhale_stmts) @ [ inhale_stmt ] + (bind_stmt :: exhale_stmts) @ [ inhale_stmt ] | _, _ -> - (assert_stmt :: bind_stmt :: exhale_stmts) + (bind_stmt :: exhale_stmts) @ [ inhale_stmt; reassign_lhs_stmt ]) in @@ -1937,7 +1945,7 @@ let rewrite_add_predicate_validity_lemmas (c : Callable.t) : out_arg1.var_loc, "This output parameter may not be uniquely determined by the input parameter(s)") in - Stmt.mk_spec ~error:[fun _ -> error] spec_expr) + Stmt.mk_spec ~spec_error:[fun _ -> error] spec_expr) in (in_args @ out_args1 @ out_args2, renamings1, renamings2, postconds) @@ -2156,8 +2164,9 @@ let rec rewrite_ssa_stmts (s : Stmt.t) : QualIdent.from_ident ident) in - let bind_rhs = Expr.alpha_renaming bind_stmt.bind_rhs subst_map in - + let spec_form = Expr.alpha_renaming bind_stmt.bind_rhs.spec_form subst_map in + let bind_rhs = { bind_stmt.bind_rhs with spec_form } in + Rewriter.return Stmt.{ s with stmt_desc = Basic (Bind { bind_lhs; bind_rhs }) } | _ -> diff --git a/lib/frontend/typing.ml b/lib/frontend/typing.ml index 04e316d..d3ca009 100644 --- a/lib/frontend/typing.ml +++ b/lib/frontend/typing.ml @@ -1340,10 +1340,11 @@ module ProcessCallable = struct qual_ident :: assign_lhs, var_decl :: var_decls_lhs ) in - let+ bind_rhs = - disambiguate_process_expr bind_desc.bind_rhs (Type.any |> Type.set_ghost true) + let+ spec_form = + disambiguate_process_expr bind_desc.bind_rhs.spec_form (Type.any |> Type.set_ghost true) disam_tbl in + let bind_rhs = { bind_desc.bind_rhs with spec_form } in let bind_desc = Stmt.{ bind_lhs; bind_rhs } in Stmt.Bind bind_desc, disam_tbl | FieldWrite fw_desc -> diff --git a/test/concurrent/templates/single-node.rav b/test/concurrent/templates/single-node.rav index ee76411..308e04b 100644 --- a/test/concurrent/templates/single-node.rav +++ b/test/concurrent/templates/single-node.rav @@ -2,7 +2,7 @@ module Lock { field bit: Bool - pred lock(l: Ref, b: Bool) { + pred lock(l: Ref; b: Bool) { own(l.bit, b, 1.0) } @@ -266,4 +266,4 @@ module IntSetNodeImpl : NodeImpl { unfold nodeR(n, c2); assert false; } -} \ No newline at end of file +}