From 6791a6c6b67784feb5f8f3b28ebcd08ead22eef9 Mon Sep 17 00:00:00 2001
From: Zain K Aamer <ZippeyKeys12@gmail.com>
Date: Thu, 19 Dec 2024 17:41:16 -0500
Subject: [PATCH] [CN-Exec] Give more info for `Predicate not found` (#775)

Also make a distinct message for `Alloc`
---
 backend/cn/lib/cn_internal_to_ail.ml | 52 ++++++++++++++++++++++++++--
 1 file changed, 49 insertions(+), 3 deletions(-)

diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml
index 7498064a5..9aec367f4 100644
--- a/backend/cn/lib/cn_internal_to_ail.ml
+++ b/backend/cn/lib/cn_internal_to_ail.ml
@@ -2548,18 +2548,41 @@ let cn_to_ail_resource_internal
   dts
   globals
   (preds : (Sym.t * Def.Predicate.t) list)
-  _loc
+  loc
   =
   let calculate_return_type = function
     | Request.Owned (sct, _) ->
       ( Sctypes.to_ctype sct,
         BT.of_sct Memory.is_signed_integer_type Memory.size_of_integer_type sct )
     | PName pname ->
+      if Sym.equal pname Alloc.Predicate.sym then (
+        Cerb_colour.with_colour
+          (fun () ->
+            print_endline
+              Pp.(
+                plain
+                  (Pp.item
+                     "'Alloc' not currently supported at runtime"
+                     (!^"Used at" ^^^ Locations.pp loc))))
+          ();
+        exit 2);
       let matching_preds =
         List.filter (fun (pred_sym', _def) -> Sym.equal pname pred_sym') preds
       in
       let pred_sym', pred_def' =
-        match matching_preds with [] -> failwith "Predicate not found" | p :: _ -> p
+        match matching_preds with
+        | [] ->
+          Cerb_colour.with_colour
+            (fun () ->
+              print_endline
+                Pp.(
+                  plain
+                    (Pp.item
+                       "Predicate not found"
+                       (Sym.pp pname ^^^ !^"at" ^^^ Locations.pp loc))))
+            ();
+          exit 2
+        | p :: _ -> p
       in
       let cn_bt = bt_to_cn_base_type pred_def'.oarg_bt in
       let ctype =
@@ -3509,11 +3532,34 @@ let cn_to_ail_assume_resource_internal
       ( Sctypes.to_ctype sct,
         BT.of_sct Memory.is_signed_integer_type Memory.size_of_integer_type sct )
     | PName pname ->
+      if Sym.equal pname Alloc.Predicate.sym then (
+        Cerb_colour.with_colour
+          (fun () ->
+            print_endline
+              Pp.(
+                plain
+                  (Pp.item
+                     "'Alloc' not currently supported at runtime"
+                     (!^"Used at" ^^^ Locations.pp loc))))
+          ();
+        exit 2);
       let matching_preds =
         List.filter (fun (pred_sym', _def) -> Sym.equal pname pred_sym') preds
       in
       let pred_sym', pred_def' =
-        match matching_preds with [] -> failwith "Predicate not found" | p :: _ -> p
+        match matching_preds with
+        | [] ->
+          Cerb_colour.with_colour
+            (fun () ->
+              print_endline
+                Pp.(
+                  plain
+                    (Pp.item
+                       "Predicate not found"
+                       (Sym.pp pname ^^^ !^"at" ^^^ Locations.pp loc))))
+            ();
+          exit 2
+        | p :: _ -> p
       in
       let cn_bt = bt_to_cn_base_type pred_def'.oarg_bt in
       let ctype =