CN: Re-add label consistency check

PR #797 split out the consistency and welltyped checks for a few
constructs, but accidentally removed the consistency checks for labels.
This commit adds them back.

This commit also deletes some code which was made redundant by aba34a0,
but was not deleted in that commit.

backend/cn/lib/check.ml

@@ -2669,6 +2669,11 @@ let time_check_c_functions (global_var_constraints, (checked : c_function list))
       global.fun_decls
       (return ())
   in
+  let@ () =
+    ListM.iterM
+      (fun (_, (loc, args_and_body)) -> WellTyped.WProc.consistent loc args_and_body)
+      checked
+  in
   let@ errors = check_c_functions checked in
   Cerb_debug.end_csv_timing "type checking functions";
   return errors

backend/cn/lib/wellTyped.ml

@@ -2319,16 +2319,7 @@ module BaseTyping = struct
 end
 
 module WLabel = struct
-  open Mucore
-
   let typ l = WArgs.typ (fun _body -> False.False) l
-
-  let consistent (loc : Loc.t) (lt : _ expr arguments) : unit m =
-    WArgs.consistent (fun _loc _body -> return ()) "loop/label" loc lt
-
-
-  let welltyped (loc : Loc.t) (lt : _ expr arguments) : _ expr arguments m =
-    WArgs.welltyped (fun _loc body -> return body) "loop/label" loc lt
 end
 
 module WProc = struct
@@ -2363,17 +2354,6 @@ module WProc = struct
     WArgs.consistent
       (fun loc (_body, labels, rt) ->
         let@ () = pure_and_no_initial_resources loc (WRT.consistent loc rt) in
-        let@ () =
-          PmapM.iterM
-            (fun _sym def ->
-              match def with
-              | Return _ -> return ()
-              | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) ->
-                pure_and_no_initial_resources
-                  loc
-                  (WLabel.consistent loc label_args_and_body))
-            labels
-        in
         PmapM.iterM
           (fun _sym def ->
             match def with
@@ -2397,21 +2377,6 @@ module WProc = struct
     WArgs.welltyped
       (fun loc (body, labels, rt) ->
         let@ rt = pure_and_no_initial_resources loc (WRT.welltyped loc rt) in
-        let@ labels =
-          PmapM.mapM
-            (fun _sym def ->
-              match def with
-              | Return loc -> return (Return loc)
-              | Label (loc, label_args_and_body, annots, parsed_spec, loop_info) ->
-                let@ label_args_and_body =
-                  pure_and_no_initial_resources
-                    loc
-                    (WLabel.welltyped loc label_args_and_body)
-                in
-                return (Label (loc, label_args_and_body, annots, parsed_spec, loop_info)))
-            labels
-            Sym.compare
-        in
         let label_context = label_context rt labels in
         let@ labels =
           PmapM.mapM

tests/cn/memcpy.c.verify

@@ -17,12 +17,6 @@ tests/cn/memcpy.c:17:16: warning: 'each' expects a 'u64', but 'j' with type 'i32
 tests/cn/memcpy.c:19:16: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
           take srcInv = each (i32 j; 0i32 <= j && j < n)
                ^
-tests/cn/memcpy.c:17:16: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
-  /*@ inv take dstInv = each (i32 j; 0i32 <= j && j < n)
-               ^
-tests/cn/memcpy.c:19:16: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
-          take srcInv = each (i32 j; 0i32 <= j && j < n)
-               ^
 tests/cn/memcpy.c:28:30: warning: 'extract' expects a 'u64', but '(i32)read_&i0' with type 'i32' was provided. This will become an error in the future.
     /*@ extract Owned<char>, (i32)i; @*/
                              ^~~~~~