From 230a582261dbfe478f6a7989f63bf3999b7d8796 Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Fri, 22 Mar 2024 12:56:46 +0000 Subject: [PATCH 1/6] Add additional legal magic methods to whitelist Include additional whitelisted names for magic dunderscore functions as needed for external project. --- src/nagini_translation/lib/constants.py | 28 ++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/nagini_translation/lib/constants.py b/src/nagini_translation/lib/constants.py index 2c0315bd..fe4de51f 100644 --- a/src/nagini_translation/lib/constants.py +++ b/src/nagini_translation/lib/constants.py @@ -214,17 +214,43 @@ '__ge__', '__lt__', '__le__', + '__add__', - '__sub_', + '__sub__', '__mul__', + '__truediv__', '__floordiv__', '__mod__', + '__divmod__', + '__pow__', + '__lshift__', + '__rshift__', + '__and__', + '__or__', + '__xor__', + + '__radd__', + '__rsub__', + '__rmul__', + '__rmatmul__', + '__rtruediv__', + '__rfloordiv__', + '__rmod__', + '__rdivmod__', + '__rpow__(self,', + '__rlshift__', + '__rrshift__', + '__rand__', + '__rxor__', + '__ror__', + '__init__', '__enter__', '__exit__', '__str__', '__len__', '__bool__', + '__getitem__', '__setitem__', } From 3d39cfd8ac21677068cb98ca80ef34b05355f080 Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Mon, 25 Mar 2024 12:08:23 +0000 Subject: [PATCH 2/6] Modify integer comparison functions to support float operand --- src/nagini_translation/resources/bool.sil | 32 ++++++++++++++----- .../resources/preamble.index | 20 +++++++----- 2 files changed, 36 insertions(+), 16 deletions(-) diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index f25a0444..0c60fee4 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -68,28 +68,44 @@ function bool___eq__(self: Ref, other: Ref): Bool ensures result == object___eq__(self, other) -function int___ge__(self: Int, other: Int): Bool +function int___ge__(self: Ref, other: Ref): Bool decreases _ + requires issubtype(typeof(self), int()) + requires issubtype(typeof(other), float()) { - self >= other + issubtype(typeof(other), int()) + ? int___unbox__(self) >= int___unbox__(other) + : float___ge__(self, other) } -function int___gt__(self: Int, other: Int): Bool +function int___gt__(self: Ref, other: Ref): Bool decreases _ + requires issubtype(typeof(self), int()) + requires issubtype(typeof(other), float()) { - self > other + issubtype(typeof(other), int()) + ? int___unbox__(self) >= int___unbox__(other) + : float___gt__(self, other) } -function int___le__(self: Int, other: Int): Bool +function int___le__(self: Ref, other: Ref): Bool decreases _ + requires issubtype(typeof(self), int()) + requires issubtype(typeof(other), float()) { - self <= other + issubtype(typeof(other), int()) + ? int___unbox__(self) >= int___unbox__(other) + : float___le__(self, other) } -function int___lt__(self: Int, other: Int): Bool +function int___lt__(self: Ref, other: Ref): Bool decreases _ + requires issubtype(typeof(self), int()) + requires issubtype(typeof(other), float()) { - self < other + issubtype(typeof(other), int()) + ? int___unbox__(self) >= int___unbox__(other) + : float___lt__(self, other) } function int___add__(self: Int, other: Int): Int diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index index 65db3ca1..33414dab 100644 --- a/src/nagini_translation/resources/preamble.index +++ b/src/nagini_translation/resources/preamble.index @@ -254,20 +254,24 @@ "type": "__prim__int" }, "__ge__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": [] }, "__gt__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": [] }, "__lt__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": [] }, "__le__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": [] }, "__int__": { "args": ["int"], From c7c3f775daa9a34684f54af7770786997dc84c70 Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Mon, 25 Mar 2024 13:56:07 +0100 Subject: [PATCH 3/6] Fixing some typos and ommitions in bool.sil and preamble.index --- src/nagini_translation/lib/constants.py | 2 +- src/nagini_translation/resources/bool.sil | 6 +++--- src/nagini_translation/resources/preamble.index | 8 ++++---- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/nagini_translation/lib/constants.py b/src/nagini_translation/lib/constants.py index fe4de51f..dcf186af 100644 --- a/src/nagini_translation/lib/constants.py +++ b/src/nagini_translation/lib/constants.py @@ -237,7 +237,7 @@ '__rfloordiv__', '__rmod__', '__rdivmod__', - '__rpow__(self,', + '__rpow__', '__rlshift__', '__rrshift__', '__rand__', diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index 0c60fee4..741a4bd0 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -84,7 +84,7 @@ function int___gt__(self: Ref, other: Ref): Bool requires issubtype(typeof(other), float()) { issubtype(typeof(other), int()) - ? int___unbox__(self) >= int___unbox__(other) + ? int___unbox__(self) > int___unbox__(other) : float___gt__(self, other) } @@ -94,7 +94,7 @@ function int___le__(self: Ref, other: Ref): Bool requires issubtype(typeof(other), float()) { issubtype(typeof(other), int()) - ? int___unbox__(self) >= int___unbox__(other) + ? int___unbox__(self) <= int___unbox__(other) : float___le__(self, other) } @@ -104,7 +104,7 @@ function int___lt__(self: Ref, other: Ref): Bool requires issubtype(typeof(other), float()) { issubtype(typeof(other), int()) - ? int___unbox__(self) >= int___unbox__(other) + ? int___unbox__(self) < int___unbox__(other) : float___lt__(self, other) } diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index index 33414dab..5569bda4 100644 --- a/src/nagini_translation/resources/preamble.index +++ b/src/nagini_translation/resources/preamble.index @@ -256,22 +256,22 @@ "__ge__": { "args": ["int", "float"], "type": "__prim__bool", - "requires": [] + "requires": ["int___unbox__", "float___ge__"] }, "__gt__": { "args": ["int", "float"], "type": "__prim__bool", - "requires": [] + "requires": ["int___unbox__", "float___gt__"] }, "__lt__": { "args": ["int", "float"], "type": "__prim__bool", - "requires": [] + "requires": ["int___unbox__", "float___lt__"] }, "__le__": { "args": ["int", "float"], "type": "__prim__bool", - "requires": [] + "requires": ["int___unbox__", "float___le__"] }, "__int__": { "args": ["int"], From 2c0349b07506ae1bcfde20e783786eab2dc5adcd Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Tue, 26 Mar 2024 13:02:34 +0100 Subject: [PATCH 4/6] Fix type mismatch in uninterpreted float comparison functions Uninterpreted versions of float comparison functions refer to the respective integer comparisons if the operands are actually integers. The integer comparison functions expect their parameters to still be boxed types, so the float functions should not unbox the arguments. --- src/nagini_translation/resources/float.sil | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/nagini_translation/resources/float.sil b/src/nagini_translation/resources/float.sil index 309fb7c2..a6012d18 100644 --- a/src/nagini_translation/resources/float.sil +++ b/src/nagini_translation/resources/float.sil @@ -14,28 +14,28 @@ function float___ge__(self: Ref, other: Ref): Bool requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> - (result == int___ge__(int___unbox__(self), int___unbox__(other))) + (result == int___ge__(self, other)) function float___gt__(self: Ref, other: Ref): Bool decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> - (result == int___gt__(int___unbox__(self), int___unbox__(other))) + (result == int___gt__(self, other)) function float___le__(self: Ref, other: Ref): Bool decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> - (result == int___le__(int___unbox__(self), int___unbox__(other))) + (result == int___le__(self, other)) function float___lt__(self: Ref, other: Ref): Bool decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> - (result == int___lt__(int___unbox__(self), int___unbox__(other))) + (result == int___lt__(self, other)) function float___eq__(self: Ref, other: Ref): Bool decreases _ From 16a1d06e69a6e5a6377f498f4c0807c94bf1099f Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Tue, 26 Mar 2024 16:39:35 +0100 Subject: [PATCH 5/6] Mirror changes to int type definition into SIF mode preamble.index file --- .../sif/resources/preamble.index | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index index 4f8551d2..9bcc2026 100644 --- a/src/nagini_translation/sif/resources/preamble.index +++ b/src/nagini_translation/sif/resources/preamble.index @@ -257,20 +257,24 @@ "type": "__prim__int" }, "__ge__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": ["int___unbox__", "float___ge__"] }, "__gt__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": ["int___unbox__", "float___gt__"] }, "__lt__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": ["int___unbox__", "float___lt__"] }, "__le__": { - "args": ["__prim__int", "__prim__int"], - "type": "__prim__bool" + "args": ["int", "float"], + "type": "__prim__bool", + "requires": ["int___unbox__", "float___le__"] }, "__int__": { "args": ["int"], From 0acaad293a0440c6b9c055406849e5a796b004b9 Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Tue, 2 Apr 2024 10:50:41 +0200 Subject: [PATCH 6/6] Add float.sil to list of files included in SIF mode Since integer comparison functions reference the equivalent float versions of those functions, the definitions of the float type functions need to be included in the translation output in SIF mode too. The relevant file paths are added to the include list in the SIF mode version of all.sil --- src/nagini_translation/sif/resources/all.sil | 1 + 1 file changed, 1 insertion(+) diff --git a/src/nagini_translation/sif/resources/all.sil b/src/nagini_translation/sif/resources/all.sil index bfda3a22..3d9388b7 100644 --- a/src/nagini_translation/sif/resources/all.sil +++ b/src/nagini_translation/sif/resources/all.sil @@ -15,6 +15,7 @@ domain SIFDomain[T] { } import "../../resources/bool.sil" +import "../../resources/float.sil" import "references.sil" import "../../resources/bytes.sil" import "../../resources/iterator.sil"