disallow var as module members; disallow reassignment to val

lib/ast/astDef.ml

@@ -1066,7 +1066,7 @@ module Stmt = struct
     new_args : (qual_ident * expr option) list;
   }
 
-  type assign_desc = { assign_lhs : expr list; assign_rhs : expr }
+  type assign_desc = { assign_lhs : expr list; assign_rhs : expr; assign_is_init : bool }
   type bind_desc = { bind_lhs : expr list; bind_rhs : expr }
 
   type field_read_desc = { 
@@ -1380,7 +1380,7 @@ module Stmt = struct
     { stmt_desc = Basic (Call { call_lhs = lhs; call_name = name; call_args = args }); stmt_loc = loc }
 
   let mk_assign ~loc lhs rhs =
-    { stmt_desc = Basic (Assign { assign_lhs = lhs; assign_rhs = rhs }); stmt_loc = loc }
+    { stmt_desc = Basic (Assign { assign_lhs = lhs; assign_rhs = rhs; assign_is_init = false }); stmt_loc = loc }
 
   let mk_return ~loc e = { stmt_desc = Basic (Return e); stmt_loc = loc }
 

lib/ast/rewriter.ml

@@ -603,9 +603,9 @@ module Stmt = struct
       { stmt with stmt_desc = Basic (Spec (sk, { spec with spec_form = new_spec_form; })); }
 
     | Assign assign ->
-      let* new_lhs = List.map assign.assign_lhs ~f in
-      let+ new_expr = f assign.assign_rhs in
-      { stmt with stmt_desc = Basic (Assign { assign_lhs = new_lhs; assign_rhs = new_expr; }); }
+      let* assign_lhs = List.map assign.assign_lhs ~f in
+      let+ assign_rhs = f assign.assign_rhs in
+      { stmt with stmt_desc = Basic (Assign { assign with assign_lhs; assign_rhs; }); }
 
     | Bind bind_desc ->
       let* bind_lhs = List.map bind_desc.bind_lhs ~f in
@@ -711,7 +711,7 @@ module Stmt = struct
       | Assign assign ->
         let+ assign_rhs = Expr.rewrite_qual_idents ~f assign.assign_rhs
         and+ assign_lhs = List.map assign.assign_lhs ~f:(Expr.rewrite_qual_idents ~f) in
-        { stmt with stmt_desc = Basic (Assign { assign_lhs; assign_rhs }); }
+        { stmt with stmt_desc = Basic (Assign { assign with assign_lhs; assign_rhs }); }
 
       | Bind bind_desc ->
         let+ bind_lhs = List.map bind_desc.bind_lhs ~f:(Expr.rewrite_qual_idents ~f)

lib/frontend/parser.mly

@@ -131,7 +131,12 @@ mod_inst_args:
 | { [] }
 
 member_def_list_opt:
-| m = member_def; ms = member_def_list_opt { m :: ms }
+| m = member_def; ms = member_def_list_opt {
+  match m with
+  | Module.SymbolDef (VarDef { var_decl = { var_loc = loc; var_const = false; _}; _ }) ->
+      Error.syntax_error loc "Modules and interfaces cannot have var members"
+  | _ -> m :: ms
+}
 | m = member_def; SEMICOLON; ms = member_def_list_opt { m :: ms }
 | (* empty *) { [] }
 
@@ -397,6 +402,7 @@ stmt_wo_trailing_substmt:
   let assign =
     Stmt.{ assign_lhs = [];
            assign_rhs = e;
+           assign_is_init = false;
          }
   in
   Stmt.(Basic (Assign assign))
@@ -516,6 +522,7 @@ new_or_expr:
   let assign =
     Stmt.{ assign_lhs = [];
            assign_rhs = e;
+           assign_is_init = false
          }
   in
   Stmt.(Basic (Assign assign))

lib/frontend/rewrites/heapsExplicitTrnsl.ml

@@ -3026,7 +3026,7 @@ end
         else
           Error.type_error s.stmt_loc "Expected a FracRA type."
 
-      | Assign {assign_lhs = [Expr.App (Read, [ref_expr; field_expr], _)]; assign_rhs} ->
+      | Assign {assign_lhs = [Expr.App (Read, [ref_expr; field_expr], _)]; assign_rhs; _} ->
         let field_name = Expr.to_qual_ident field_expr in
 
         let* field_symbol = Rewriter.find_and_reify s.stmt_loc field_name in

lib/frontend/rewrites/rewrites.ml

@@ -20,7 +20,7 @@ let rec rewrite_stmt_error_msg call_id (stmt: Stmt.t): Stmt.t Rewriter.t =
       List.map loop_desc.loop_contract ~f:(fun spec ->
           let error callee =
             Error.Verification, Expr.to_loc spec.spec_form,
-            if Ident.(QualIdent.unqualify callee = call_id) then
+            if Ident.(QualIdent.unqualify callee <> call_id) then
               "This loop invariant may not hold upon loop entry"
             else 
               "This loop invariant may not be maintained"
@@ -1879,7 +1879,7 @@ let rec rewrite_ssa_stmts (s: Stmt.t) : (Stmt.t, var_decl ident_map) Rewriter.t_
 
       in
 
-      Rewriter.return Stmt.{ s with stmt_desc = Basic (Assign { assign_lhs; assign_rhs; }) }
+      Rewriter.return Stmt.{ s with stmt_desc = Basic (Assign { assign_stmt with assign_lhs; assign_rhs; }) }
 
     | Havoc qual_iden ->
       if QualIdent.is_local qual_iden then

lib/frontend/typing.ml

@@ -944,7 +944,7 @@ module ProcessCallable = struct
             let var_expr = (Expr.from_var_decl var_def.var_decl) in
 
               (* Expr.App (Var var, [], {expr_loc = stmt.stmt_loc; expr_type = var_decl.var_type}) in *)
-            let assign_desc = Stmt.{ assign_lhs = [var_expr]; assign_rhs = expr } in
+            let assign_desc = Stmt.{ assign_lhs = [var_expr]; assign_rhs = expr; assign_is_init = true } in
 
             let+ stmt, disam_tbl' = process_stmt {stmt_desc = (Stmt.Basic (Assign assign_desc)); stmt_loc = stmt.stmt_loc} disam_tbl' in
 
@@ -956,15 +956,26 @@ module ProcessCallable = struct
         Stmt.Basic (Spec (sk, spec)), disam_tbl
 
       | Assign assign_desc ->
-        (
-        List.iter assign_desc.assign_lhs ~f:(fun expr -> 
+        let* assign_lhs = Rewriter.List.map assign_desc.assign_lhs 
+            ~f:(fun expr -> disambiguate_process_expr expr Type.any disam_tbl)
+        in
+
+        let* _ = Rewriter.List.iter assign_lhs ~f:(fun expr -> 
           match expr with
           | App (Var qual_ident, [], _) -> 
-            ()
-          | App (Read, [ref_expr; field_expr], _) -> 
-            ()
-          | _ -> Error.type_error stmt.stmt_loc "Expected assignable expression on left-hand side of assignment"
-        );
+            let+ _, symbol = Rewriter.resolve_and_find stmt.stmt_loc qual_ident in
+            begin match Rewriter.Symbol.orig_symbol symbol with
+              | VarDef { var_decl = { var_const = true; _ }; _} when not assign_desc.assign_is_init ->
+                Error.type_error (Expr.to_loc expr) "Cannot assign to val"
+              | VarDef _ -> ()
+              | _ ->
+                Error.type_error (Expr.to_loc expr) "Expected assignable expression on left-hand side of assignment"
+            end
+            | App (Read, [ref_expr; field_expr], _) -> 
+              Rewriter.return ()
+            | _ -> Error.type_error (Expr.to_loc expr) "Expected assignable expression on left-hand side of assignment"
+          )
+        in
 
         Logs.debug (fun m -> m "process_stmt: assign_desc: %a" Stmt.pr_basic_stmt (Assign assign_desc));
         let* disam_assign_rhs = 
@@ -998,9 +1009,6 @@ module ProcessCallable = struct
                 process_au_action_stmt stmt.stmt_desc stmt.stmt_loc disam_tbl
             else begin
 
-              let* assign_lhs = Rewriter.List.map assign_desc.assign_lhs 
-                  ~f:(fun expr -> disambiguate_process_expr expr Type.any disam_tbl)
-              in
 
               let expected_return_type =
                 Type.mk_prod (Expr.to_loc assign_desc.assign_rhs) (List.map assign_lhs ~f:Expr.to_type)
@@ -1035,11 +1043,7 @@ module ProcessCallable = struct
           end
 
         | false ->
-          let* assign_lhs = Rewriter.List.map assign_desc.assign_lhs 
-            ~f:(fun expr -> 
-                 disambiguate_process_expr expr Type.any disam_tbl)
-          in
-
+
           let expected_type =
             Type.mk_prod stmt.stmt_loc (List.map assign_lhs ~f:Expr.to_type)
           in
@@ -1089,15 +1093,15 @@ module ProcessCallable = struct
           | _ ->
 
           let assign_desc =
-            Stmt.{ 
-              assign_lhs = assign_lhs;
-              assign_rhs = assign_rhs;
+            Stmt.{
+              assign_desc with
+              assign_lhs;
+              assign_rhs;
             }
           in
 
           Stmt.Basic (Assign assign_desc), disam_tbl
         end
-        )
 
       | Bind bind_desc ->
         let* bind_lhs = Rewriter.List.map bind_desc.bind_lhs ~f:(fun e -> 

test/ci/back-end/atomic_spec/counter_no_inv.rav

@@ -21,7 +21,7 @@ proc incr(x: Ref, implicit ghost v: Int)
   ghost var v2: Int := openAU(phi);
   unfold counter(x,v2);
 
-  var res: Bool := CAS(x.c, v1, new_v1);
+  var res: Bool := cas(x.c, v1, new_v1);
 
   {! 
     if (res) {
@@ -54,4 +54,4 @@ proc read(x: Ref, implicit ghost v: Int)
   commitAU(phi, v1);
 
   return v1;
-}
+}

test/ci/back-end/atomic_spec/treiber_stack_atomics.rav

@@ -44,7 +44,7 @@ proc push(s: Ref, x: Int, implicit ghost xs: IntList)
   unfold is_stack(s, xs1);
   hd1 :| is_list(hd1, xs1) && own(s, head, hd1, 1.0);
 
-  var res : Bool := CAS(s.head, hd, s0);
+  var res : Bool := cas(s.head, hd, s0);
 
   {!
     if (res) {
@@ -126,7 +126,7 @@ proc pop(s: Ref, implicit ghost xs: IntList)
   unfold is_stack(s, xs1);
   hd1 :| is_list(hd1, xs1) && own(s, head, hd1, 1.0);
 
-  var res : Bool := CAS(s.head, hd, hd_next);
+  var res : Bool := cas(s.head, hd, hd_next);
 
   {!
     if (res) {
@@ -156,4 +156,4 @@ proc pop(s: Ref, implicit ghost xs: IntList)
 
     return ret;
   }
-}
+}

test/ci/back-end/iterated-star/array-max.rav

@@ -22,7 +22,7 @@ module ArrayMax[M: IArray] {
     forall j: Int :: 0 <= j < M.len(a) ==> own(M.loc(a, j), value, m[j], 1.0)
   }
 
-  var x: Int := 4
+  val x: Int := 4
 
   pred is_max(i: Int, m: Map[Int, Int], u: Int) {
     forall j: Int :: 0 <= j && j < u ==> m[j] <= m[i]

test/ci/front-end/cas_rewriter_test.rav

@@ -14,10 +14,10 @@ proc p(x:Ref)
 {
   // x.f := 0;
   unfold my_inv(x);
-  ghost var b : Bool := CAS(x.f, 0, 5);
-  // var b1 : Bool := CAS(g(x).f, 0, 5);
+  ghost var b : Bool := cas(x.f, 0, 5);
+  // var b1 : Bool := cas(g(x).f, 0, 5);
   // var b: Int := g(x).f;
   // var b1: Int := x.f;
   fold my_inv(x);
   // assert (b == true);
-}
+}

test/ci/front-end/datatype_test.rav

@@ -10,10 +10,10 @@ module M {
   module M1 = Library.Frac[N1]
   module M2 = Library.Frac[N2]
 
-  var x : Int
-  var y : M2.T = M2.frac_chunk(x, 0.75)
+  val x : Int = 3
+  val y : M2.T = M2.frac_chunk(x, 0.75)
 
   proc p() {
     var y : M2.T = M2.frac_chunk(x, 0.75);
   }
-}
+}

test/ci/front-end/map_compr.rav

@@ -1,6 +1,6 @@
 field f: Int
 
-var y: Bool
+val y: Bool = true
 
 proc p() {
 

test/concurrent/treiber_stack/treiber_stack_atomics.rav

@@ -128,10 +128,10 @@ module Stack[T: Type] {
       return none;
     }
 
-    var top_next: Ref := top.next;
-    var top_value: T := top.value;
+    val top_next: Ref := top.next;
+    val top_value: T := top.value;
 
-    var xs1: TList := openAU(phi);
+    ghost val xs1: TList := openAU(phi);
 
     ghost val top1: Ref;
     unfold is_stack(s, xs1);
@@ -154,8 +154,8 @@ module Stack[T: Type] {
     if (res) {
       return some(top_value);
     } else { 
-      ghost var xs2: TList := openAU(phi);
-      var ret: TOption := pop(s);
+      ghost val xs2: TList := openAU(phi);
+      val ret: TOption := pop(s);
       commitAU(phi, ret);
 
       return ret;

test/linked-lists/list.rav

@@ -17,7 +17,7 @@ module List {
       assert y == z ? true : own(y, next, z, 1.0) && lseg(z, z);
       fold lseg(y, z);
     } else {
-      val xnext: Ref := x.next;
+      val xnext: Ref = x.next;
       append_tail(xnext, y, z);
       assert x == z ? true : own(x, next, xnext, 1.0) && lseg(xnext, z);
       fold lseg(x, z);
@@ -34,7 +34,7 @@ module List {
       invariant lseg(x, curr) && lseg(curr, null)
     {
       unfold lseg(curr, null);
-      ghost var old_curr: Ref = curr;
+      ghost val old_curr: Ref := curr;
       curr := curr.next;
       append_tail(x, old_curr, curr);
     }