attach error messages to bind statements; eliminate redundant assert …

…in proc call encoding

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]

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

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

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

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 }) }
       | _ ->

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 ->

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;
   }
-}
+}