From 3d8b6f135db233006f6628d47e83dbf3b0ca6ec7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 28 Sep 2024 13:44:48 +0200 Subject: [PATCH] More annotations for precondition errors for builtin functions --- src/nagini_translation/resources/bool.sil | 2 +- src/nagini_translation/resources/float.sil | 4 ++-- src/nagini_translation/resources/float_ieee32.sil | 4 ++-- src/nagini_translation/resources/float_real.sil | 8 ++++---- src/nagini_translation/resources/list.sil | 4 ++-- src/nagini_translation/resources/seq.sil | 4 ++-- src/nagini_translation/resources/tuple.sil | 7 ++++--- 7 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index afbd15ba..31e3894a 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -130,7 +130,7 @@ function int___mul__(self: Int, other: Int): Int function int___floordiv__(self: Int, other: Int): Int decreases _ - requires other != 0 + requires @error("Divisor may be zero.")(other != 0) { self \ other } diff --git a/src/nagini_translation/resources/float.sil b/src/nagini_translation/resources/float.sil index 03091d69..8cb75623 100644 --- a/src/nagini_translation/resources/float.sil +++ b/src/nagini_translation/resources/float.sil @@ -101,7 +101,7 @@ function float___truediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) - requires issubtype(typeof(other), int()) ==> int___unbox__(other) != 0 + requires @error("Divisor may be zero.")(issubtype(typeof(other), int()) ==> @error("Divisor may be zero.")(int___unbox__(other) != 0)) requires issubtype(typeof(other), int()) // cannot express non-zero at the moment ensures issubtype(typeof(result), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> @@ -123,7 +123,7 @@ function float___rtruediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) - requires issubtype(typeof(self), int()) ==> int___unbox__(self) != 0 + requires @error("Divisor may be zero.")(issubtype(typeof(self), int()) ==> @error("Divisor may be zero.")(int___unbox__(self) != 0)) requires issubtype(typeof(self), int()) // cannot express non-zero at the moment ensures issubtype(typeof(result), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> diff --git a/src/nagini_translation/resources/float_ieee32.sil b/src/nagini_translation/resources/float_ieee32.sil index cb9cf479..30b67530 100644 --- a/src/nagini_translation/resources/float_ieee32.sil +++ b/src/nagini_translation/resources/float_ieee32.sil @@ -99,7 +99,7 @@ function float___truediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) - requires float___unbox__(other) != ___float32_zero() + requires @error("Divisor may be zero.")(float___unbox__(other) != ___float32_zero()) ensures issubtype(typeof(result), float()) ensures result == __prim__perm___box__(___float32_div(float___unbox__(self), float___unbox__(other))) @@ -119,7 +119,7 @@ function float___rtruediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) - requires float___unbox__(self) != ___float32_zero() + requires @error("Divisor may be zero.")(float___unbox__(self) != ___float32_zero()) ensures issubtype(typeof(result), float()) ensures result == __prim__perm___box__(___float32_div(float___unbox__(other), float___unbox__(self))) diff --git a/src/nagini_translation/resources/float_real.sil b/src/nagini_translation/resources/float_real.sil index 596be318..33148854 100644 --- a/src/nagini_translation/resources/float_real.sil +++ b/src/nagini_translation/resources/float_real.sil @@ -330,8 +330,8 @@ function float___truediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) - requires float___is_nan__(other) == false && float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==> - float___unbox__(other) != 0 / 1 + requires @error("Divisor may be zero.")(float___is_nan__(other) == false && float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==> + @error("Divisor may be zero.")(float___unbox__(other) != 0 / 1)) ensures issubtype(typeof(result), float()) ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==> result == float___box_nan() @@ -366,8 +366,8 @@ function float___rtruediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) - requires float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==> - float___unbox__(self) != 0 / 1 + requires @error("Divisor may be zero.")(float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==> + @error("Divisor may be zero.")(float___unbox__(self) != 0 / 1)) ensures issubtype(typeof(result), float()) ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==> result == float___box_nan() diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil index beea33c6..92692b5e 100644 --- a/src/nagini_translation/resources/list.sil +++ b/src/nagini_translation/resources/list.sil @@ -75,8 +75,8 @@ method list___getitem_slice__(self: Ref, key: Ref) returns (_res: Ref) method list___setitem__(self: Ref, key: Int, item: Ref) returns () requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) requires acc(self.list_acc) - requires key >= 0 - requires key < list___len__(self) + requires @error("List index may be negative.")(key >= 0) + requires @error("List index may be out of bounds.")(key < list___len__(self)) requires issubtype(typeof(item), list_arg(typeof(self), 0)) ensures acc(self.list_acc) ensures self.list_acc == old(self.list_acc)[key := item] diff --git a/src/nagini_translation/resources/seq.sil b/src/nagini_translation/resources/seq.sil index d430c764..38e1fd88 100644 --- a/src/nagini_translation/resources/seq.sil +++ b/src/nagini_translation/resources/seq.sil @@ -24,8 +24,8 @@ function PSeq___getitem__(self: Ref, index: Ref): Ref decreases _ requires issubtype(typeof(self), PSeq(PSeq_arg(typeof(self), 0))) requires issubtype(typeof(index), int()) - requires let ln == (PSeq___len__(self)) in - ((int___unbox__(index) < 0 ==> int___unbox__(index) >= -ln) && (int___unbox__(index) >= 0 ==> int___unbox__(index) < ln)) + requires @error("Index may be out of bounds.")(let ln == (PSeq___len__(self)) in + @error("Index may be out of bounds.")((int___unbox__(index) < 0 ==> int___unbox__(index) >= -ln) && (int___unbox__(index) >= 0 ==> int___unbox__(index) < ln))) ensures result == (int___unbox__(index) >= 0 ? PSeq___sil_seq__(self)[int___unbox__(index)] : PSeq___sil_seq__(self)[PSeq___len__(self) + int___unbox__(index)]) ensures issubtype(typeof(result), PSeq_arg(typeof(self), 0)) diff --git a/src/nagini_translation/resources/tuple.sil b/src/nagini_translation/resources/tuple.sil index 0e91f742..a9c6010b 100644 --- a/src/nagini_translation/resources/tuple.sil +++ b/src/nagini_translation/resources/tuple.sil @@ -105,7 +105,8 @@ function tuple___len__(self: Ref): Int function tuple___getitem__(self: Ref, key: Int): Ref decreases _ - requires let ln == (tuple___len__(self)) in ((key >= 0 ==> key < ln) && (key < 0 ==> key >= -ln)) + requires @error("Tuple index may be out of bounds.")(let ln == (tuple___len__(self)) in + @error("Tuple index may be out of bounds.")((key >= 0 ==> key < ln) && (key < 0 ==> key >= -ln))) ensures key >= 0 ==> issubtype(typeof(result), tuple_arg(typeof(self), key)) ensures key < 0 ==> issubtype(typeof(result), tuple_arg(typeof(self), tuple___len__(self) + key)) ensures key >= 0 ==> result == tuple___val__(self)[key] @@ -114,8 +115,8 @@ function tuple___getitem__(self: Ref, key: Int): Ref function tuple___getitem_slice__(self: Ref, key: Ref): Ref decreases _ requires issubtype(typeof(key), slice()) - requires (slice___start__(key, tuple___len__(self)) >= 0 && slice___start__(key, tuple___len__(self)) <= tuple___len__(self)) - requires (slice___stop__(key, tuple___len__(self)) >= 0 && slice___stop__(key, tuple___len__(self)) <= tuple___len__(self)) + requires @error("Slice start may be out of bounds.")(slice___start__(key, tuple___len__(self)) >= 0 && slice___start__(key, tuple___len__(self)) <= tuple___len__(self)) + requires @error("Slice end index may be out of bounds.")(slice___stop__(key, tuple___len__(self)) >= 0 && slice___stop__(key, tuple___len__(self)) <= tuple___len__(self)) ensures typeof(result) == tuple(tuple_args(typeof(self))[slice___start__(key, tuple___len__(self))..slice___stop__(key, tuple___len__(self))]) ensures forall i: Int :: {tuple_arg(typeof(result), i)} (i >= 0 && i < (slice___stop__(key, tuple___len__(self)) - slice___start__(key, tuple___len__(self)))) ==> tuple_arg(typeof(result), i) == tuple_arg(typeof(self), i + slice___start__(key, tuple___len__(self))) ensures tuple___len__(result) == (slice___stop__(key, tuple___len__(self)) - slice___start__(key, tuple___len__(self)))