From 33f21dba5b8d31ce41c300e5ad67d345cd4c5234 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 11 Mar 2024 16:48:55 +0100
Subject: [PATCH] Better error messages for built-in functions (using Viper
 annotations)

---
 src/nagini_translation/lib/errors/wrappers.py   | 5 ++++-
 src/nagini_translation/resources/bool.sil       | 4 ++--
 src/nagini_translation/resources/list.sil       | 3 ++-
 src/nagini_translation/resources/preamble.index | 4 ++--
 src/nagini_translation/resources/set_dict.sil   | 2 +-
 5 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/nagini_translation/lib/errors/wrappers.py b/src/nagini_translation/lib/errors/wrappers.py
index 12398012..d9c74713 100644
--- a/src/nagini_translation/lib/errors/wrappers.py
+++ b/src/nagini_translation/lib/errors/wrappers.py
@@ -84,7 +84,10 @@ def string(self, show_viper_reason: bool) -> str:
         """
         reason = self._reason_string or self._node
         if reason is None and self.identifier in VAGUE_REASONS:
-            if not show_viper_reason:
+            if (self.offending_node.info().getClass().getSimpleName() == "AnnotationInfo" and
+                    self.offending_node.info().values().contains("error")):
+                return self.offending_node.info().values().get("error").get().head()
+            elif not show_viper_reason:
                 return VAGUE_REASONS[self.identifier]
             else:
                 return self._reason.readableMessage()
diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
index 212db54e..f25a0444 100644
--- a/src/nagini_translation/resources/bool.sil
+++ b/src/nagini_translation/resources/bool.sil
@@ -119,7 +119,7 @@ function int___floordiv__(self: Int, other: Int): Int
 
 function int___div__(self: Int, other: Int): Ref
     decreases _
-    requires other != 0
+    requires @error("Divisor may be zero.")(other != 0)
     ensures (self % other == 0) ==> (typeof(result) == int() && int___unbox__(result) == self \ other)
     ensures (self % other != 0) ==> typeof(result) == float()
 
@@ -161,7 +161,7 @@ function Place___eq__(self: Ref, other: Ref): Bool
 
 function object___cast__(typ: PyType, obj: Ref): Ref
     decreases _
-    requires issubtype(typeof(obj), typ)
+    requires @error("Cast may not succeed.")issubtype(typeof(obj), typ)
     ensures result == obj
     ensures issubtype(typeof(obj), typ)
 
diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil
index 69d8cefa..beea33c6 100644
--- a/src/nagini_translation/resources/list.sil
+++ b/src/nagini_translation/resources/list.sil
@@ -55,7 +55,8 @@ function list___getitem__(self: Ref, key: Ref): Ref
     requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
     requires issubtype(typeof(key), int())
     requires acc(self.list_acc, wildcard)
-    requires let ln == (list___len__(self)) in ((int___unbox__(key) < 0 ==> int___unbox__(key) >= -ln) && (int___unbox__(key) >= 0 ==> int___unbox__(key) < ln))
+    requires @error("List index may be out of bounds.")(let ln == (list___len__(self)) in (int___unbox__(key) < 0 ==> int___unbox__(key) >= -ln))
+    requires @error("List index may be out of bounds.")(let ln == (list___len__(self)) in (int___unbox__(key) >= 0 ==> int___unbox__(key) < ln))
     ensures result == (int___unbox__(key) >= 0 ? self.list_acc[int___unbox__(key)] : self.list_acc[list___len__(self) + int___unbox__(key)])
     ensures issubtype(typeof(result), list_arg(typeof(self), 0))
 
diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
index 19fae0e3..65db3ca1 100644
--- a/src/nagini_translation/resources/preamble.index
+++ b/src/nagini_translation/resources/preamble.index
@@ -47,7 +47,7 @@
             "args": ["list", "__prim__int", "object"],
             "type": null,
             "MustTerminate": true,
-            "requires": ["__len__"]
+            "requires": ["__len__", "__getitem__"]
         },
         "__iter__": {
             "args": ["list"],
@@ -76,7 +76,7 @@
         "__getitem__": {
             "args": ["list", "int"],
             "type": "object",
-            "requires": ["__len__"]
+            "requires": ["__len__", "int___unbox__"]
         },
         "__contains__": {
             "args": ["list", "object"],
diff --git a/src/nagini_translation/resources/set_dict.sil b/src/nagini_translation/resources/set_dict.sil
index a6d6e3de..6c988654 100644
--- a/src/nagini_translation/resources/set_dict.sil
+++ b/src/nagini_translation/resources/set_dict.sil
@@ -134,7 +134,7 @@ function dict___getitem__(self: Ref, key: Ref) : Ref
     decreases _
     requires issubtype(typeof(self), dict(dict_arg(typeof(self), 0), dict_arg(typeof(self), 1)))
     requires acc(self.dict_acc, wildcard)
-    requires dict___contains__(self, key)
+    requires @error("Key might not be present in dictionary.")dict___contains__(self, key)
     ensures issubtype(typeof(result), dict_arg(typeof(self), 1))
     ensures result == self.dict_acc[key]