From 0bb93bf2adb99ba357f86b5d7ead1b55ca340e3a Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc-mak@users.noreply.github.com>
Date: Sat, 28 Dec 2024 23:15:43 +0000
Subject: [PATCH] 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     |  5 +++++
 backend/cn/lib/wellTyped.ml | 35 -----------------------------------
 tests/cn/memcpy.c.verify    |  6 ------
 3 files changed, 5 insertions(+), 41 deletions(-)

diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
index 6ad4c8778..14051f148 100644
--- a/backend/cn/lib/check.ml
+++ b/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
diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml
index 981ade6b8..4a0940003 100644
--- a/backend/cn/lib/wellTyped.ml
+++ b/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
diff --git a/tests/cn/memcpy.c.verify b/tests/cn/memcpy.c.verify
index 5208f19ec..c354d7b31 100644
--- a/tests/cn/memcpy.c.verify
+++ b/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; @*/
                              ^~~~~~