diff --git a/contrib/nitcc/src/grammar.nit b/contrib/nitcc/src/grammar.nit index feb4498790..c5c5b951aa 100644 --- a/contrib/nitcc/src/grammar.nit +++ b/contrib/nitcc/src/grammar.nit @@ -115,6 +115,7 @@ class Gram p.alts.add_all(pool) end end + self.prods = self.prods.clone for p in prods do self.prods.remove(p) self.ast_prods.add(p) diff --git a/examples/circular_list.nit b/examples/circular_list.nit index 41d2e05e68..fb27df4506 100644 --- a/examples/circular_list.nit +++ b/examples/circular_list.nit @@ -29,6 +29,15 @@ class CircularList[E] redef fun first do return self.node.item + redef fun [](index) do + var i = 0 + for item in self do + if i == index then return item + i += 1 + end + return null + end + redef fun push(e) do var new_node = new CLNode[E](e) diff --git a/lib/core/collection/abstract_collection.nit b/lib/core/collection/abstract_collection.nit index 9e2179b444..c3130e3afa 100644 --- a/lib/core/collection/abstract_collection.nit +++ b/lib/core/collection/abstract_collection.nit @@ -64,7 +64,12 @@ interface Collection[E] # # assert [1,2,3].is_empty == false # assert [1..1[.is_empty == true - fun is_empty: Bool do return length == 0 + fun is_empty: Bool + is + ensure(result == (length == 0)) + do + return length == 0 + end # Alias for `not is_empty`. # @@ -72,7 +77,12 @@ interface Collection[E] # # assert [1,2,3].not_empty == true # assert [1..1[.not_empty == false - fun not_empty: Bool do return not self.is_empty + fun not_empty: Bool + is + ensure(result == (length != 0)) + do + return not self.is_empty + end # Number of items in the collection. # @@ -92,7 +102,12 @@ interface Collection[E] # assert [1,2,3].has(9) == false # assert [1..5[.has(2) == true # assert [1..5[.has(9) == false + # assert [3..3[.has(1) == false # empty collection + # + # ENSURE `is_empty implies result == false` fun has(item: nullable Object): Bool + is + ensure(is_empty implies not result) do for i in self do if i == item then return true return false @@ -110,6 +125,8 @@ interface Collection[E] # # ENSURE `is_empty implies result == true` fun has_only(item: nullable Object): Bool + is + ensure(is_empty implies result) do for i in self do if i != item then return false return true @@ -119,7 +136,10 @@ interface Collection[E] # Comparisons are done with == # # assert [10,20,10].count(10) == 2 + # ENSURE `is_empty implies result == 0` fun count(item: nullable Object): Int + is + ensure(is_empty implies result == 0) do var nb = 0 for i in self do if i == item then nb += 1 @@ -130,8 +150,9 @@ interface Collection[E] # # assert [1,2,3].first == 1 fun first: E + is + expect(not_empty) do - assert length > 0 return iterator.item end @@ -205,12 +226,12 @@ end # They are mainly used with collections and obtained from `Collection::iterator`. interface Iterator[E] # The current item. - # Require `is_ok`. - fun item: E is abstract + # EXPECT `is_ok`. + fun item: E is abstract, expect(is_ok) # Jump to the next item. - # Require `is_ok`. - fun next is abstract + # ENSURE `is_ok`. + fun next is abstract, expect(is_ok) # Jump to the next item `step` times. # @@ -233,10 +254,11 @@ interface Iterator[E] # If `step` is negative, this method aborts. # But specific subclasses can change this and do something more meaningful instead. # - # Require `is_ok` + # EXPECT `is_ok` fun next_by(step: Int) + is + expect(is_ok) do - assert step >= 0 while is_ok and step > 0 do next step -= 1 @@ -324,7 +346,7 @@ abstract class CachedIterator[E: Object] # The current item, if any. # If not, the cache is effectively filled (with `next_item`). - # Return `null` iff there is no more elements. + # Return `null` if there is no more elements. protected fun current_item: nullable E do var cache = self.cache @@ -403,7 +425,7 @@ interface RemovableCollection[E] # assert a.length == 0 # # ENSURE `is_empty` - fun clear is abstract + fun clear is abstract, ensure(is_empty) # Remove an occurrence of `item` # @@ -431,8 +453,8 @@ interface SimpleCollection[E] # assert a.has(3) == true # assert a.has(10) == false # - # Ensure col.has(item) - fun add(item: E) is abstract + # ENSURE self.has(item) + fun add(item: E) is abstract, ensure(self.has(item)) # Add each item of `coll`. # @@ -440,7 +462,13 @@ interface SimpleCollection[E] # a.add_all([3..5]) # assert a.has(4) == true # assert a.has(10) == false - fun add_all(coll: Collection[E]) do for i in coll do add(i) + # ENSURE `self.has_all(item)` + fun add_all(coll: Collection[E]) + is + ensure(self.has_all(coll)) + do + for i in coll do add(i) + end end # Abstract sets. @@ -608,7 +636,7 @@ interface MapRead[K, V] # assert x.is_empty == true # x["four"] = 4 # assert x.is_empty == false - fun is_empty: Bool is abstract + fun is_empty: Bool is abstract, ensure(result == (length == 0)) # Alias for `not is_empty`. # @@ -618,7 +646,12 @@ interface MapRead[K, V] # assert map.not_empty == false # map["one"] = 1 # assert map.not_empty == true - fun not_empty: Bool do return not self.is_empty + fun not_empty: Bool + is + ensure(result == (length != 0)) + do + return not self.is_empty + end # Number of items in the collection. # @@ -723,7 +756,7 @@ interface Map[K, V] # assert x["four"] == 40 # assert x.values.has(4) == false # - fun []=(key: K, value: V) is abstract + fun []=(key: K, value: V) is abstract, ensure(self[key] == value) # Add each (key,value) of `map` into `self`. # If a same key exists in `map` and `self`, then the value in self is discarded. @@ -758,7 +791,7 @@ interface Map[K, V] # assert x.keys.has("four") == false # # ENSURE `is_empty` - fun clear is abstract + fun clear is abstract, ensure(is_empty) redef fun values: RemovableCollection[V] is abstract @@ -768,16 +801,16 @@ end # Iterators for Map. interface MapIterator[K, V] # The current item. - # Require `is_ok`. - fun item: V is abstract + # ENSURE `is_ok`. + fun item: V is abstract, expect(is_ok) # The key of the current item. - # Require `is_ok`. - fun key: K is abstract + # EXPECT `is_ok`. + fun key: K is abstract, expect(is_ok) # Jump to the next item. - # Require `is_ok`. - fun next is abstract + # EXPECT `is_ok`. + fun next is abstract, expect(is_ok) # Is there a current item ? fun is_ok: Bool is abstract @@ -842,10 +875,9 @@ interface SequenceRead[E] # var a = [1,2,3] # assert a.first == 1 # - # REQUIRE `not is_empty` + # EXPECT `not_empty` redef fun first do - assert not_empty: not is_empty return self[0] end @@ -859,7 +891,7 @@ interface SequenceRead[E] # assert a[2] == 30 # # REQUIRE `index >= 0 and index < length` - fun [](index: Int): E is abstract + fun [](index: Int): E is abstract, expect(index >= 0 and index < length) # Return the index-th element but wrap # @@ -874,9 +906,15 @@ interface SequenceRead[E] # assert a.modulo(-10) == 30 # ~~~ # - # REQUIRE `not_empty` + # EXPECT `not_empty` # ENSURE `result == self[modulo_index(index)]` - fun modulo(index: Int): E do return self[modulo_index(index)] + fun modulo(index: Int): E + is + expect(not_empty) + ensure(result == self[modulo_index(index)]) + do + return self[modulo_index(index)] + end # Returns the real index for a modulo index. # @@ -888,8 +926,10 @@ interface SequenceRead[E] # assert a.modulo_index(-10) == 2 # ~~~ # - # REQUIRE `not_empty` + # EXPECT `not_empty` fun modulo_index(index: Int): Int + is + expect(not_empty) do var length = self.length if index >= 0 then @@ -935,10 +975,11 @@ interface SequenceRead[E] # var a = [1,2,3] # assert a.last == 3 # - # REQUIRE `not is_empty` + # EXPECT `not_empty` fun last: E + is + expect(not_empty) do - assert not_empty: not is_empty return self[length-1] end @@ -1082,7 +1123,11 @@ interface Sequence[E] # a.first = 10 # assert a == [10,2,3] fun first=(item: E) - do self[0] = item end + is + ensure(self.first == item) + do + self[0] = item + end # Set the last item. # Is equivalent with `self[length-1] = item`. @@ -1097,6 +1142,8 @@ interface Sequence[E] # b.last = 10 # assert b == [10] fun last=(item: E) + is + ensure(self[length-1] == item) do var l = length if l > 0 then @@ -1115,7 +1162,7 @@ interface Sequence[E] # a.push(10) # a.push(20) # assert a == [1,2,3,10,20] - fun push(e: E) is abstract + fun push(e: E) is abstract, ensure(self[length-1] == e) # Add each item of `coll` after the last. # @@ -1133,8 +1180,8 @@ interface Sequence[E] # assert a.pop == 2 # assert a == [1] # - # REQUIRE `not is_empty` - fun pop: E is abstract + # EXPECT `not_empty` + fun pop: E is abstract, expect(not_empty) # Add an item before the first one. # @@ -1142,7 +1189,7 @@ interface Sequence[E] # a.unshift(10) # a.unshift(20) # assert a == [20,10,1,2,3] - fun unshift(e: E) is abstract + fun unshift(e: E) is abstract, ensure(self.first == e) # Add all items of `coll` before the first one. # @@ -1161,8 +1208,8 @@ interface Sequence[E] # assert a.shift == 2 # assert a == [3] # - # REQUIRE `not is_empty` - fun shift: E is abstract + # EXPECT `not_empty` + fun shift: E is abstract, expect(not_empty) # Set the `item` at `index`. # @@ -1176,8 +1223,8 @@ interface Sequence[E] # a[3] = 400 # assert a == [10,200,30,400] # - # REQUIRE `index >= 0 and index <= length` - fun []=(index: Int, item: E) is abstract + # EXPECT `index >= 0 and index <= length` + fun []=(index: Int, item: E) is abstract, expect(index >= 0 and index <= length) # Set the index-th element but wrap # @@ -1193,9 +1240,15 @@ interface Sequence[E] # assert a == [100, 200, 301] # ~~~ # - # REQUIRE `not_empty` + # EXPECT `not_empty` # ENSURE `self[modulo_index(index)] == value` - fun modulo=(index: Int, value: E) do self[modulo_index(index)] = value + fun modulo=(index: Int, value: E) + is + expect(not_empty) + ensure(self[modulo_index(index)] == value) + do + self[modulo_index(index)] = value + end # Insert an element at a given position, following elements are shifted. # @@ -1203,9 +1256,9 @@ interface Sequence[E] # a.insert(100, 2) # assert a == [10, 20, 100, 30, 40] # - # REQUIRE `index >= 0 and index <= length` + # EXPECT `index >= 0 and index <= length` # ENSURE `self[index] == item` - fun insert(item: E, index: Int) is abstract + fun insert(item: E, index: Int) is abstract, expect(index >= 0 and index <= length), ensure(self[index] == item) # Insert all elements at a given position, following elements are shifted. # @@ -1213,11 +1266,13 @@ interface Sequence[E] # a.insert_all([100..102], 2) # assert a == [10, 20, 100, 101, 102, 30, 40] # - # REQUIRE `index >= 0 and index <= length` + # EXPECT `index >= 0 and index <= length` # ENSURE `self[index] == coll.first` fun insert_all(coll: Collection[E], index: Int) + is + expect(index >= 0 and index <= length) + ensure(self[index] == coll.first) do - assert index >= 0 and index < length if index == length then add_all(coll) end @@ -1233,8 +1288,8 @@ interface Sequence[E] # a.remove_at(1) # assert a == [10,30] # - # REQUIRE `index >= 0 and index < length` - fun remove_at(index: Int) is abstract + # EXPECT `index >= 0 and index < length` + fun remove_at(index: Int) is abstract, expect(index >= 0 and index < length) # Rotates the elements of self once to the left # diff --git a/lib/core/collection/array.nit b/lib/core/collection/array.nit index f01bbb5d68..702b50b35d 100644 --- a/lib/core/collection/array.nit +++ b/lib/core/collection/array.nit @@ -215,17 +215,17 @@ abstract class AbstractArray[E] redef fun push(item) do add(item) + # EXPECT `not_empty` redef fun pop do - assert not_empty: not is_empty var r = last _length -= 1 return r end + # EXPECT `not_empty` redef fun shift do - assert not_empty: not is_empty var r = first var l = length-1 copy_to(1, l, self, 0) @@ -318,15 +318,15 @@ class Array[E] super AbstractArray[E] super Cloneable + # EXPECT `index >= 0 and index <= length` redef fun [](index) do - assert index: index >= 0 and index < _length return _items.as(not null)[index] end + # EXPECT `index >= 0 and index <= length` redef fun []=(index, item) do - assert index: index >= 0 and index < _length + 1 if _capacity <= index then enlarge(index + 1) end @@ -432,8 +432,9 @@ class Array[E] # Create an empty array with a given capacity. init with_capacity(cap: Int) + is + expect(cap >= 0) do - assert positive: cap >= 0 _items = new NativeArray[E](cap) _capacity = cap _length = 0 @@ -441,8 +442,9 @@ class Array[E] # Create an array of `count` elements init filled_with(value: E, count: Int) + is + expect(count >= 0) do - assert positive: count >= 0 _items = new NativeArray[E](count) _capacity = count _length = count @@ -455,8 +457,9 @@ class Array[E] # Create a array filled with a given native array. init with_native(nat: NativeArray[E], size: Int) + is + expect(size >= 0) do - assert positive: size >= 0 _items = nat _capacity = size _length = size @@ -542,8 +545,9 @@ class Array[E] # assert a * 2 == [1,2,3,1,2,3] # assert (a * 10).length == 30 fun *(repeat: Int): Array[E] + is + expect(repeat >= 0) do - assert repeat >= 0 var res = new Array[E].with_capacity(length * repeat) while repeat > 0 do res.add_all(self) @@ -605,11 +609,8 @@ class ArraySet[E] redef fun length do return _array.length - redef fun first - do - assert _array.length > 0 - return _array.first - end + # EXPECT `not_empty` + redef fun first do return _array.first redef fun remove(item) do diff --git a/lib/core/collection/circular_array.nit b/lib/core/collection/circular_array.nit index 1cc757b4a0..4d0b38068b 100644 --- a/lib/core/collection/circular_array.nit +++ b/lib/core/collection/circular_array.nit @@ -65,10 +65,11 @@ class CircularArray[E] # # The method takes care of the initial gap and the possible wrapping. # - # REQUIRE: `0 <= index and index < length` + # EXPECT: `0 <= index and index < length` private fun offset(index: Int): Int + is + expect(0 <= index and index < length) do - assert index >= 0 var head = self._head var tail = self._tail var offset = head + index @@ -116,10 +117,9 @@ class CircularArray[E] super end + # EXPECT `not_empty` redef fun pop do - var l = length - 1 - assert l >= 0 - length = l + length = length - 1 var native = _native var t = tail @@ -145,10 +145,9 @@ class CircularArray[E] head = h end + # EXPECT `not_empty` redef fun shift do - var l = length - 1 - assert l >= 0 - length = l + length = length - 1 var native = _native var h = head @@ -197,7 +196,11 @@ class CircularArray[E] native = new_native end + # ENSURE `self[index] == item` redef fun insert(item, index) + is + expect(index >= 0) # Since this is a circular structure, the expected condition only need to be `index >= 0`. + ensure(self[index] == item) do # Special insertion at the end (is push) if index >= length then @@ -205,7 +208,6 @@ class CircularArray[E] push(item) return end - assert index >= 0 var new_len = length + 1 diff --git a/lib/core/collection/hash_collection.nit b/lib/core/collection/hash_collection.nit index 25cf2b9c7e..370274f0af 100644 --- a/lib/core/collection/hash_collection.nit +++ b/lib/core/collection/hash_collection.nit @@ -384,9 +384,9 @@ private class HashMapIterator[K, V] super MapIterator[K, V] redef fun is_ok do return _node != null + # EXPECT `is_ok`. redef fun item do - assert is_ok return _node._value end @@ -396,15 +396,15 @@ private class HashMapIterator[K, V] # _node.second = value #end + # EXPECT `is_ok`. redef fun key do - assert is_ok return _node._key end + # EXPECT `is_ok`. redef fun next do - assert is_ok _node = _node._next_item end @@ -433,9 +433,9 @@ class HashSet[E] redef fun is_empty do return _the_length == 0 + # EXPECT `not_empty` redef fun first do - assert _the_length > 0 return _first_item._key end @@ -486,15 +486,15 @@ private class HashSetIterator[E] super Iterator[E] redef fun is_ok do return _node != null + # EXPECT `is_ok` redef fun item do - assert is_ok return _node._key end + # EXPECT `is_ok` redef fun next do - assert is_ok _node = _node._next_item end diff --git a/lib/core/collection/list.nit b/lib/core/collection/list.nit index 241238b4d3..75bee7667a 100644 --- a/lib/core/collection/list.nit +++ b/lib/core/collection/list.nit @@ -70,9 +70,12 @@ class List[E] end # Return a list of elements between 'from' and 'to'. - fun slice(from: Int, to: Int): List[E] do - assert from >= 0 and from < length - assert to >= 0 and to < length and from <= to + # + # EXPECT: `from >= 0 and from < length and to >= 0 and to < length and from <= to` + fun slice(from: Int, to: Int): List[E] + is + expect(from >= 0 and from < length and to >= 0 and to < length and from <= to) + do var list = new List[E] while from <= to do list.add(self[from]) diff --git a/lib/core/collection/range.nit b/lib/core/collection/range.nit index 29fa17e7a4..c5a6b186a2 100644 --- a/lib/core/collection/range.nit +++ b/lib/core/collection/range.nit @@ -19,7 +19,26 @@ import abstract_collection class Range[E: Discrete] super Collection[E] - redef var first + # Representation of the first element + private var first_element: E + + # In introduction `first()` defines `expect(not_empty)` + # but in our case, the `first` method now represents the access to the `first_element` attribute. + # The expected contract is therefore no longer necessary this is why `expect(true)`. + redef fun first + is + expect(true) + do + return first_element + end + + # Set the first element `first_element` + fun first=(element :E) + is + ensure(first_element == element) + do + first_element = element + end # Get the last element. var last: E @@ -86,7 +105,7 @@ class Range[E: Discrete] # assert a == b # assert a.to_a == [10, 11, 12, 13, 14, 15] init(from: E, to: E) is old_style_init do - first = from + first_element = from last = to after = to.successor(1) end @@ -100,7 +119,7 @@ class Range[E: Discrete] # assert a.to_a == [10, 11, 12, 13, 14] init without_last(from: E, to: E) do - first = from + first_element = from if from <= to then last = to.predecessor(1) after = to diff --git a/lib/core/collection/union_find.nit b/lib/core/collection/union_find.nit index 864c5092a9..67d66287aa 100644 --- a/lib/core/collection/union_find.nit +++ b/lib/core/collection/union_find.nit @@ -86,10 +86,11 @@ class DisjointSet[E] var number_of_subsets: Int = 0 # Get the root node of an element - # require: `has(e)` + # EXPECT: `has(e)` private fun find(e:E): DisjointSetNode + is + expect(has(e)) do - assert nodes.has_key(e) var ne = nodes[e] if ne.parent == ne then return ne var res = nfind(ne) @@ -101,6 +102,8 @@ class DisjointSet[E] # Use *path compression* to flatten the structure # ENSURE: `result.parent == result` private fun nfind(ne: DisjointSetNode): DisjointSetNode + is + ensure(result.parent == result) do var nf = ne.parent if nf == ne then return ne @@ -126,7 +129,10 @@ class DisjointSet[E] # Initially it is in its own disjoint subset # # ENSURE: `has(e)` - redef fun add(e) do + redef fun add(e) + is + ensure(self.has(e)) + do if nodes.has_key(e) then return var ne = new DisjointSetNode nodes[e] = ne @@ -199,6 +205,8 @@ class DisjointSet[E] # Combine the subsets of `e` and `f` # ENSURE: `in_same_subset(e,f)` fun union(e,f:E) + is + ensure(in_same_subset(e,f)) do var ne = find(e) var nf = find(f) @@ -223,8 +231,10 @@ class DisjointSet[E] end # Combine the subsets of all elements of `es` - # ENSURE: `all_in_same_subset(cs)` + # ENSURE: `all_in_same_subset(es)` fun union_all(es:Collection[E]) + is + ensure(all_in_same_subset(es)) do if es.is_empty then return var f = es.first diff --git a/lib/pthreads/concurrent_collections.nit b/lib/pthreads/concurrent_collections.nit index a8b4bbc8b0..48bb15aeda 100644 --- a/lib/pthreads/concurrent_collections.nit +++ b/lib/pthreads/concurrent_collections.nit @@ -82,6 +82,8 @@ abstract class ConcurrentCollection[E] var mutex = new Mutex redef fun count(e) + is + no_contract do mutex.lock var r = real_collection.count(e) @@ -90,6 +92,8 @@ abstract class ConcurrentCollection[E] end redef fun first + is + no_contract do mutex.lock var r = real_collection.first @@ -98,6 +102,8 @@ abstract class ConcurrentCollection[E] end redef fun has(e) + is + no_contract do mutex.lock var r = real_collection.has(e) @@ -106,6 +112,8 @@ abstract class ConcurrentCollection[E] end redef fun has_all(e) + is + #no_contract do mutex.lock var r = real_collection.has_all(e) @@ -114,6 +122,8 @@ abstract class ConcurrentCollection[E] end redef fun has_only(e) + is + no_contract do mutex.lock var r = real_collection.has_only(e) @@ -122,6 +132,8 @@ abstract class ConcurrentCollection[E] end redef fun is_empty + is + no_contract do mutex.lock var r = real_collection.is_empty @@ -130,6 +142,8 @@ abstract class ConcurrentCollection[E] end redef fun iterator + is + #no_contract do mutex.lock var r = real_collection.iterator @@ -138,6 +152,8 @@ abstract class ConcurrentCollection[E] end redef fun length + is + #no_contract do mutex.lock var r = real_collection.length @@ -146,6 +162,8 @@ abstract class ConcurrentCollection[E] end redef fun to_a + is + #no_contract do mutex.lock var r = real_collection.to_a @@ -154,6 +172,8 @@ abstract class ConcurrentCollection[E] end redef fun rand + is + #no_contract do mutex.lock var r = real_collection.rand @@ -162,6 +182,8 @@ abstract class ConcurrentCollection[E] end redef fun join(sep, last_sep) + is + #no_contract do mutex.lock var r = real_collection.join(sep, last_sep) @@ -170,6 +192,8 @@ abstract class ConcurrentCollection[E] end redef fun to_s + is + #no_contract do mutex.lock var r = real_collection.to_s @@ -186,6 +210,8 @@ abstract class ConcurrentSequenceRead[E] redef type REAL: SequenceRead[E] redef fun ==(o) + is + #no_contract do mutex.lock var r = real_collection == o @@ -194,6 +220,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun [](index) + is + no_contract do mutex.lock var r = real_collection[index] @@ -202,6 +230,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun hash + is + #no_contract do mutex.lock var r = real_collection.hash @@ -210,6 +240,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun index_of(index) + is + #no_contract do mutex.lock var r = real_collection.index_of(index) @@ -218,6 +250,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun index_of_from(index, from) + is + #no_contract do mutex.lock var r = real_collection.index_of_from(index, from) @@ -226,6 +260,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun iterator_from(index) + is + #no_contract do mutex.lock var r = real_collection.iterator_from(index) @@ -234,6 +270,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun last + is + no_contract do mutex.lock var r = real_collection.last @@ -242,6 +280,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun last_index_of(e) + is + #no_contract do mutex.lock var r = real_collection.last_index_of(e) @@ -250,6 +290,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun last_index_of_from(e, from) + is + #no_contract do mutex.lock var r = real_collection.last_index_of_from(e, from) @@ -258,6 +300,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun reverse_iterator + is + #no_contract do mutex.lock var r = real_collection.reverse_iterator @@ -266,6 +310,8 @@ abstract class ConcurrentSequenceRead[E] end redef fun reverse_iterator_from(from) + is + #no_contract do mutex.lock var r = real_collection.reverse_iterator_from(from) @@ -282,6 +328,8 @@ abstract class ConcurrentSequence[E] redef type REAL: Sequence[E] redef fun []=(index, e) + is + no_contract do mutex.lock real_collection[index] = e @@ -289,6 +337,8 @@ abstract class ConcurrentSequence[E] end redef fun add(e) + is + no_contract do mutex.lock real_collection.add e @@ -296,6 +346,8 @@ abstract class ConcurrentSequence[E] end redef fun append(e) + is + #no_contract do mutex.lock real_collection.append e @@ -303,6 +355,8 @@ abstract class ConcurrentSequence[E] end redef fun first=(e) + is + no_contract do mutex.lock real_collection.first = e @@ -310,6 +364,8 @@ abstract class ConcurrentSequence[E] end redef fun insert(e, i) + is + no_contract do mutex.lock real_collection.insert(e, i) @@ -317,6 +373,8 @@ abstract class ConcurrentSequence[E] end redef fun insert_all(from, pos) + is + no_contract do mutex.lock real_collection @@ -324,6 +382,8 @@ abstract class ConcurrentSequence[E] end redef fun last=(e) + is + no_contract do mutex.lock real_collection.last = e @@ -331,6 +391,8 @@ abstract class ConcurrentSequence[E] end redef fun pop + is + no_contract do mutex.lock var r = real_collection.pop @@ -339,6 +401,8 @@ abstract class ConcurrentSequence[E] end redef fun prepend(e) + is + #no_contract do mutex.lock real_collection.prepend e @@ -346,6 +410,8 @@ abstract class ConcurrentSequence[E] end redef fun push(e) + is + no_contract do mutex.lock real_collection.push e @@ -353,6 +419,8 @@ abstract class ConcurrentSequence[E] end redef fun remove_at(index) + is + no_contract do mutex.lock real_collection.remove_at(index) @@ -360,6 +428,8 @@ abstract class ConcurrentSequence[E] end redef fun shift + is + no_contract do mutex.lock var r = real_collection.shift @@ -368,6 +438,8 @@ abstract class ConcurrentSequence[E] end redef fun unshift(e) + is + no_contract do mutex.lock real_collection.unshift(e) @@ -375,6 +447,8 @@ abstract class ConcurrentSequence[E] end redef fun subarray(start, len) + is + #no_contract do mutex.lock var r = real_collection.subarray(start, len) @@ -394,6 +468,8 @@ class ConcurrentArray[E] init do self.real_collection = new Array[E] redef fun clear + is + no_contract do mutex.lock real_collection.clear @@ -401,6 +477,8 @@ class ConcurrentArray[E] end redef fun enlarge(cap) + is + #no_contract do mutex.lock real_collection.enlarge(cap) @@ -408,6 +486,8 @@ class ConcurrentArray[E] end redef fun remove_all(e) + is + #no_contract do mutex.lock real_collection.remove_all(e) @@ -415,6 +495,8 @@ class ConcurrentArray[E] end redef fun swap_at(a, b) + is + #no_contract do mutex.lock real_collection.swap_at(a, b) @@ -422,6 +504,8 @@ class ConcurrentArray[E] end redef fun has(e) + is + no_contract do mutex.lock var result = real_collection.has(e) @@ -434,6 +518,8 @@ class ConcurrentArray[E] # redef fun add(e) + is + no_contract do mutex.lock real_collection.add e @@ -460,6 +546,8 @@ class ConcurrentList[E] init do self.real_collection = new List[E] redef fun link(l) + is + #no_contract do mutex.lock real_collection.link(l) @@ -467,6 +555,8 @@ class ConcurrentList[E] end redef fun slice(from, to) + is + no_contract do mutex.lock var r = real_collection.slice(from, to) @@ -479,6 +569,8 @@ class ConcurrentList[E] # redef fun pop + is + no_contract do mutex.lock var r = real_collection.pop @@ -487,6 +579,8 @@ class ConcurrentList[E] end redef fun is_empty + is + no_contract do mutex.lock var r = real_collection.is_empty @@ -495,6 +589,8 @@ class ConcurrentList[E] end redef fun unshift(e) + is + no_contract do mutex.lock real_collection.unshift(e) @@ -502,6 +598,8 @@ class ConcurrentList[E] end redef fun push(e) + is + no_contract do mutex.lock real_collection.push(e) @@ -509,6 +607,8 @@ class ConcurrentList[E] end redef fun shift + is + no_contract do mutex.lock var value = real_collection.shift @@ -525,14 +625,20 @@ class ReverseBlockingQueue[E] private var cond = new PthreadCond # Adding the signal to release eventual waiting thread(s) - redef fun push(e) do + redef fun push(e) + is + no_contract + do mutex.lock real_collection.push(e) mutex.unlock end # When the Queue is empty, signal any possible waiting thread - redef fun remove(e) do + redef fun remove(e) + is + #no_contract + do mutex.lock real_collection.remove(e) if real_collection.is_empty then cond.signal @@ -540,7 +646,10 @@ class ReverseBlockingQueue[E] end # Wait until the Queue is empty - redef fun is_empty do + redef fun is_empty + is + no_contract + do mutex.lock while not real_collection.is_empty do self.cond.wait(mutex) mutex.unlock @@ -558,7 +667,10 @@ class BlockingQueue[E] private var cond = new PthreadCond # Adding the signal to release eventual waiting thread(s) - redef fun push(e) do + redef fun push(e) + is + no_contract + do mutex.lock real_collection.push(e) self.cond.signal @@ -566,7 +678,10 @@ class BlockingQueue[E] mutex.unlock end - redef fun unshift(e) do + redef fun unshift(e) + is + no_contract + do mutex.lock real_collection.unshift(e) self.cond.signal @@ -574,7 +689,10 @@ class BlockingQueue[E] end # If empty, blocks until an item is inserted with `push` or `unshift` - redef fun shift do + redef fun shift + is + no_contract + do mutex.lock while real_collection.is_empty do self.cond.wait(mutex) var r = real_collection.shift @@ -582,7 +700,10 @@ class BlockingQueue[E] return r end - redef fun is_empty do + redef fun is_empty + is + no_contract + do mutex.lock var r = real_collection.is_empty mutex.unlock diff --git a/lib/pthreads/redef_collections.nit b/lib/pthreads/redef_collections.nit index 4893cb248a..75edad14fd 100644 --- a/lib/pthreads/redef_collections.nit +++ b/lib/pthreads/redef_collections.nit @@ -38,6 +38,8 @@ redef class Array var mutex = new Mutex redef fun add(e) + is + no_contract do mutex.lock super @@ -45,6 +47,8 @@ redef class Array end redef fun []=(index, e) + is + no_contract do mutex.lock super @@ -52,6 +56,8 @@ redef class Array end redef fun [](index) + is + no_contract do mutex.lock var r = super @@ -60,6 +66,8 @@ redef class Array end redef fun remove_at(index) + is + no_contract do mutex.lock super @@ -67,6 +75,8 @@ redef class Array end redef fun shift + is + no_contract do mutex.lock var r = super @@ -75,6 +85,8 @@ redef class Array end redef fun unshift(e) + is + no_contract do mutex.lock super @@ -82,6 +94,8 @@ redef class Array end redef fun insert_all(from, pos) + is + no_contract do mutex.lock super @@ -89,6 +103,8 @@ redef class Array end redef fun swap_at(a, b) + is + no_contract do mutex.lock super @@ -96,6 +112,8 @@ redef class Array end redef fun ==(o) + is + no_contract do mutex.lock var r = super @@ -104,6 +122,8 @@ redef class Array end redef fun enlarge(cap) + is + no_contract do mutex.lock super diff --git a/share/man/nitc.md b/share/man/nitc.md index 64d8c530d0..889b6ae40a 100644 --- a/share/man/nitc.md +++ b/share/man/nitc.md @@ -548,6 +548,30 @@ Option used to disable the contracts(ensures, expects) usage. ### `--full-contract` Option used to enables contracts (ensures, expects) on all classes. Warning this is an expensive option at runtime. +### `--all-ensure` +Enable all ensure usage (disable default contract strategy). + +### `--all-expect` +Enable all expect usage (disable default contract strategy). + +### `--all-invariant` +Enable all invariant usage (disable default contract strategy). + +### `--in-out-invariant` +Option used to enable `invariant` verification on entry and exit of a method. By default, invariants are only checked on exit. Note, that the contracts are not checked on a `self` call. + +### `--contract-metrics` +Display the number of contract evaluation for each contract type. + +### `--keep-old-instance` +Store the instance of `old` representation in the class and thus systematic instantiation. This option should not be used in a multi-threaded environment. + +### `--true-contract` +Replace all contracts condition by `true` expression. Only for benchmark. + +### `--only-lock-check-contract` +Only inject the evaluation lock state check. Only for benchmark. + # ENVIRONMENT VARIABLES ### `NIT_DIR` diff --git a/src/astbuilder.nit b/src/astbuilder.nit index 0b911c6d47..e2d9a0c90c 100644 --- a/src/astbuilder.nit +++ b/src/astbuilder.nit @@ -203,11 +203,11 @@ class ASTBuilder # Build a callsite to call the `mproperty` in the current method `caller_method`. # `is_self_call` indicate if the method caller is a property of `self` - fun create_callsite(modelbuilder: ModelBuilder, caller_property: APropdef, mproperty: MMethod, is_self_call: Bool): CallSite + fun create_callsite(modelbuilder: ModelBuilder, caller_property: APropdef, recvtype: MType, mproperty: MMethod, is_self_call: Bool): CallSite do # FIXME It's not the better solution to call `TypeVisitor` here to build a model entity, but some make need to have a callsite var type_visitor = new TypeVisitor(modelbuilder, caller_property.mpropdef.as(not null)) - var callsite = type_visitor.build_callsite_by_property(caller_property, mproperty.intro_mclassdef.bound_mtype, mproperty, is_self_call) + var callsite = type_visitor.build_callsite_by_property(caller_property, recvtype, mproperty, is_self_call) assert callsite != null return callsite end @@ -1051,7 +1051,10 @@ redef class ModelBuilder private fun get_mmethod(name: String, mclassdef: MClassDef, visibility: nullable MVisibility): MMethod do visibility = visibility or else public_visibility var mproperty = try_get_mproperty_by_name(null, mclassdef, name).as(nullable MMethod) - if mproperty == null then mproperty = new MMethod(mclassdef, name, mclassdef.location, visibility) + if mproperty == null then + mproperty = new MMethod(mclassdef, name, mclassdef.location, visibility) + mproperty.is_fictive = true + end return mproperty end @@ -1066,6 +1069,7 @@ redef class ModelBuilder # Take care, if `is_abstract == false` the AMethPropdef returned has an empty body (potential error if the given signature has an return type). fun create_method_from_property(mproperty: MMethod, mclassdef: MClassDef, is_abstract: Bool, msignature: nullable MSignature): AMethPropdef do var m_def = new MMethodDef(mclassdef, mproperty, mclassdef.location) + m_def.is_fictive = true if msignature == null then msignature = new MSignature(new Array[MParameter]) @@ -1088,7 +1092,10 @@ redef class ModelBuilder fun create_attribute_from_name(name: String, mclassdef: MClassDef, mtype: MType, visibility: nullable MVisibility): AAttrPropdef do if visibility == null then visibility = public_visibility var mattribute = try_get_mproperty_by_name(null, mclassdef, name) - if mattribute == null then mattribute = new MAttribute(mclassdef, name, mclassdef.location, visibility) + if mattribute == null then + mattribute = new MAttribute(mclassdef, name, mclassdef.location, visibility) + mattribute.is_fictive = true + end return create_attribute_from_property(mattribute.as(MAttribute), mclassdef, mtype) end @@ -1096,6 +1103,7 @@ redef class ModelBuilder # See `create_attribute_from_propdef` for more information. fun create_attribute_from_property(mattribute: MAttribute, mclassdef: MClassDef, mtype: MType): AAttrPropdef do var attribut_def = new MAttributeDef(mclassdef, mattribute, mclassdef.location) + attribut_def.is_fictive = true attribut_def.static_mtype = mtype return create_attribute_from_propdef(attribut_def) end @@ -1128,7 +1136,10 @@ redef class ModelBuilder fun create_class_from_name(name: String, super_type: Array[MClassType], mmodule: MModule, visibility: nullable MVisibility): AStdClassdef do if visibility == null then visibility = public_visibility var mclass = try_get_mclass_by_name(null, mmodule, name) - if mclass == null then mclass = new MClass(mmodule, name, mmodule.location, new Array[String], concrete_kind, visibility) + if mclass == null then + mclass = new MClass(mmodule, name, mmodule.location, new Array[String], concrete_kind, visibility) + mclass.is_fictive = true + end return create_class_from_mclass(mclass, super_type, mmodule) end @@ -1137,6 +1148,7 @@ redef class ModelBuilder # See `create_class_from_mclassdef` for more information. fun create_class_from_mclass(mclass: MClass, super_type: Array[MClassType], mmodule: MModule): AStdClassdef do var mclassdef = new MClassDef(mmodule, mclass.mclass_type, mmodule.location) + mclassdef.is_fictive = true mclassdef.set_supertypes(super_type) mclassdef.add_in_hierarchy diff --git a/src/compiler/abstract_compiler.nit b/src/compiler/abstract_compiler.nit index e10be397b8..14e8b75d29 100644 --- a/src/compiler/abstract_compiler.nit +++ b/src/compiler/abstract_compiler.nit @@ -803,6 +803,9 @@ abstract class AbstractCompiler self.header.add_decl("extern int glob_argc;") self.header.add_decl("extern char **glob_argv;") self.header.add_decl("extern val *glob_sys;") + + # Global fonction used by the contract infrastructure + self.header.add_decl("extern int *getInAssertion(); // Used to know if we are currently checking some assertions.") end # Stack stocking environment for longjumps @@ -942,6 +945,28 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref ); } return data; } + + static pthread_key_t in_assertion_key; + static pthread_once_t in_assertion_key_created = PTHREAD_ONCE_INIT; + + static void create_in_assertion() + { + pthread_key_create(&in_assertion_key, NULL); + } + + //Flag used to know if we are currently checking some assertions. + int *getInAssertion() + { + pthread_once(&in_assertion_key_created, &create_in_assertion); + int* in_assertion = pthread_getspecific(in_assertion_key); + if (in_assertion == NULL) { + in_assertion = malloc(sizeof(int)); + *in_assertion = 0; + pthread_setspecific(in_assertion_key, in_assertion); + } + return in_assertion; + } + #else // Use __thread when available __thread struct catch_stack_t catchStack = {-1, 0, NULL}; @@ -950,6 +975,12 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref ); { return &catchStack; } + + __thread int in_assertion = 0; // Flag used to know if we are currently checking some assertions. + + int *getInAssertion(){ + return &in_assertion; + } #endif """ @@ -1029,6 +1060,16 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref ); v.add_decl("exit(status);") v.add_decl("\}") + if modelbuilder.toolcontext.opt_contract_metrics.value then + v.compiler.header.add_decl("extern long count_executed_precondition_contracts; // Count the number of executed precondition") + v.compiler.header.add_decl("extern long count_executed_postcondition; // Count the number of executed postcondition") + v.compiler.header.add_decl("extern long count_executed_invariant; // Count the number of executed invariant") + + v.add_decl("long count_executed_precondition_contracts= 0; // Count the number of executed contract") + v.add_decl("long count_executed_postcondition= 0; // Count the number of executed contract") + v.add_decl("long count_executed_invariant= 0; // Count the number of executed contract") + end + compile_before_main(v) if no_main then @@ -1107,6 +1148,13 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref ); v.add("printf(\"inlined: %ld (%.2f%%)\\n\", count_invoke_by_inline, 100.0*count_invoke_by_inline/count_invoke_total);") end + if modelbuilder.toolcontext.opt_contract_metrics.value then + v.add("printf(\"# dynamic contract checked: total %ld\\n\", (count_executed_invariant + count_executed_precondition_contracts + count_executed_postcondition));") + v.add("printf(\"# dynamic invariant checked: total %ld\\n\", count_executed_invariant);") + v.add("printf(\"# dynamic precondition checked: total %ld\\n\", count_executed_precondition_contracts);") + v.add("printf(\"# dynamic postcondition checked: total %ld\\n\", count_executed_postcondition);") + end + if self.modelbuilder.toolcontext.opt_isset_checks_metrics.value then v.add("printf(\"# dynamic attribute reads: %ld\\n\", count_attr_reads);") v.add("printf(\"# dynamic isset checks: %ld\\n\", count_isset_checks);") @@ -1346,12 +1394,15 @@ abstract class AbstractCompilerVisitor # Force to get the primitive property named `name` in the instance `recv` or abort fun get_property(name: String, recv: MType): MMethod + is + expect(recv isa MClassType) do - assert recv isa MClassType - return self.compiler.modelbuilder.force_get_primitive_method(self.current_node, name, recv.mclass, self.compiler.mainmodule) + return self.compiler.modelbuilder.force_get_primitive_method(self.current_node, name, recv.as(MClassType).mclass, self.compiler.mainmodule) end fun compile_callsite(callsite: CallSite, arguments: Array[RuntimeVariable]): nullable RuntimeVariable + is + ensure(callsite.is_broken implies result == null) do if callsite.is_broken then return null return self.send(callsite.mproperty, arguments) @@ -1514,18 +1565,20 @@ abstract class AbstractCompilerVisitor # Generate a monomorphic send for the method `m`, the type `t` and the arguments `args` fun monomorphic_send(m: MMethod, t: MType, args: Array[RuntimeVariable]): nullable RuntimeVariable + is + expect(t isa MClassType) do - assert t isa MClassType var propdef = m.lookup_first_definition(self.compiler.mainmodule, t) - return self.call(propdef, t, args) + return self.call(propdef, t.as(MClassType), args) end # Generate a monomorphic super send from the method `m`, the type `t` and the arguments `args` fun monomorphic_super_send(m: MMethodDef, t: MType, args: Array[RuntimeVariable]): nullable RuntimeVariable + is + expect(t isa MClassType) do - assert t isa MClassType m = m.lookup_next_definition(self.compiler.mainmodule, t) - return self.call(m, t, args) + return self.call(m, t.as(MClassType), args) end # Attributes handling @@ -1585,13 +1638,14 @@ abstract class AbstractCompilerVisitor # Return an unique and stable identifier associated with an escapemark fun escapemark_name(e: nullable EscapeMark): String + is + expect(e != null) do - assert e != null if frame.escapemark_names.has_key(e) then return frame.escapemark_names[e] var name = e.name if name == null then name = "label" name = get_name(name) - frame.escapemark_names[e] = name + frame.escapemark_names[e.as(not null)] = name return name end @@ -2154,8 +2208,9 @@ abstract class AbstractRuntimeFunction # Fills the argument array inside v.frame.arguments, calling `resolve_ith_parameter` # for each parameter. private fun fill_parameters(v: VISITOR) + is + expect(v.frame != null) do - assert v.frame != null for i in [0..msignature.arity[ do var arg = resolve_ith_parameter(v, i) v.frame.arguments.add(arg) @@ -2179,8 +2234,9 @@ abstract class AbstractRuntimeFunction # e.g `RES f(T0 p0, T1 p1, ..., TN pN)` # Step 5 protected fun signature_to_c(v: VISITOR): String + is + expect(v.frame != null) do - assert v.frame != null var arguments = v.frame.arguments var comment = new FlatBuffer var selfvar = v.frame.selfvar @@ -2217,6 +2273,8 @@ abstract class AbstractRuntimeFunction # no curly brace. # Step 7 protected fun body_to_c(v: VISITOR) + is + expect(v.frame != null) do mmethoddef.compile_inside_to_c(v, v.frame.arguments) end @@ -2424,8 +2482,9 @@ class StaticFrame # Returns the first argument (the receiver) of a frame. # REQUIRE: arguments.length >= 1 fun selfvar: RuntimeVariable + is + expect(arguments.length >= 1) do - assert arguments.length >= 1 return arguments.first end end @@ -2443,7 +2502,12 @@ redef class MType # Is the associated C type a primitive one? # # ENSURE `result == (ctype != "val*")` - fun is_c_primitive: Bool do return false + fun is_c_primitive: Bool + is + ensure(result == (ctype != "val*")) + do + return false + end end redef class MClassType @@ -3858,6 +3922,19 @@ redef class AIfExpr end end +redef class AIfInAssertion + + redef fun stmt(v) + do + v.add("if (!*getInAssertion())\{") + if v.compiler.modelbuilder.toolcontext.opt_contract_metrics.value then v.add(mcontract.write_c_metric) + v.add("*getInAssertion() = 1;") + v.stmt(self.n_body) + v.add("*getInAssertion() = 0;") + v.add("\}") + end +end + redef class AIfexprExpr redef fun expr(v) do diff --git a/src/compiler/coloring.nit b/src/compiler/coloring.nit index 80f29ec254..724fcb29c5 100644 --- a/src/compiler/coloring.nit +++ b/src/compiler/coloring.nit @@ -182,30 +182,38 @@ class POSetColorer[E: Object] # All ids are strictly positive (`>= 1`). # # REQUIRE: is_colored - fun ids: Map[E, Int] do - assert is_colored + fun ids: Map[E, Int] + is + expect(is_colored) + do return ids_cache end private var ids_cache = new HashMap[E, Int] # Resulting colors # REQUIRE: is_colored - fun colors: Map[E, Int] do - assert is_colored + fun colors: Map[E, Int] + is + expect(is_colored) + do return colors_cache end private var colors_cache = new HashMap[E, Int] # REQUIRE: is_colored - fun poset: POSet[E] do - assert is_colored + fun poset: POSet[E] + is + expect(is_colored) + do return poset_cache end private var poset_cache: POSet[E] is noinit # REQUIRE: is_colored - fun conflicts: Map[E, Set[E]] do - assert is_colored + fun conflicts: Map[E, Set[E]] + is + expect(is_colored) + do return conflicts_cache end private var conflicts_cache: Map[E, Set[E]] is noinit diff --git a/src/compiler/compiler_ffi/compiler_ffi.nit b/src/compiler/compiler_ffi/compiler_ffi.nit index 7a536b152c..8cd9431781 100644 --- a/src/compiler/compiler_ffi/compiler_ffi.nit +++ b/src/compiler/compiler_ffi/compiler_ffi.nit @@ -82,9 +82,10 @@ end redef class MExplicitCall private fun compile_extern_callback(v: AbstractCompilerVisitor, ccu: CCompilationUnit, compile_implementation_too: Bool) + is + expect(mproperty isa MMethod) do - var mproperty = mproperty - assert mproperty isa MMethod + var mproperty = mproperty.as(MMethod) # In nitni files, declare internal function as extern var full_friendly_csignature = mproperty.build_csignature(recv_mtype, v.compiler.mainmodule, null, long_signature, internal_call_context) @@ -198,9 +199,10 @@ end redef class MExplicitSuper private fun compile_extern_callback(v: AbstractCompilerVisitor, ccu: CCompilationUnit, compile_implementation_too: Bool) + is + expect(from.mproperty isa MMethod) do - var mproperty = from.mproperty - assert mproperty isa MMethod + var mproperty = from.mproperty.as(MMethod) var mclass_type = from.mclassdef.mclass.mclass_type # In nitni files, declare internal function as extern diff --git a/src/compiler/global_compiler.nit b/src/compiler/global_compiler.nit index 737ec48f3a..3dca1db0f1 100644 --- a/src/compiler/global_compiler.nit +++ b/src/compiler/global_compiler.nit @@ -147,6 +147,8 @@ class GlobalCompiler # Return the C symbol associated to a live type runtime # REQUIRE: self.runtime_type_analysis.live_types.has(mtype) fun classid(mtype: MClassType): String + is + expect(self.runtime_type_analysis.live_types.has(mtype)) do if self.classids.has_key(mtype) then return self.classids[mtype] @@ -186,9 +188,10 @@ class GlobalCompiler # Declare C structures and identifiers for a runtime class fun declare_runtimeclass(mtype: MClassType) + is + expect(self.runtime_type_analysis.live_types.has(mtype)) do var v = self.header - assert self.runtime_type_analysis.live_types.has(mtype) v.add_decl("/* runtime class {mtype} */") var idnum = classids.length var idname = "ID_" + mtype.c_name @@ -243,9 +246,10 @@ class GlobalCompiler # Generate the init-instance of a live type (allocate + init-instance) fun generate_init_instance(mtype: MClassType) + is + expect(self.runtime_type_analysis.live_types.has(mtype)) + expect(not mtype.is_c_primitive) do - assert self.runtime_type_analysis.live_types.has(mtype) - assert not mtype.is_c_primitive var v = self.new_visitor var is_native_array = mtype.mclass.name == "NativeArray" @@ -297,8 +301,9 @@ class GlobalCompiler end fun generate_box_instance(mtype: MClassType) + is + expect(self.runtime_type_analysis.live_types.has(mtype)) do - assert self.runtime_type_analysis.live_types.has(mtype) var v = self.new_visitor self.header.add_decl("val* BOX_{mtype.c_name}({mtype.ctype});") diff --git a/src/compiler/java_compiler.nit b/src/compiler/java_compiler.nit index 7b83104ac6..301c5ab460 100644 --- a/src/compiler/java_compiler.nit +++ b/src/compiler/java_compiler.nit @@ -684,9 +684,11 @@ class JavaCompilerVisitor end # Generate a monomorphic send for the method `m`, the type `t` and the arguments `args` - fun monomorphic_send(m: MMethod, t: MType, args: Array[RuntimeVariable]): nullable RuntimeVariable do - assert t isa MClassType - var propdef = m.lookup_first_definition(self.compiler.mainmodule, t) + fun monomorphic_send(m: MMethod, t: MType, args: Array[RuntimeVariable]): nullable RuntimeVariable + is + expect(t isa MClassType) + do + var propdef = m.lookup_first_definition(self.compiler.mainmodule, t.as(MClassType)) return self.static_call(propdef, args) end @@ -760,9 +762,11 @@ class JavaCompilerVisitor end # Generate a return with `value` - fun ret(value: RuntimeVariable) do - var frame = self.frame - assert frame != null + fun ret(value: RuntimeVariable) + is + expect(frame != null) + do + var frame = self.frame.as(not null) var returnvar = frame.returnvar if returnvar != null then assign(returnvar, value) diff --git a/src/compiler/separate_compiler.nit b/src/compiler/separate_compiler.nit index 38bc466893..5b411d445c 100644 --- a/src/compiler/separate_compiler.nit +++ b/src/compiler/separate_compiler.nit @@ -720,8 +720,9 @@ class SeparateCompiler # Globaly compile the type structure of a live type fun compile_type_to_c(mtype: MType) + is + expect(not mtype.need_anchor) do - assert not mtype.need_anchor var is_live = mtype isa MClassType and runtime_type_analysis.live_types.has(mtype) var is_cast_live = runtime_type_analysis.live_cast_types.has(mtype) var c_name = mtype.c_name @@ -1386,8 +1387,9 @@ class SeparateCompilerVisitor # If the C expression is evaluated to 0, it means there is no tag. # Thus the expression can be used as a condition. fun extract_tag(value: RuntimeVariable): String + is + expect(not value.mtype.is_c_primitive) do - assert not value.mtype.is_c_primitive return "((long){value}&3)" # Get the two low bits end @@ -2351,8 +2353,10 @@ class SeparateCompilerVisitor end end - fun link_unresolved_type(mclassdef: MClassDef, mtype: MType) do - assert mtype.need_anchor + fun link_unresolved_type(mclassdef: MClassDef, mtype: MType) + is + expect(mtype.need_anchor) + do var compiler = self.compiler if not compiler.live_unresolved_types.has_key(self.frame.mpropdef.mclassdef) then compiler.live_unresolved_types[self.frame.mpropdef.mclassdef] = new HashSet[MType] diff --git a/src/contracts.nit b/src/contracts.nit index f7b81faf56..387896d48c 100644 --- a/src/contracts.nit +++ b/src/contracts.nit @@ -21,15 +21,53 @@ module contracts import parse_annotations import phase import semantize +import mclassdef_collect intrude import model_contract intrude import astbuilder intrude import modelize_property intrude import scope intrude import typing +intrude import model redef class ToolContext # Parses contracts annotations. var contracts_phase: Phase = new ContractsPhase(self, [modelize_property_phase,typing_phase]) + + # Option --no-contract + var opt_no_contract = new OptionBool("Disable the contracts usage", "--no-contract") + + # Option --full-contract + var opt_full_contract = new OptionBool("Enable all contracts usage", "--full-contract") + + # Option --in-out-invariant + var opt_in_out_invariant = new OptionBool("Enable invariant verification in enter and exit", "--in-out-invariant") + + # Option --contract-metrics + var opt_contract_metrics = new OptionBool("Enable dynamic count of contract checking", "--contract-metrics") + + # Option --keep-old-instance + var opt_old_attribute = new OptionBool("Enable the conservation of ensure `old` intance in a class attribute", "--keep-old-instance") + + # Option --all-ensure + var opt_all_ensure = new OptionBool("Enable all ensure usage (disable default contract strategy)", "--all-ensure") + + # Option --all-expect + var opt_all_expect = new OptionBool("Enable all expect usage (disable default contract strategy)", "--all-expect") + + # Option --all-invariant + var opt_all_invariant = new OptionBool("Enable all invariant usage (disable default contract strategy)", "--all-invariant") + + # Option --true-contract + var opt_true_contract = new OptionBool("Replace contract condition by `true` expression", "--true-contract") + + # Option --only-lock-check-contract + var opt_only_in_assertion_check = new OptionBool("Only inject the evaluation lock state check", "--only-lock-check-contract") + + redef init + do + super + option_context.add_option(opt_no_contract, opt_full_contract, opt_in_out_invariant, opt_contract_metrics, opt_old_attribute, opt_all_ensure, opt_all_expect, opt_all_invariant, opt_true_contract, opt_only_in_assertion_check) + end end private class ContractsPhase @@ -110,6 +148,9 @@ private class ContractsVisitor # Keep the `in_contract` attribute to avoid searching at each contrat var in_contract_attribute: nullable MAttribute = null + # Keep the invariant property to avoid searching at each invariant + var global_invariant: nullable MInvariant = null + redef fun visit(node) do node.create_contracts(self) @@ -121,8 +162,8 @@ private class ContractsVisitor fun define_signature(mcontract: MContract, nsignature: nullable ASignature, msignature: nullable MSignature) do if nsignature != null and msignature != null then nsignature.ret_type = msignature.return_mtype - self.n_signature = mcontract.adapt_nsignature(nsignature) - self.m_signature = mcontract.adapt_msignature(msignature) + self.n_signature = mcontract.adapt_nsignature(nsignature, self) + self.m_signature = mcontract.adapt_msignature(msignature, self) end # Define the new contract take in consideration that an old contract exist or not @@ -140,78 +181,41 @@ private class ContractsVisitor end end - # Inject the incontract attribute (`_in_contract_`) in the `Sys` class - # This attribute allows to check if the contract need to be executed - private fun inject_incontract_in_sys + # Return an `AIfAssertion` with the contract encapsulated by an `if` to check if it's already in a contract verification. + private fun encapsulated_contract_call(mcontract: MContract, call_to_contracts: Array[ACallExpr]): AIfInAssertion do - # If the `in_contract_attribute` already know just return - if in_contract_attribute != null then return - - var sys_class = toolcontext.modelbuilder.get_mclass_by_name(visited_module, mainmodule, "Sys") - - # Try to get the `in_contract` property, if it has already defined in a previously visited module. - var in_contract_property = toolcontext.modelbuilder.try_get_mproperty_by_name(visited_module, sys_class.intro, "__in_contract_") - if in_contract_property != null then - self.in_contract_attribute = in_contract_property.as(MAttribute) + var n_block = ast_builder.make_block + if not toolcontext.opt_only_in_assertion_check.value then n_block.add_all(call_to_contracts) + return new AIfInAssertion(mcontract, n_block) + end + # Inject the invariant method (`_invariant_`) verification in the root `Object` class + # By default the method is empty. + # Note the method is not abstract because the implementation of this method makes a super call to resolve multiple inheritance problem + private fun inject_invariant_in_object + do + # If the global_invariant already know just return + if global_invariant != null then return + # Get the object class from the modelbuilder + var object_class = toolcontext.modelbuilder.get_mclass_by_name(visited_module, mainmodule, "Object") + + # Try to get a global invariant if it's already defined in a previously visited module. + var invariant_property = toolcontext.modelbuilder.try_get_mproperty_by_name(visited_module, object_class.intro, "_invariant_") + if invariant_property != null then + global_invariant = invariant_property.as(MInvariant) return end - var bool_false = new AFalseExpr.make(mainmodule.bool_type) - var n_in_contract_attribute = toolcontext.modelbuilder.create_attribute_from_name("__in_contract_", sys_class.intro, mainmodule.bool_type, public_visibility).create_setter(toolcontext.modelbuilder, true).define_default(bool_false) + var m_invariant = new MInvariant(object_class.intro, "_invariant_", object_class.intro.location, public_visibility) + global_invariant = m_invariant - in_contract_attribute = n_in_contract_attribute.mpropdef.mproperty + toolcontext.modelbuilder.create_method_from_property(m_invariant, object_class.intro, false, new MSignature(new Array[MParameter])) end - - # Return the `_in_contract_` attribute. - # If the attribute `_in_contract_` does not exist it's injected with `inject_incontract_in_sys` - private fun get_incontract: MAttribute + # Return the invariant property `_invariant_` + # If the `_invariant_` does not exist it's injected this with `inject_invariant_in_object` + private fun get_global_invariant: MInvariant do - if self.in_contract_attribute == null then inject_incontract_in_sys - return in_contract_attribute.as(not null) - end - - # Return an `AIfExpr` with the contract encapsulated by an `if` to check if it's already in a contract verification. - # - # Example: - # ~~~nitish - # class A - # fun bar([...]) is except([...]) - # - # fun _contract_bar([...]) - # do - # if not sys._in_contract_ then - # sys._in_contract_ = true - # _bar_expect([...]) - # sys._in_contract_ = false - # end - # bar([...]) - # end - # - # fun _bar_expect([...]) - # end - # ~~~~ - # - private fun encapsulated_contract_call(visited_method: AMethPropdef, call_to_contracts: Array[ACallExpr]): AIfExpr - do - var sys_property = toolcontext.modelbuilder.model.get_mproperties_by_name("sys").first.as(MMethod) - var callsite_sys = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, sys_property, true) - - var incontract_attribute = get_incontract - - var callsite_get_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.getter.as(MMethod), false) - var callsite_set_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.setter.as(MMethod), false) - - var n_condition = ast_builder.make_not(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_get_incontract, null)) - - var n_if = ast_builder.make_if(n_condition, null) - - var if_then_block = n_if.n_then.as(ABlockExpr) - - if_then_block.add(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_set_incontract, [new ATrueExpr.make(mainmodule.bool_type)])) - if_then_block.add_all(call_to_contracts) - if_then_block.add(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_set_incontract, [new AFalseExpr.make(mainmodule.bool_type)])) - - return n_if + if self.global_invariant == null then inject_invariant_in_object + return global_invariant.as(not null) end end @@ -229,6 +233,7 @@ private class CallSiteVisitor redef fun visit(node) do + if node isa AAnnotation then return # Annotations don't need to be woven node.check_callsite(self) node.visit_all(self) end @@ -239,18 +244,100 @@ private class CallSiteVisitor private fun drive_callsite_to_contract(callsite: CallSite): CallSite do var contract_facet = callsite.mproperty.mcontract_facet + var invariant_facet = callsite.mproperty.minvariant_facet var visited_mpropdef = visited_propdef.mpropdef - if visited_mpropdef isa MContract or visited_mpropdef isa MFacet then return callsite + if visited_mpropdef.mproperty isa MContract or visited_mpropdef.mproperty isa MFacet then return callsite if visited_mpropdef == null or contract_facet == null then return callsite - return ast_builder.create_callsite(toolcontext.modelbuilder, visited_propdef, contract_facet, callsite.recv_is_self) + var facet: MFacet + if not callsite.recv_is_self and invariant_facet != null then + facet = invariant_facet + else + facet = contract_facet + end + + return ast_builder.create_callsite(toolcontext.modelbuilder, visited_propdef, callsite.recv, facet, callsite.recv_is_self) + end +end + +# Visitor to evaluate the expressions to detect the old usage in ensure. +private class OldVisitor + super Visitor + + # Actual visited mpropdef + var visited_mpropdef: MPropDef + + # The Instance of the actual contract visitor. + var contract_visitor: ContractsVisitor + + # Array of attributes to keep the old value. + var old_attributes = new HashMap[AExpr, nullable AAttrPropdef] + + redef fun visit(node) + do + node.check_old(self) + node.visit_all(self) + end + + # Create all old attributes and inject them into the given `mclassdef` + private fun build_old_attributes(mclassdef: MClassDef) + do + # Get the number of attributes in the given mclassdef. + # It will be used to define the name of the attribute. + var number_attributes = mclassdef.mclass.collect_intro_mattributes.length + + for old_expr, attribute in old_attributes do + + # Typing the old expression to assign the correct type to the attribute + old_expr.do_typing(contract_visitor.toolcontext.modelbuilder, visited_mpropdef) + if old_expr.mtype == null then continue # skip error. The generation of warning is not needed since the typing does it for us. + + var attribute_name = "_old_{number_attributes}" + + var resolved_mtype = old_expr.mtype.anchor_to(contract_visitor.visited_module.mmodule.as(not null), visited_mpropdef.mclassdef.bound_mtype).as_nullable + var n_attribute = contract_visitor.toolcontext.modelbuilder.create_attribute_from_name(attribute_name, mclassdef, resolved_mtype, public_visibility).create_setter(contract_visitor.toolcontext.modelbuilder, true) + n_attribute.noinit = true + + old_attributes[old_expr] = n_attribute + number_attributes += 1 + end + end + + # Switch old references captured during the visit with references to old attributes, generated by the `build_old_attributes` method. + # Example: + # ~~~nitish + # from: + # fun add_one(i: Int) is ensure(old(i) + 1 == i) + # to: + # fun add_one(i: Int) is ensure(old.i + 1 == i) + # ~~ + # + private fun switch_call_to_old_attribut(mensure: MEnsure, n_caller_propdef: APropdef) + do + for expr, n_attribut in old_attributes do + + # If this happens, the attribute was not generated due to a typing error. See `build_old_attributes` + if n_attribut == null then continue + + # Cast the old parameter because it's typed with object type + var object_type = contract_visitor.toolcontext.modelbuilder.get_mclass_by_name(contract_visitor.visited_module, contract_visitor.mainmodule, "Object").mclass_type + var n_old_var_param = contract_visitor.ast_builder.make_var(mensure.old_param, object_type) + + var n_old_cast = new AAsCastExpr.init_aascastexpr(n_old_var_param, new TKwas , null, mensure.old_mclass.mclass_type.create_ast_representation, null) + + var attid = new TAttrid + attid.text = "{n_attribut.mpropdef.mproperty.name}" + + expr.replace_with(new AAttrExpr.init_aattrexpr(n_old_cast, attid)) + end end end redef class ANode private fun create_contracts(v: ContractsVisitor) do end private fun check_callsite(v: CallSiteVisitor) do end + private fun check_old(v: OldVisitor) do end end redef class AAnnotation @@ -261,6 +348,12 @@ redef class AAnnotation # return this condition `(true and i == 10 and f >= 1.0)` private fun construct_condition(v : ContractsVisitor): AExpr do + if v.toolcontext.opt_true_contract.value then + var bool_true = new ATrueExpr.make(v.mainmodule.bool_type) + bool_true.location = self.location + return bool_true + end + var n_condition = n_args.first n_args.remove_at(0) for n_arg in n_args do n_condition = v.ast_builder.make_and(n_condition, n_arg) @@ -273,11 +366,14 @@ redef class MContract # Should contract be called? # return `true` if the contract needs to be called. - private fun is_called(v: ContractsVisitor, mpropdef: MPropDef): Bool + private fun is_called(v: ContractsVisitor, mclassdef: MClassDef): Bool do return v.toolcontext.opt_full_contract.value end + # Return the string that it represents the incrementation of contract invocation counter. + fun write_c_metric: String is abstract + # Method use to diplay warning when the contract is not present at the introduction private fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation])do end @@ -290,25 +386,25 @@ redef class MContract private fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef) is abstract # Create and return an adapted `MSignature` specifically for the contract in fonction of the given `m_signature` - private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_contract + private fun adapt_specific_msignature(m_signature: MSignature, visitor: ContractsVisitor): MSignature do return m_signature.adapt_to_contract # Create and return an adapted `ASignature` specifically for the contract in fonction of the given `n_signature` - private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_contract + private fun adapt_specific_nsignature(n_signature: ASignature, visitor: ContractsVisitor): ASignature do return n_signature.adapt_to_contract # Adapt the `m_signature` to the contract # If `m_signature == null` return a new `MSignature` else it calls a specific adapt method see `adapt_specific_msignature` - private fun adapt_msignature(m_signature: nullable MSignature): MSignature + private fun adapt_msignature(m_signature: nullable MSignature, visitor: ContractsVisitor): MSignature do if m_signature == null then return new MSignature(new Array[MParameter]) - return adapt_specific_msignature(m_signature) + return adapt_specific_msignature(m_signature, visitor) end # Adapt the `n_signature` to the contract # If `n_signature == null` return a new `ASignature` else it calls a specific adapt method see `adapt_specific_nsignature` - private fun adapt_nsignature(n_signature: nullable ASignature): ASignature + private fun adapt_nsignature(n_signature: nullable ASignature, visitor: ContractsVisitor): ASignature do if n_signature == null then return new ASignature - return adapt_specific_nsignature(n_signature) + return adapt_specific_nsignature(n_signature, visitor) end # Create the initial contract (intro) @@ -371,13 +467,19 @@ end redef class MExpect - redef fun is_called(v: ContractsVisitor, mpropdef: MPropDef): Bool + redef fun write_c_metric: String do return "count_executed_precondition_contracts++;" + + redef fun is_called(v: ContractsVisitor, mclassdef: MClassDef): Bool do + if super then return true + if v.toolcontext.opt_all_expect.value then return true + if v.toolcontext.opt_all_ensure.value or v.toolcontext.opt_all_invariant.value then return false + var main_package = v.mainmodule.mpackage - var actual_package = mpropdef.mclassdef.mmodule.mpackage + var actual_package = mclassdef.mmodule.mpackage if main_package != null and actual_package != null then var condition_direct_arc = v.toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package) - return super or main_package == actual_package or condition_direct_arc + return main_package == actual_package or condition_direct_arc end return false end @@ -428,13 +530,13 @@ redef class MExpect redef fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef) do - var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true) + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self.intro_mclassdef.bound_mtype, self, true) var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder) var n_callexpect = v.ast_builder.make_call(new ASelfExpr, callsite,args) # Creation of the new instruction block with the call to expect condition var actual_expr = n_mpropdef.n_block var new_block = new ABlockExpr - new_block.n_expr.push v.encapsulated_contract_call(n_mpropdef, [n_callexpect]) + new_block.n_expr.push v.encapsulated_contract_call(self, [n_callexpect]) if actual_expr isa ABlockExpr then new_block.n_expr.add_all(actual_expr.n_expr) else if actual_expr != null then @@ -447,11 +549,6 @@ end redef class BottomMContract - redef fun is_called(v: ContractsVisitor, mpropdef: MPropDef): Bool - do - return super or v.mainmodule.mpackage == mpropdef.mclassdef.mmodule.mpackage - end - redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr do # Define contract block @@ -508,23 +605,61 @@ end redef class MEnsure - redef fun adapt_specific_msignature(m_signature: MSignature): MSignature + redef fun is_called(v: ContractsVisitor, mclassdef: MClassDef): Bool do - return m_signature.adapt_to_ensurecondition + if super then return true + if v.toolcontext.opt_all_ensure.value then return true + if v.toolcontext.opt_all_expect.value or v.toolcontext.opt_all_invariant.value then return false + return v.mainmodule.mpackage == mclassdef.mmodule.mpackage end - redef fun adapt_specific_nsignature(n_signature: ASignature): ASignature + redef fun write_c_metric: String do return "count_executed_postcondition++;" + + redef fun adapt_specific_msignature(m_signature: MSignature, visitor: ContractsVisitor): MSignature do - return n_signature.adapt_to_ensurecondition + var msignature = m_signature.adapt_to_ensurecondition + + # Addition of a parameter to express `old` reference + var object_class = visitor.toolcontext.modelbuilder.get_mclass_by_name(visitor.visited_module, visitor.mainmodule, "Object") + + if object_class != null then + var object_mtype = object_class.mclass_type.as_nullable + # Addition of a parameter to express `old` reference + msignature.mparameters.add(new MParameter("old", object_mtype, false)) + end + + return msignature + end + + redef fun adapt_specific_nsignature(n_signature: ASignature, visitor: ContractsVisitor): ASignature + do + var nsignature = n_signature.adapt_to_ensurecondition + + # Addition of a parameter to express `old` reference + var object_class = visitor.toolcontext.modelbuilder.get_mclass_by_name(visitor.visited_module, visitor.mainmodule, "Object") + + if object_class != null then + old_param.declared_type = object_class.mclass_type.as_nullable + nsignature.n_params.add new AParam.make(self.old_param, object_class.mclass_type.as_nullable.create_ast_representation) + end + + return nsignature end redef fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef) do - var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true) + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self.intro_mclassdef.bound_mtype, self, true) var n_self = new ASelfExpr # argument to call the contract method var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder) + var n_read_old: nullable AVarExpr = null + + if self.old_mclass != null then + inject_old(v, n_mpropdef) + n_read_old = v.ast_builder.make_var_read(self.old_param, old_mclass.mclass_type) + end + var actual_block = n_mpropdef.n_block # never happen. If it's the case the problem is in the contract facet building assert actual_block isa ABlockExpr @@ -538,20 +673,384 @@ redef class MEnsure var return_expr = actual_block.n_expr.pop # Adding the read return to argument args.add(read_result) + if n_read_old != null then args.add(n_read_old) var n_call_contract = v.ast_builder.make_call(n_self, callsite, args) - actual_block.add_all([v.encapsulated_contract_call(n_mpropdef, [n_call_contract]), return_expr]) + actual_block.add_all([v.encapsulated_contract_call(self, [n_call_contract]), return_expr]) else + if n_read_old != null then args.add(n_read_old) # build the call to the contract method var n_call_contract = v.ast_builder.make_call(n_self, callsite, args) - actual_block.add v.encapsulated_contract_call(n_mpropdef, [n_call_contract]) + actual_block.add v.encapsulated_contract_call(self, [n_call_contract]) end + n_mpropdef.do_all(v.toolcontext) mfacet.has_applied_ensure = true end + + # Old attribute use to avoid new instantiation old class + var old_attribute: nullable MAttribute + + # Return an `TAttrid` corresponding to `old_attribute` + fun get_attid: TAttrid + is + expect(old_attribute != null) + do + var att_id = new TAttrid + att_id.text = "{old_attribute.name}" + return att_id + end + + # Inject the `old` variable into the `n_block` of the given `n_mpropdef`. + # + # The purpose of the variable is to capture the values of `old()` expr to use it in contracts. + # This variable will be injected at the start of the block (first instruction) + private fun inject_old(v: ContractsVisitor, n_mpropdef: AMethPropdef) + do + # Creation of a new block with as first expression the `old` variable and follow by all expr of the `n_mpropdef` body + var new_block = v.ast_builder.make_block + + # Create a new old_object to store the old expression value + var old_class_initdef = old_mclass.intro.default_init + var callsite_new_old_class = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, old_class_initdef.mproperty.intro_mclassdef.bound_mtype, old_class_initdef.mproperty, false) + var n_new_old_class = v.ast_builder.make_new(callsite_new_old_class, null) + n_new_old_class.n_type = old_mclass.mclass_type.create_ast_representation + + + if v.toolcontext.opt_old_attribute.value then + if old_attribute == null then + var oldclass_mtype = self.old_mclass.mclass_type.as_nullable + var attribute_name = "_old_{self.old_mclass.name}" + var mclassdef = n_mpropdef.mpropdef.mclassdef + var n_attribute = v.toolcontext.modelbuilder.create_attribute_from_name(attribute_name, mclassdef, oldclass_mtype, public_visibility).create_setter(v.toolcontext.modelbuilder, true) + n_attribute.noinit = true + old_attribute = n_attribute.mpropdef.mproperty + end + + var if_old_attribute = v.ast_builder.make_if(new AEqExpr.init_aeqexpr(new AAttrExpr.init_aattrexpr(new ASelfExpr, self.get_attid), new TEq, new ANullExpr.init_anullexpr( new TKwnull, null)), null) + if_old_attribute.n_then = new AAttrAssignExpr.init_aattrassignexpr(new ASelfExpr, self.get_attid, new TAssign, n_new_old_class) + + new_block.add if_old_attribute + end + + # Args to call the old init property + var n_args_call_init_property = new Array[AExpr] + n_args_call_init_property.add_all(n_mpropdef.n_signature.make_parameter_read(v.ast_builder)) + + if v.toolcontext.opt_old_attribute.value then + var n_old_cast = new AAsCastExpr.init_aascastexpr(new AAttrExpr.init_aattrexpr(new ASelfExpr, self.get_attid), new TKwas , null, self.old_mclass.mclass_type.create_ast_representation, null) + n_args_call_init_property.add(n_old_cast) + else + n_args_call_init_property.add(n_new_old_class) + end + + var callsite_old_class_init = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, old_mclass.init_old_property.intro_mclassdef.bound_mtype, old_mclass.init_old_property.as(not null), true) + var ncall_init_old = v.ast_builder.make_call(new ASelfExpr, callsite_old_class_init, n_args_call_init_property) + + new_block.add v.ast_builder.make_var_assign(self.old_param, ncall_init_old) + new_block.n_expr.add_all(n_mpropdef.n_block.as(ABlockExpr).n_expr) + n_mpropdef.n_block = new_block + end +end + +redef class MInvariant + super BottomMContract + + redef fun is_called(v: ContractsVisitor, mclassdef: MClassDef): Bool + do + if super then return true + if v.toolcontext.opt_all_invariant.value then return true + if v.toolcontext.opt_all_ensure.value or v.toolcontext.opt_all_expect.value then return false + return v.mainmodule.mpackage == mclassdef.mmodule.mpackage + end + + redef fun write_c_metric: String do return "count_executed_invariant++;" + + redef fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef) + do + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self.intro_mclassdef.bound_mtype, self, true) + var n_self = new ASelfExpr + # build the call to the contract method + var n_call = v.ast_builder.make_call(n_self, callsite, null) + var actual_block = n_mpropdef.n_block + # never happen. If it's the case the problem is in the contract facet building + assert actual_block isa ABlockExpr + + var new_block = v.ast_builder.make_block + + if v.toolcontext.opt_in_out_invariant.value and not n_mpropdef.mpropdef.mproperty.is_init then new_block.add v.encapsulated_contract_call(self, [n_call]) + + new_block.n_expr.add_all(actual_block.n_expr) + + n_mpropdef.n_block = new_block + + var ret_type = n_mpropdef.mpropdef.mproperty.intro.msignature.return_mtype + if ret_type != null then + # Inject the variable result (the injection of the result is necessary even if the invariants cannot take `result` as an argument) + # In this case the result variable is here to keep the return value of the original method. + # exemple + # ~~~nitish + # class A + # fun bar([...]): Bool is invariant([...]) + # + # fun _contract_bar([...]) + # do + # var result = bar([...]) + # # Check if the invariant check call is necessary and execute it. + # [...] + # return result + # end + # + # fun _bar_expect([...]) + # end + # ~~~~ + var result_var = inject_result(v, n_mpropdef, ret_type) + var return_expr = new_block.n_expr.pop + new_block.add_all([v.encapsulated_contract_call(self, [n_call]), return_expr]) + else + new_block.add(n_call) + end + end +end + +redef class MClass + + # Build the invariant verification property `_invariant` if is not exist and return it + private fun build_invariant(v: ContractsVisitor): MInvariant + do + var m_invariant = self.minvariant + if m_invariant != null then return m_invariant + # get a invariant property from the `ContractsVisitor` + m_invariant = v.get_global_invariant + self.minvariant = m_invariant + return m_invariant + end + + # Try to get the class definition `MClassDef` in the given `mmodule`. Return `null` if not exist. + fun try_get_mclassdef(mmodule: MModule): nullable MClassDef + do + for mclassdef in mclassdefs do + if mclassdef.mmodule == mmodule then return mclassdef + end + return null + end +end + +redef class MOldClass + + # Create a new method to init old parameter of the contract. + private fun build_old_init_methdef(v: OldVisitor, n_method: AMethPropdef) + do + var modelbuilder = v.contract_visitor.toolcontext.modelbuilder + var mpropdef = n_method.mpropdef + if mpropdef == null then abort + + var init_msignature = make_init_msignature(mpropdef.mproperty.intro.msignature.mparameters.to_a) + + var n_methdef = modelbuilder.create_method_from_name("_init_old_{mpropdef.name}", mpropdef.mclassdef, false, init_msignature, public_visibility) + + # This method is a little bit weird. But I need to do this because of the variables. + # Once the variable defines the scope will not redefine it so we will have to reuse the same, and i use a specific variable to + # TO-DO: One solution would be to keep the variable information in the msignature. + n_methdef.n_signature.n_params.last.variable = old_variable + + # FIXME set the location because the callsite creation need the node location + n_methdef.location = n_method.location + n_methdef.validate + + if self.init_old_property == null then + n_methdef.n_block = make_intro_block(v, n_methdef) + else + n_methdef.n_block = make_sub_block(v, n_methdef) + end + + n_methdef.do_all(v.contract_visitor.toolcontext) + self.init_old_property = n_methdef.mpropdef.mproperty + end + + # Create all old attribute assignments based on the OldVisitor `old_attributes` + private fun build_old_assignations(v: OldVisitor, n_method: AMethPropdef): Array[AExpr] + do + var ast_builder = v.contract_visitor.ast_builder + var array_assign = new Array[AExpr] + + for expr, n_attribut in v.old_attributes do + if n_attribut == null then continue # skip error + + var attid = new TAttrid + attid.text = "{n_attribut.mpropdef.mproperty.name}" + + array_assign.add new AAttrAssignExpr.init_aattrassignexpr(v.contract_visitor.ast_builder.make_var(self.old_variable, self.mclass_type), attid, new TAssign, expr) + end + return array_assign + end + + # Create a block with a new assignment of old attributes. + private fun make_intro_block(v: OldVisitor, n_method: AMethPropdef): ABlockExpr + do + var ast_builder = v.contract_visitor.ast_builder + var n_block = ast_builder.make_block + n_block.add_all(build_old_assignations(v, n_method)) + + var read_old_variable = v.contract_visitor.ast_builder.make_var(self.old_variable, self.mclass_type) + n_block.add(ast_builder.make_return(read_old_variable)) + + return n_block + end + + # Create a block with a call of super `init_old` and the new old attributes assignation. + private fun make_sub_block(v: OldVisitor, n_method: AMethPropdef): ABlockExpr + do + var ast_builder = v.contract_visitor.ast_builder + var super_call = ast_builder.make_super_call(n_method.n_signature.make_parameter_read(ast_builder)) + var assign_old_variable = v.contract_visitor.ast_builder.make_var_assign(self.old_variable, super_call) + var n_block = ast_builder.make_block + + n_block.add(assign_old_variable) + n_block.add_all(make_intro_block(v, n_method).n_expr.to_a) + + return n_block + end + + # Create new MSignature for the `init_old_property`. + # This signature is create with the given `MParameter` representing the argument of the method and with the add of a old parameter. + # + # Exemple : + # ~~~nitish + # fun add_i_to_a(i) is ensure (old(a) + i == a) + # + # fun init_old_add_i_to_a(i, old): OldClass + # ~~~ + private fun make_init_msignature(mparameters: Array[MParameter]): MSignature + do + var msignature = new MSignature(mparameters, self.mclass_type) + msignature.mparameters.add(new MParameter("old", self.mclass_type, false)) + msignature.return_mtype = self.mclass_type + return msignature + end +end + +redef class MClassDef + + # Is there an inherited invariant contract? + private fun has_inherited_invariant: Bool + do + var super_classes = self.in_hierarchy.direct_greaters + for super_class in super_classes do + if super_class.mclass.has_invariant then return true + end + return false + end +end + +redef class AClassdef + + # Entry point to create a contract (verification of inheritance, or new contract). + redef fun create_contracts(v) + do + if mclassdef == null then return + v.ast_builder.check_mmodule(mclassdef.mmodule) + v.current_location = self.location + # Invariants are always considered to be a redefinition of contract. + # This is due to an empty invariant method which is added to the root `object` class. + v.is_intro_contract = false + check_annotation(v) + if not mclass.has_invariant then check_redef(v) + end + + # Verification if the class has an inherited contract to apply it. + private fun check_redef(v: ContractsVisitor) + do + # Check if the method has an attached contract (Inherited) + if mclassdef.has_inherited_invariant then mclass.minvariant = v.global_invariant + end + + # Verification of the annotation to know if it is a contract annotation. + # If this is the case, we built the appropriate contract. + private fun check_annotation(v: ContractsVisitor) + do + var annotation_invariants = get_annotations("invariant") + var annotation_no_contract = get_annotations("no_contract") + + if not annotation_invariants.is_empty and not annotation_no_contract.is_empty then + v.toolcontext.error(location, "The new contract definition is not correct when using `no_contract`. Remove the `invariant` definition or the `no_contract`") + return + end + + if not annotation_no_contract.is_empty then + var minvariant = mclass.minvariant + if minvariant == null then + v.toolcontext.warning(location, "useless_nocontract", "Useless `no_contract`, no invariant was declared or inherited for `{mclass.name}`. Remove the `no_contract`") + else + # Add an empty invariant method to replace the actual definition + v.toolcontext.modelbuilder.create_method_from_property(minvariant, mclassdef.as(not null), false, minvariant.intro.msignature) + end + return + end + + if not annotation_invariants.is_empty then + + var minvariant = mclass.build_invariant(v) + + v.define_signature(minvariant, null, null) + v.build_contract(annotation_invariants, minvariant, mclassdef.as(not null)) + + add_invariant_in_super_def(v) + # Construct invariant facet for the `default_init` + mclassdef.default_init.mproperty.define_invariant_facet(v, mclassdef.as(not null), mclass.minvariant.as(not null)) + end + end + + # Create all contract facet for each inherited property definition of the class to take in consideration the invariant + # Redefine or introduced properties will be processed later + private fun add_invariant_in_super_def(v: ContractsVisitor) + do + var mpropertys = mclassdef.collect_inherited_mmethods(v.mainmodule, new ModelFilter) + for mproperty in mpropertys do + if mproperty isa MFacet or mproperty isa MContract or mproperty.has_invariant_facet then continue + + # All property defined in Object is considered as a pure property (without side effect) + # TO-DO add an option to manage it. Take care with `!=` and `==` on MNullableType you can't do a call to invariant facet because the object might be null. + if mproperty.intro.mclassdef.name == "Object" then continue + + # Check if the actual class definition redef this property definition. if it's the case do nothing the visit of the method will do the job + if mclassdef.mpropdefs_by_property.has_key(mproperty) then continue + + if mproperty.intro.is_intern then continue + # Do not generate invariant facet with inherited `defaultinit` + if not mproperty.name == "defaultinit" then mproperty.define_invariant_facet(v, mclassdef.as(not null), mclass.minvariant.as(not null)) + end + end end redef class MMethod + # Define invariant facet for the MMethod in the given mclassdef. + # This method also defines the contract facet. + private fun define_invariant_facet(v: ContractsVisitor, classdef: MClassDef, minvariant: MInvariant) + do + if not minvariant.is_called(v, classdef) then return + + # Do nothing the invariant facet already exist + if has_invariant_facet then return + + # Make a contract facet if it's not exist + if not self.has_contract_facet then define_contract_facet(v, classdef) + + # Make invariant mproperty facet + var invariant_facet = build_invariant_facet + + # Check if the MMethod has a invariant facet in the intro_mclassdef + if classdef != intro_mclassdef then + create_facet(v, intro_mclassdef, invariant_facet, self.mcontract_facet.as(not null)) + end + + # Create an ast definition for the invariant facet + var n_invariant_facet = create_facet(v, classdef, invariant_facet, self.mcontract_facet.as(not null)) + minvariant.adapt_method_to_contract(v, invariant_facet, n_invariant_facet) + n_invariant_facet.location = v.current_location + n_invariant_facet.do_all(v.toolcontext) + end + # Define contract facet for MMethod in the given mclassdef. The facet represents the entry point with contracts (expect, ensure) of the method. # If a contract is given adapt the contract facet. # @@ -587,7 +1086,9 @@ redef class MMethod if not exist_contract_facet then # If has no contract facet in intro just create it if classdef != intro_mclassdef then - create_facet(v, intro_mclassdef, contract_facet, self) + var n_intro_face = create_facet(v, intro_mclassdef, contract_facet, self) + n_intro_face.location = self.intro.location + n_intro_face.do_all(v.toolcontext) end n_contract_facet = create_facet(v, classdef, contract_facet, self) else @@ -598,17 +1099,9 @@ redef class MMethod else # create a new contract facet definition n_contract_facet = create_facet(v, classdef, contract_facet, self) - var block = v.ast_builder.make_block - # super call to the contract facet - var args = n_contract_facet.n_signature.make_parameter_read(v.ast_builder) - var n_super_call = v.ast_builder.make_super_call(args) - # verification for add a return or not - if self.intro.msignature.return_mtype != null then - block.add(v.ast_builder.make_return(n_super_call)) - else - block.add(n_super_call) - end - n_contract_facet.n_block = block + + if self.has_expect and self.mexpect != mcontract then mexpect.adapt_method_to_contract(v, contract_facet, n_contract_facet) + if self.has_ensure and self.mensure != mcontract then mensure.adapt_method_to_contract(v, contract_facet, n_contract_facet) end end if mcontract != null then mcontract.adapt_method_to_contract(v, contract_facet, n_contract_facet) @@ -639,7 +1132,7 @@ redef class MMethod var args: Array[AExpr] args = n_contractdef.n_signature.make_parameter_read(v.ast_builder) - var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_contractdef, called, true) + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_contractdef, called.intro_mclassdef.bound_mtype, called, true) var n_call = v.ast_builder.make_call(new ASelfExpr, callsite, args) if self.intro.msignature.return_mtype == null then @@ -663,7 +1156,7 @@ redef class MMethodDef if not exist_contract and not is_intro then no_intro_contract(v, mcontract, n_annotations) v.build_contract(n_annotations, mcontract, mclassdef) # Check if the contract must be called to know if it's needed to construct the facet - if mcontract.is_called(v, self) then mproperty.define_contract_facet(v, mclassdef, mcontract) + if mcontract.is_called(v, self.mclassdef) then mproperty.define_contract_facet(v, mclassdef, mcontract) end # Create a contract on the introduction classdef of the property. @@ -701,16 +1194,108 @@ redef class APropdef end end +redef class AAttrPropdef + # Entry point to create a contract (verification of inheritance, or new contract). + redef fun create_contracts(v) + do + v.ast_builder.check_mmodule(v.visited_module.mmodule.as(not null)) + v.current_location = self.location + check_annotation(v) + check_redef(v) + check_invariant(v) + end + + # Verification of the annotation to know if it is a contract annotation. + # If this is the case, we built the appropriate contract. + private fun check_annotation(v: ContractsVisitor) + do + var annotations_expect = get_annotations("expect") + var annotations_ensure = get_annotations("ensure") + var annotation_no_contract = get_annotations("no_contract") + + if (not annotations_expect.is_empty or not annotations_ensure.is_empty) and not annotation_no_contract.is_empty then + v.toolcontext.error(location, "The new contract definition is not correct when using `no_contract`. Remove the contract definition or the `no_contract`") + return + end + + if mwritepropdef == null and (not annotations_ensure.is_empty or not annotations_ensure.is_empty) then + # The contract is not applicable on no writable attribute + v.toolcontext.error(location, "Not applicable contract on not writable attribute") + return + end + + if mwritepropdef != null and not annotation_no_contract.is_empty then + mwritepropdef.no_contract_apply(v, new ASignature.make_from_msignature(mwritepropdef.msignature.as(not null))) + return + end + + if not annotations_expect.is_empty then + v.is_intro_contract = mwritepropdef.is_intro + var exist_contract = mwritepropdef.mproperty.has_expect + mwritepropdef.construct_contract(v, new ASignature.make_from_msignature(mwritepropdef.msignature.as(not null)), annotations_expect, mwritepropdef.mproperty.build_expect, exist_contract) + end + + if not annotations_ensure.is_empty then + v.is_intro_contract = mwritepropdef.is_intro + var exist_contract = mwritepropdef.mproperty.has_ensure + + var mensure = mwritepropdef.mproperty.build_ensure + + mwritepropdef.construct_contract(v, new ASignature.make_from_msignature(mwritepropdef.msignature.as(not null)), annotations_ensure, mensure, exist_contract) + end + end + + # Verification if the method have an inherited contract to apply it. + private fun check_redef(v: ContractsVisitor) + do + var mwritepropdef = self.mwritepropdef + + if mwritepropdef != null and not mwritepropdef.is_intro then + var mexpect = mwritepropdef.mproperty.mexpect + var mensure = mwritepropdef.mproperty.mensure + var mcontract_facet = mwritepropdef.mproperty.mcontract_facet + + if mexpect != null then + if mcontract_facet != null and mcontract_facet.has_applied_expect then return + if mexpect.is_called(v, mwritepropdef.mclassdef) then mwritepropdef.mproperty.define_contract_facet(v, mwritepropdef.mclassdef, mexpect) + end + if mensure != null then + if mcontract_facet != null and mcontract_facet.has_applied_ensure then return + if mensure.is_called(v, mwritepropdef.mclassdef) then mwritepropdef.mproperty.define_contract_facet(v, mwritepropdef.mclassdef, mensure) + end + end + end + + # Check if the class has an invariant to apply it on the property + private fun check_invariant(v: ContractsVisitor) + do + var mpropdef = mpropdef or else mwritepropdef or else mreadpropdef + if not mpropdef isa MPropDef then return + + var minvariant = mpropdef.mclassdef.mclass.minvariant + if minvariant != null then + if mreadpropdef != null and not mreadpropdef.mproperty.has_invariant_facet then + mreadpropdef.mproperty.define_invariant_facet(v, mpropdef.mclassdef, minvariant) + end + if mwritepropdef != null and not mwritepropdef.mproperty.has_invariant_facet then + mwritepropdef.mproperty.define_invariant_facet(v, mpropdef.mclassdef, minvariant) + end + end + end +end + redef class AMethPropdef # Entry point to create a contract (verification of inheritance, or new contract). redef fun create_contracts(v) do + if mpropdef == null then return v.ast_builder.check_mmodule(mpropdef.mclassdef.mmodule) v.current_location = self.location v.is_intro_contract = mpropdef.is_intro check_annotation(v) if not mpropdef.is_intro then check_redef(v) + check_invariant(v) end # Verification of the annotation to know if it is a contract annotation. @@ -740,7 +1325,14 @@ redef class AMethPropdef if not annotations_ensure.is_empty then var exist_contract = mpropdef.mproperty.has_ensure - mpropdef.construct_contract(v, nsignature.clone, annotations_ensure, mpropdef.mproperty.build_ensure, exist_contract) + + var mensure = mpropdef.mproperty.build_ensure + + compute_old(v, mensure, exist_contract, annotations_ensure) + + if not v.toolcontext.check_errors then return # If an error was found in the old compute, just return + + mpropdef.construct_contract(v, nsignature.clone, annotations_ensure, mensure, exist_contract) end end @@ -753,12 +1345,76 @@ redef class AMethPropdef if mexpect != null then if mcontract_facet != null and mcontract_facet.has_applied_expect then return - if mexpect.is_called(v, mpropdef.as(not null)) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mexpect) + if mexpect.is_called(v, mpropdef.mclassdef) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mexpect) end if mensure != null then if mcontract_facet != null and mcontract_facet.has_applied_ensure then return - if mensure.is_called(v, mpropdef.as(not null)) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mensure) + if mensure.is_called(v, mpropdef.mclassdef) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mensure) + end + end + + # Check if the class has an invariant to apply it on the property + private fun check_invariant(v: ContractsVisitor) + do + var minvariant = mpropdef.mclassdef.mclass.minvariant + if minvariant != null and not mpropdef.mproperty.has_invariant_facet then mpropdef.mproperty.define_invariant_facet(v, mpropdef.mclassdef, minvariant) + end + + # Checks the `old` in the ensure annotations. If `old`s are found a new class is generated to keep the old values and an `init_old_{name_method}` method is injected. + # + # Exemple: + # ~~~nitish + # from: + # classe A + # fun add_one(i: Int):Int is ensure(old(i) + 1 == result) + # end + # to: + # classe A + # fun add_one(i: Int):Int is ensure(old(i) + 1 == result) + # + # fun init_old_ensure_add_one(i: Int, old: Old_ensure_add_one): Old_ensure_add_one do + # old.i = i + # return old + # end + # end + # classe Old_ensure_add_one + # var _1: Int + # end + # ~~ + # + private fun compute_old(v: ContractsVisitor, mensure: MEnsure, exist_contract: Bool, annotations_ensure: Collection[AAnnotation]) + do + var old_visitor = new OldVisitor(mpropdef.as(not null), v) + + for annotation_ensure in annotations_ensure do old_visitor.enter_visit(annotation_ensure) + if old_visitor.old_attributes.is_empty then return + + if self.mpropdef.mproperty.is_init then + v.toolcontext.error(location, "The `old` cannot be used with a constructor") + return + end + + # Take into consideration if an ensure contract is already defined without `old` to force the facet override + if exist_contract and not mensure.has_old_mclass then mpropdef.mproperty.mcontract_facet.has_applied_ensure = false + + var old_mclass = mensure.build_old_mclass + + # Try to get the old_classdef in the current context + var old_classdef = old_mclass.try_get_mclassdef(mpropdef.mclassdef.mmodule) + + var n_class: AStdClassdef + + # If the old class does not exist in the current context build a new. + if old_classdef == null then + var object_type = v.mainmodule.get_primitive_class("Object").mclass_type + n_class = v.toolcontext.modelbuilder.create_class_from_mclass(old_mclass, [object_type], mpropdef.mclassdef.mmodule) + else + n_class = v.toolcontext.modelbuilder.mclassdef2node(old_classdef).as(AStdClassdef) end + + old_visitor.build_old_attributes(n_class.mclassdef.as(not null)) + old_visitor.switch_call_to_old_attribut(mensure, self) + old_mclass.build_old_init_methdef(old_visitor, self) end end @@ -828,12 +1484,31 @@ redef class ASignature end end +redef class ACallExpr + + # Checks if the call is an old. If it's the case register in the OldVisitor and remove it. + redef fun check_old(v: OldVisitor) + do + if n_qid.n_id.text == "old" then + var n_arguments = n_args + # Check that the old is in good form `old(one_expression)` + if n_arguments isa AParExprs and n_arguments.n_exprs.length == 1 then + v.old_attributes[n_arguments.n_exprs.first] = null + # Remove the old value + self.replace_with(n_arguments.n_exprs.first) + end + end + end +end + redef class ASendExpr redef fun check_callsite(v) do var actual_callsite = callsite if actual_callsite != null then callsite = v.drive_callsite_to_contract(actual_callsite) + # Set the signature mapping with the old value, this avoids having to re-check the callsite. + callsite.signaturemap = actual_callsite.signaturemap end end end @@ -844,6 +1519,39 @@ redef class ANewExpr var actual_callsite = callsite if actual_callsite != null then callsite = v.drive_callsite_to_contract(actual_callsite) + # Set the signature mapping with the old value, this avoids having to re-check the callsite + callsite.signaturemap = actual_callsite.signaturemap end end end + +# Ast representation of the `in_assertion` checking +# Note, the node if is only composed with a then body (`n_body`) +class AIfInAssertion + super AExpr + + # The associed contract + var mcontract: MContract + + # The body of the if + var n_body: AExpr is writable + + redef fun accept_scope_visitor(v) + do + v.enter_visit_block(n_body, null) + end + + redef fun visit_all(v: Visitor) + do + v.enter_visit(n_body) + end + + redef fun accept_typing(v) + do + v.visit_stmt(n_body) + + self.is_typed = true + + self.mtype = n_body.mtype + end +end diff --git a/src/frontend/check_annotation.nit b/src/frontend/check_annotation.nit index 9dc9cfd8d2..b65cf636c2 100644 --- a/src/frontend/check_annotation.nit +++ b/src/frontend/check_annotation.nit @@ -112,6 +112,7 @@ after after_all example +invariant expect ensure no_contract diff --git a/src/interpreter/naive_interpreter.nit b/src/interpreter/naive_interpreter.nit index 527f16eb9a..36b4a920ab 100644 --- a/src/interpreter/naive_interpreter.nit +++ b/src/interpreter/naive_interpreter.nit @@ -23,6 +23,7 @@ private import parser::tables import mixin private import model::serialize_model private import frontend::explain_assert_api +private import contracts redef class ToolContext # --discover-call-trace @@ -74,6 +75,9 @@ class NaiveInterpreter # Name of all supported functional names var routine_types: Set[String] = new HashSet[String] + # Flag used to know if we are currently checking some assertions. + var in_assertion: Bool = false + init do if mainmodule.model.get_mclasses_by_name("Bool") != null then @@ -1827,6 +1831,18 @@ redef class AIfexprExpr end end + +redef class AIfInAssertion + redef fun stmt(v) + do + if not v.in_assertion then + v.in_assertion = true + v.stmt(self.n_body) + v.in_assertion = false + end + end +end + redef class ADoExpr redef fun stmt(v) do diff --git a/src/model/model.nit b/src/model/model.nit index e22ae846bf..42c8a0e225 100644 --- a/src/model/model.nit +++ b/src/model/model.nit @@ -559,8 +559,10 @@ class MClass # Return the class `self` in the class hierarchy of the module `mmodule`. # # SEE: `MModule::flatten_mclass_hierarchy` - # REQUIRE: `mmodule.has_mclass(self)` + # EXPECT: `mmodule.has_mclass(self)` fun in_hierarchy(mmodule: MModule): POSetElement[MClass] + is + expect(mmodule.has_mclass(self)) do return mmodule.flatten_mclass_hierarchy[self] end @@ -585,10 +587,11 @@ class MClass # Return a generic type based on the class # Is the class is not generic, then the result is `mclass_type` # - # REQUIRE: `mtype_arguments.length == self.arity` + # EXPECT: `mtype_arguments.length == self.arity` fun get_mtype(mtype_arguments: Array[MType]): MClassType + is + expect(mtype_arguments.length == self.arity) do - assert mtype_arguments.length == self.arity if self.arity == 0 then return self.mclass_type var res = get_mtype_cache.get_or_null(mtype_arguments) if res != null then return res @@ -727,8 +730,9 @@ class MClassDef # The hierarchy must not already be set # REQUIRE: `self.in_hierarchy == null` fun set_supertypes(supertypes: Array[MClassType]) + is + expect(self.in_hierarchy == null)# unique_invocation do - assert unique_invocation: self.in_hierarchy == null var mmodule = self.mmodule var model = mmodule.model var mtype = self.bound_mtype @@ -752,8 +756,10 @@ class MClassDef # REQUIRE: `self.in_hierarchy == null` # ENSURE: `self.in_hierarchy != null` fun add_in_hierarchy + is + expect(self.in_hierarchy == null)# unique_invocation + ensure(self.in_hierarchy != null) do - assert unique_invocation: self.in_hierarchy == null var model = mmodule.model var res = model.mclassdef_hierarchy.add_node(self) self.in_hierarchy = res @@ -997,11 +1003,15 @@ abstract class MType # ENSURE: `not self.need_anchor implies result == self` # ENSURE: `not result.need_anchor` fun anchor_to(mmodule: MModule, anchor: nullable MClassType): MType + is + expect(self.need_anchor implies anchor != null) + expect(anchor != null and not anchor.need_anchor) + ensure(not self.need_anchor implies result == self) + ensure(not result.need_anchor) do if not need_anchor then return self - assert anchor != null and not anchor.need_anchor # Just resolve to the anchor and clear all the virtual types - var res = self.resolve_for(anchor, null, mmodule, true) + var res = self.resolve_for(anchor.as(not null), null, mmodule, true) assert not res.need_anchor return res end @@ -1025,8 +1035,10 @@ abstract class MType # # REQUIRE: `super_mclass` is a super-class of `self` # REQUIRE: `self.need_anchor implies anchor != null and self.can_resolve_for(anchor, null, mmodule)` - # ENSURE: `result.mclass = super_mclass` + # ENSURE: `result.mclass == super_mclass` fun supertype_to(mmodule: MModule, anchor: nullable MClassType, super_mclass: MClass): MClassType + is + ensure(result.mclass == super_mclass) do if super_mclass.arity == 0 then return super_mclass.mclass_type if self isa MClassType and self.mclass == super_mclass then return self @@ -1121,7 +1133,7 @@ abstract class MType # # REQUIRE: `can_resolve_for(mtype, anchor, mmodule)` # ENSURE: `not self.need_anchor implies result == self` - fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract + fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract, ensure(not self.need_anchor implies result == self) # Resolve formal type to its verbatim bound. # If the type is not formal, just return self @@ -1186,7 +1198,9 @@ abstract class MType # REQUIRE: `anchor != null implies not anchor.need_anchor` # REQUIRE: `mtype.need_anchor implies anchor != null and mtype.can_resolve_for(anchor, null, mmodule)` # ENSURE: `not self.need_anchor implies result == true` - fun can_resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule): Bool is abstract + fun can_resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule): Bool is abstract, + expect(anchor != null implies not anchor.need_anchor), + ensure(not self.need_anchor implies result) # Return the nullable version of the type # If the type is already nullable then self is returned @@ -1257,28 +1271,29 @@ abstract class MType # This function is used mainly internally. # # REQUIRE: `not self.need_anchor` - fun collect_mclassdefs(mmodule: MModule): Set[MClassDef] is abstract + fun collect_mclassdefs(mmodule: MModule): Set[MClassDef] is abstract, expect(not self.need_anchor) # Compute all the super-classes. # This function is used mainly internally. # # REQUIRE: `not self.need_anchor` - fun collect_mclasses(mmodule: MModule): Set[MClass] is abstract + fun collect_mclasses(mmodule: MModule): Set[MClass] is abstract, expect(not self.need_anchor) # Compute all the declared super-types. # Super-types are returned as declared in the classdefs (verbatim). # This function is used mainly internally. # # REQUIRE: `not self.need_anchor` - fun collect_mtypes(mmodule: MModule): Set[MClassType] is abstract + fun collect_mtypes(mmodule: MModule): Set[MClassType] is abstract, expect(not self.need_anchor) # Is the property in self for a given module # This method does not filter visibility or whatever # # REQUIRE: `not self.need_anchor` fun has_mproperty(mmodule: MModule, mproperty: MProperty): Bool + is + expect(not self.need_anchor) do - assert not self.need_anchor return self.collect_mclassdefs(mmodule).has(mproperty.intro_mclassdef) end end @@ -2227,8 +2242,10 @@ abstract class MProperty # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter) # ENSURE: `not mtype.has_mproperty(mmodule, self) == result.is_empty` fun lookup_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF] + is + expect(not mtype.need_anchor) + ensure(not mtype.has_mproperty(mmodule, self) == result.is_empty) do - assert not mtype.need_anchor mtype = mtype.undecorate var cache = self.lookup_definitions_cache[mmodule, mtype] @@ -2280,8 +2297,10 @@ abstract class MProperty # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter) # ENSURE: `not mtype.has_mproperty(mmodule, self) implies result.is_empty` fun lookup_super_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF] + is + expect(not mtype.need_anchor) + ensure(not mtype.has_mproperty(mmodule, self) implies result.is_empty) do - assert not mtype.need_anchor mtype = mtype.undecorate # First, select all candidates @@ -2349,6 +2368,9 @@ abstract class MProperty # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter) # REQUIRE: `mtype.has_mproperty(mmodule, self)` fun lookup_first_definition(mmodule: MModule, mtype: MType): MPROPDEF + is + expect(not mtype.need_anchor) + expect(mtype.has_mproperty(mmodule, self)) do return lookup_all_definitions(mmodule, mtype).first end @@ -2359,15 +2381,15 @@ abstract class MProperty # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter) # REQUIRE: `mtype.has_mproperty(mmodule, self)` fun lookup_all_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF] + is + expect(not mtype.undecorate.need_anchor) + expect(mtype.undecorate.has_mproperty(mmodule, self)) do mtype = mtype.undecorate var cache = self.lookup_all_definitions_cache[mmodule, mtype] if cache != null then return cache - assert not mtype.need_anchor - assert mtype.has_mproperty(mmodule, self) - #print "select prop {mproperty} for {mtype} in {self}" # First, select all candidates var candidates = new Array[MPROPDEF] @@ -2620,8 +2642,9 @@ abstract class MPropDef # # REQUIRE: `not mtype.need_anchor` fun lookup_next_definition(mmodule: MModule, mtype: MType): MPROPDEF + is + expect(not mtype.need_anchor) do - assert not mtype.need_anchor var mpropdefs = self.mproperty.lookup_all_definitions(mmodule, mtype) var i = mpropdefs.iterator diff --git a/src/model/model_contract.nit b/src/model/model_contract.nit index 2e13a45acd..a4e1bcab8f 100644 --- a/src/model/model_contract.nit +++ b/src/model/model_contract.nit @@ -43,6 +43,34 @@ class MEnsure super BottomMContract redef fun is_already_applied(mfacet: MFacet): Bool do return mfacet.has_applied_ensure + + # The `MOldClass` contract if any + var old_mclass: nullable MOldClass = null + + var old_param = new Variable("old") + + # Is there an `old_mclass`? + private fun has_old_mclass: Bool + do + return self.old_mclass != null + end + + # Build `old_mclass` if is not exist and return it + private fun build_old_mclass: MOldClass + do + var m_old_mclass = self.old_mclass + # build a new `MOldClass` to keep the old value + if m_old_mclass == null then m_old_mclass = new MOldClass(intro_mclassdef.mmodule, "_{self.c_name}_old", intro_mclassdef.location, new Array[String], concrete_kind, public_visibility) + self.old_mclass = m_old_mclass + return m_old_mclass + end +end + +# An invariant contract representation +class MInvariant + super BottomMContract + + redef fun is_already_applied(mfacet: MFacet): Bool do return mfacet.has_applied_invariant end # A facet contract representation @@ -55,15 +83,34 @@ class MFacet # Is there an `ensure` contract applied? var has_applied_ensure: Bool = false + + # Is there an `invariant` contract applied? + var has_applied_invariant: Bool = false +end + +redef class MClass + + # The `MInvariant` contract if any + var minvariant: nullable MInvariant = null + + # Is there an invariant contract? + private fun has_invariant: Bool + do + return self.minvariant != null + end end redef class MMethod - # The contract facet of the method - # is representing the method with a contract + # The entry point of the method with the contract verification + # Depending of the context, this method can verify expect/ensure or both. # This method calls contracts (expect, ensure) and the method var mcontract_facet: nullable MFacet = null + # The entry point of the method with the invariant and contracts verification + # This method calls the `mcontract_facet` and invariant contract + var minvariant_facet: nullable MFacet = null + # The `MExpect` contract if any var mexpect: nullable MExpect = null @@ -75,7 +122,7 @@ redef class MMethod do var m_mensure = self.mensure # build a new `MEnsure` contract - if m_mensure == null then m_mensure = new MEnsure(intro_mclassdef, "_ensure_{name}", intro_mclassdef.location, public_visibility) + if m_mensure == null then m_mensure = new MEnsure(intro_mclassdef, "{name}_ensure_", intro_mclassdef.location, public_visibility) self.mensure = m_mensure return m_mensure end @@ -91,7 +138,7 @@ redef class MMethod do var m_mexpect = self.mexpect # build a new `MExpect` contract - if m_mexpect == null then m_mexpect = new MExpect(intro_mclassdef, "_expect_{name}", intro_mclassdef.location, public_visibility) + if m_mexpect == null then m_mexpect = new MExpect(intro_mclassdef, "{name}_expect_", intro_mclassdef.location, public_visibility) self.mexpect = m_mexpect return m_mexpect end @@ -117,4 +164,31 @@ redef class MMethod do return self.mcontract_facet != null end + + # Build `invariant_facet` if is not exist and return it + private fun build_invariant_facet: MFacet + do + var m_minvariant_facet = self.minvariant_facet + # build a new `MFacet` contract + if m_minvariant_facet == null then m_minvariant_facet = new MFacet(intro_mclassdef, "_invariant_{name}", intro_mclassdef.location, public_visibility) + self.minvariant_facet = m_minvariant_facet + return m_minvariant_facet + end + + # Is there an invariant facet? + fun has_invariant_facet: Bool + do + return self.minvariant_facet != null + end end + +# Representation of `old` in ensure contract. +class MOldClass + super MClass + + # Property to init all old attributes. + var init_old_property: nullable MMethod + + # The old variable. + var old_variable = new Variable("old") +end \ No newline at end of file diff --git a/src/toolcontext.nit b/src/toolcontext.nit index 043e9ee380..0797723308 100644 --- a/src/toolcontext.nit +++ b/src/toolcontext.nit @@ -405,18 +405,12 @@ class ToolContext # Option --stub-man var opt_stub_man = new OptionBool("Generate a stub manpage in pandoc markdown format", "--stub-man") - # Option --no-contract - var opt_no_contract = new OptionBool("Disable the contracts usage", "--no-contract") - - # Option --full-contract - var opt_full_contract = new OptionBool("Enable all contracts usage", "--full-contract") - # Verbose level var verbose_level: Int = 0 init do - option_context.add_option(opt_warn, opt_warning, opt_quiet, opt_stop_on_first_error, opt_keep_going, opt_no_color, opt_log, opt_log_dir, opt_nit_dir, opt_help, opt_version, opt_set_dummy_tool, opt_verbose, opt_bash_completion, opt_stub_man, opt_no_contract, opt_full_contract) + option_context.add_option(opt_warn, opt_warning, opt_quiet, opt_stop_on_first_error, opt_keep_going, opt_no_color, opt_log, opt_log_dir, opt_nit_dir, opt_help, opt_version, opt_set_dummy_tool, opt_verbose, opt_bash_completion, opt_stub_man) # Hide some internal options opt_stub_man.hidden = true diff --git a/tests/contracts_invariant_1.nit b/tests/contracts_invariant_1.nit new file mode 100644 index 0000000000..dca5e0421b --- /dev/null +++ b/tests/contracts_invariant_1.nit @@ -0,0 +1,29 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +# Test the creation and usage of simple invariant contract. + +class Test + invariant(bar >= 10) + + var bar: Int + + fun set_bar(x: Int) do + print x + bar = x + end +end + +var test = new Test(10) +test.set_bar(10)# Fail broke the invariant diff --git a/tests/contracts_invariant_attr.nit b/tests/contracts_invariant_attr.nit new file mode 100644 index 0000000000..98945d957c --- /dev/null +++ b/tests/contracts_invariant_attr.nit @@ -0,0 +1,29 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +# Test the creation and usage of simple invariant contract with attribute. + +class Test + invariant(bar >= 10) + + var bar: Int + + fun set_bar(x: Int) do + print x + bar = x + end +end + +var test = new Test(10) +test.bar = 9 # Fail broke the invariant diff --git a/tests/contracts_invariant_defaultinit.nit b/tests/contracts_invariant_defaultinit.nit new file mode 100644 index 0000000000..a546273b2b --- /dev/null +++ b/tests/contracts_invariant_defaultinit.nit @@ -0,0 +1,27 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + invariant(i > 0) + + var i: Int + + init + do + + end + +end + +var a = new A(0) diff --git a/tests/contracts_invariant_diamond.nit b/tests/contracts_invariant_diamond.nit new file mode 100644 index 0000000000..c8196fa700 --- /dev/null +++ b/tests/contracts_invariant_diamond.nit @@ -0,0 +1,42 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + invariant(bar >= 10) + + var bar: Int +end + +class B + invariant(bar > 10) + super A + + fun set_bar(x: Int) do + print x + bar = x + end +end + +class C + invariant(bar > 12) + super A +end + +class D + super B + super C +end + +var test = new D(13) +test.set_bar(11) diff --git a/tests/contracts_invariant_in_redef.nit b/tests/contracts_invariant_in_redef.nit new file mode 100644 index 0000000000..336e197254 --- /dev/null +++ b/tests/contracts_invariant_in_redef.nit @@ -0,0 +1,23 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +import contracts_abstract + +# Test if the invariant contract is added to old method definitions. + +redef class MySubClass + invariant(false) +end + +var test = new MySubClass +test.foo(11, 2.5) diff --git a/tests/contracts_invariant_inheritance.nit b/tests/contracts_invariant_inheritance.nit new file mode 100644 index 0000000000..78374464c6 --- /dev/null +++ b/tests/contracts_invariant_inheritance.nit @@ -0,0 +1,34 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +# Test the creation and usage of invariant contracts with inheritance. + +class A + invariant(bar >= 10) + + var bar: Int +end + +class B + super A + + fun set_bar(x: Int) do + print x + bar = x + end +end + +var test = new B(10) +test.set_bar(11) # OK +test.set_bar(2) # Fail broke invariant bar >= 10 diff --git a/tests/contracts_invariant_inheritance_multi.nit b/tests/contracts_invariant_inheritance_multi.nit new file mode 100644 index 0000000000..75a7dadbc9 --- /dev/null +++ b/tests/contracts_invariant_inheritance_multi.nit @@ -0,0 +1,47 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +module contracts_invariant_inheritance_multi + +# Test the creation and usage of invariant contracts with multiple inheritance. + +class A + invariant(bar >= 10) + + var bar: Int +end + +class B + invariant(baz <= 2.0) + + var baz: Float +end + +class C + super A + super B + + autoinit bar=, baz= + + fun set_bar_baz(x: Int, y: Float) + do + print x + bar = x + print y + baz = y + end +end + +var test = new C(10, 2.0) +test.set_bar_baz(16, 1.5)# Ok +test.set_bar_baz(1, 3.8)# Fail diff --git a/tests/contracts_invariant_inheritance_multi_2.nit b/tests/contracts_invariant_inheritance_multi_2.nit new file mode 100644 index 0000000000..8fb8eb9512 --- /dev/null +++ b/tests/contracts_invariant_inheritance_multi_2.nit @@ -0,0 +1,35 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +import contracts_invariant_inheritance_multi + +# Test import a class with invariant and add a new one by new inheritance + +class E + invariant(bazz) + + var bazz = true +end + +redef class C + super E + + redef fun set_bar_baz(x: Int, y: Float) do + super + self.bazz = false + print bazz + end +end + +var test = new C(10, 2.0) +test.set_bar_baz(10, 2.0)# The method broke the E invariant with the set bazz = false diff --git a/tests/contracts_null_parameter.nit b/tests/contracts_null_parameter.nit new file mode 100644 index 0000000000..4587d227b4 --- /dev/null +++ b/tests/contracts_null_parameter.nit @@ -0,0 +1,29 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + + var null_attribut: nullable Int + + fun null_parameter(i: nullable Int) + is + ensure(null_attribut == i) + do + null_attribut = i + end +end + + +var a = new A +a.null_parameter diff --git a/tests/contracts_old_1.nit b/tests/contracts_old_1.nit new file mode 100644 index 0000000000..9880c5cd7f --- /dev/null +++ b/tests/contracts_old_1.nit @@ -0,0 +1,40 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun add_one + is + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +class B + var i: Int + + fun add_one + is + ensure(old(i) + 1 == i) + do + i = i + end +end + +var a = new A(0) +a.add_one +var b = new B(0) +b.add_one \ No newline at end of file diff --git a/tests/contracts_old_add_redef.nit b/tests/contracts_old_add_redef.nit new file mode 100644 index 0000000000..4f6387c1f0 --- /dev/null +++ b/tests/contracts_old_add_redef.nit @@ -0,0 +1,41 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun add_one + is + ensure(self.i > 0) + do + i = i + 1 + end +end + +class B + super A + + redef fun add_one + is + ensure(old(i) + 1 == i) + do + super + end +end + +var a = new A(0) +a.add_one + +var b = new B(0) +b.add_one \ No newline at end of file diff --git a/tests/contracts_old_already_declared.nit b/tests/contracts_old_already_declared.nit new file mode 100644 index 0000000000..d95440d45a --- /dev/null +++ b/tests/contracts_old_already_declared.nit @@ -0,0 +1,41 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun foo + is + ensure(old(i) < i) + do + i = i + 10 + end +end + +class B + super A + + redef fun foo + is + ensure(old(i) + 10 < i) + do + super + i = i + 10 + end +end + +var a = new A(0) +a.foo +var b = new B(0) +b.foo diff --git a/tests/contracts_old_default_init.nit b/tests/contracts_old_default_init.nit new file mode 100644 index 0000000000..bf1992b49f --- /dev/null +++ b/tests/contracts_old_default_init.nit @@ -0,0 +1,26 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + init + is + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +var a = new A(10) \ No newline at end of file diff --git a/tests/contracts_old_no_expression.nit b/tests/contracts_old_no_expression.nit new file mode 100644 index 0000000000..760ae7bd50 --- /dev/null +++ b/tests/contracts_old_no_expression.nit @@ -0,0 +1,29 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun bar do print "Test" + + fun foo + is + ensure(old(bar)) + do + i = i + 10 + end +end + +var a = new A(0) +a.foo diff --git a/tests/contracts_old_redef.nit b/tests/contracts_old_redef.nit new file mode 100644 index 0000000000..dd62c4df74 --- /dev/null +++ b/tests/contracts_old_redef.nit @@ -0,0 +1,44 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun add_one + is + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +class B + super A + + var new_int: Int + + redef fun add_one + is + ensure(old(new_int) + 1 == new_int) + do + new_int = new_int + end + +end + +var a = new A(0) +a.add_one + +var b = new B(0, 0) +b.add_one diff --git a/tests/contracts_old_same_name.nit b/tests/contracts_old_same_name.nit new file mode 100644 index 0000000000..e959b5b632 --- /dev/null +++ b/tests/contracts_old_same_name.nit @@ -0,0 +1,41 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun add_one + is + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +class B + var i: Int + + fun add_one + is + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +var a = new A(0) +a.add_one + +var b = new B(0) +b.add_one diff --git a/tests/contracts_old_same_property.nit b/tests/contracts_old_same_property.nit new file mode 100644 index 0000000000..3fa8700382 --- /dev/null +++ b/tests/contracts_old_same_property.nit @@ -0,0 +1,42 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun add_one + is + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +class B + var i: Int + + var a: A + + fun add_one + is + ensure(old(i) + 1 == i) + ensure(old(a.i) + 1 == a.i) + do + i = i + 1 + a.add_one + end +end + +var b = new B(0, new A(0)) +b.add_one diff --git a/tests/contracts_old_unknown.nit b/tests/contracts_old_unknown.nit new file mode 100644 index 0000000000..5dfa25418e --- /dev/null +++ b/tests/contracts_old_unknown.nit @@ -0,0 +1,27 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun foo + is + ensure(old(z) == 10) + do + i = i + 10 + end +end + +var a = new A(0) +a.foo diff --git a/tests/contracts_old_with_expect.nit b/tests/contracts_old_with_expect.nit new file mode 100644 index 0000000000..d1c3e2c360 --- /dev/null +++ b/tests/contracts_old_with_expect.nit @@ -0,0 +1,28 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +class A + var i: Int + + fun add_one + is + expect(i > 0) + ensure(old(i) + 1 == i) + do + i = i + 1 + end +end + +var a = new A(0) +a.add_one \ No newline at end of file diff --git a/tests/contracts_threaded.nit b/tests/contracts_threaded.nit new file mode 100644 index 0000000000..06dfbebd0b --- /dev/null +++ b/tests/contracts_threaded.nit @@ -0,0 +1,52 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +# This test shows the verification of contracts in a parallel execution. + +import pthreads + +fun foo is + threaded + expect(contract_foo) +do + print "Foo" + bar("Foo thread") +end + +fun bar(thread_name: String) +is + threaded + expect(contract_bar(thread_name)) +do + print "Bar called from {thread_name}" +end + +fun contract_foo: Bool +do + print("Foo contract") + return true +end + +fun contract_bar(thread_name: String): Bool +do + sys.nanosleep(3,0) + print("Bar contract called from {thread_name}") + return true +end + + +foo +sys.nanosleep(1,0) +bar("Main thread") +sys.nanosleep(5,0) diff --git a/tests/sav/contracts_error.res b/tests/sav/contracts_error.res index 38471299d3..2c6a91027c 100644 --- a/tests/sav/contracts_error.res +++ b/tests/sav/contracts_error.res @@ -1,2 +1 @@ contracts_error.nit:23,3--23: Error: expected an expression. -contracts_error.nit:24,3--23: Error: expected an expression. diff --git a/tests/sav/contracts_invariant_1.res b/tests/sav/contracts_invariant_1.res new file mode 100644 index 0000000000..f599e28b8a --- /dev/null +++ b/tests/sav/contracts_invariant_1.res @@ -0,0 +1 @@ +10 diff --git a/tests/sav/contracts_invariant_attr.res b/tests/sav/contracts_invariant_attr.res new file mode 100644 index 0000000000..ea06d90b3d --- /dev/null +++ b/tests/sav/contracts_invariant_attr.res @@ -0,0 +1 @@ +Runtime error: Assert 'invariant(bar >= 10)' failed (contracts_invariant_attr.nit:18) diff --git a/tests/sav/contracts_invariant_defaultinit.res b/tests/sav/contracts_invariant_defaultinit.res new file mode 100644 index 0000000000..95ba739301 --- /dev/null +++ b/tests/sav/contracts_invariant_defaultinit.res @@ -0,0 +1 @@ +Runtime error: Assert 'invariant(i > 0)' failed (contracts_invariant_defaultinit.nit:16) diff --git a/tests/sav/contracts_invariant_diamond.res b/tests/sav/contracts_invariant_diamond.res new file mode 100644 index 0000000000..ccd3163337 --- /dev/null +++ b/tests/sav/contracts_invariant_diamond.res @@ -0,0 +1,2 @@ +Runtime error: Assert 'invariant(bar > 12)' failed (contracts_invariant_diamond.nit:32) +11 diff --git a/tests/sav/contracts_invariant_in_redef.res b/tests/sav/contracts_invariant_in_redef.res new file mode 100644 index 0000000000..c49a3b43c4 --- /dev/null +++ b/tests/sav/contracts_invariant_in_redef.res @@ -0,0 +1 @@ +Runtime error: Assert 'invariant(false)' failed (contracts_invariant_in_redef.nit:19) diff --git a/tests/sav/contracts_invariant_inheritance.res b/tests/sav/contracts_invariant_inheritance.res new file mode 100644 index 0000000000..dd226fa9dc --- /dev/null +++ b/tests/sav/contracts_invariant_inheritance.res @@ -0,0 +1,3 @@ +Runtime error: Assert 'invariant(bar >= 10)' failed (contracts_invariant_inheritance.nit:18) +11 +2 diff --git a/tests/sav/contracts_invariant_inheritance_multi.res b/tests/sav/contracts_invariant_inheritance_multi.res new file mode 100644 index 0000000000..4372043fb8 --- /dev/null +++ b/tests/sav/contracts_invariant_inheritance_multi.res @@ -0,0 +1,5 @@ +Runtime error: Assert 'invariant(bar >= 10)' failed (contracts_invariant_inheritance_multi.nit:19) +16 +1.5 +1 +3.8 diff --git a/tests/sav/contracts_invariant_inheritance_multi_2.res b/tests/sav/contracts_invariant_inheritance_multi_2.res new file mode 100644 index 0000000000..81f81265ee --- /dev/null +++ b/tests/sav/contracts_invariant_inheritance_multi_2.res @@ -0,0 +1,4 @@ +Runtime error: Assert 'invariant(bazz)' failed (contracts_invariant_inheritance_multi_2.nit:19) +10 +2.0 +false diff --git a/tests/sav/contracts_old_1.res b/tests/sav/contracts_old_1.res new file mode 100644 index 0000000000..f65c23ccc2 --- /dev/null +++ b/tests/sav/contracts_old_1.res @@ -0,0 +1 @@ +Runtime error: Assert 'ensure(old(i) + 1 == i)' failed (contracts_old_1.nit:31) diff --git a/tests/sav/contracts_old_add_redef.res b/tests/sav/contracts_old_add_redef.res new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/sav/contracts_old_default_init.res b/tests/sav/contracts_old_default_init.res new file mode 100644 index 0000000000..0fbdd4a462 --- /dev/null +++ b/tests/sav/contracts_old_default_init.res @@ -0,0 +1 @@ +contracts_old_default_init.nit:18,2--23,4: The `old` cannot be used with a constructor diff --git a/tests/sav/contracts_old_no_expression.res b/tests/sav/contracts_old_no_expression.res new file mode 100644 index 0000000000..f4f329ba9b --- /dev/null +++ b/tests/sav/contracts_old_no_expression.res @@ -0,0 +1 @@ +contracts_old_no_expression.nit:22,3--18: Error: expected an expression. diff --git a/tests/sav/contracts_old_redef.res b/tests/sav/contracts_old_redef.res new file mode 100644 index 0000000000..150f8bb1df --- /dev/null +++ b/tests/sav/contracts_old_redef.res @@ -0,0 +1 @@ +Runtime error: Assert 'ensure(old(i) + 1 == i)' failed (contracts_old_redef.nit:20) diff --git a/tests/sav/contracts_old_same_property.res b/tests/sav/contracts_old_same_property.res new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/sav/contracts_old_unknown.res b/tests/sav/contracts_old_unknown.res new file mode 100644 index 0000000000..efd1aa01f8 --- /dev/null +++ b/tests/sav/contracts_old_unknown.res @@ -0,0 +1 @@ +contracts_old_unknown.nit:20,14: Error: method or variable `z` unknown in `A`. diff --git a/tests/sav/contracts_old_with_expect.res b/tests/sav/contracts_old_with_expect.res new file mode 100644 index 0000000000..8d6abf5c16 --- /dev/null +++ b/tests/sav/contracts_old_with_expect.res @@ -0,0 +1 @@ +Runtime error: Assert 'expect(i > 0)' failed (contracts_old_with_expect.nit:20) diff --git a/tests/sav/contracts_threaded.res b/tests/sav/contracts_threaded.res new file mode 100644 index 0000000000..f823b0f69e --- /dev/null +++ b/tests/sav/contracts_threaded.res @@ -0,0 +1,6 @@ +Foo contract +Foo +Bar contract called from Foo thread +Bar called from Foo thread +Bar contract called from Main thread +Bar called from Main thread diff --git a/tests/sav/error_class_glob.res b/tests/sav/error_class_glob.res index 5c09788c09..04d3f95409 100644 --- a/tests/sav/error_class_glob.res +++ b/tests/sav/error_class_glob.res @@ -1,2 +1,2 @@ -../lib/core/collection/hash_collection.nit:275,3--6: Possible duplication of the root class `Object` -../lib/core/collection/hash_collection.nit:473,3--6: Possible duplication of the root class `Object` +../lib/core/collection/abstract_collection.nit:13,1--1385,3: Error: ambiguous class name `Object`; conflict between `core::Object` and `module_0::Object`. +../lib/core/collection/abstract_collection.nit:13,1--1385,3: Type Error: missing primitive class `Object'. diff --git a/tests/sav/syntax_annotations3.res b/tests/sav/syntax_annotations3.res index 52e959447b..60964a087d 100644 --- a/tests/sav/syntax_annotations3.res +++ b/tests/sav/syntax_annotations3.res @@ -1,4 +1,4 @@ -syntax_annotations3.nit:16,2--20: Warning: unknown annotation `invariant`. +syntax_annotations3.nit:16,12--16: Error: method or variable `solde` unknown in `Account`. syntax_annotations3.nit:19,3--12: Warning: unknown annotation `pre`. syntax_annotations3.nit:20,3--22: Warning: unknown annotation `post`. syntax_annotations3.nit:28,3--7: Warning: unknown annotation `inter`. diff --git a/tests/sav/test_c_alt2.res b/tests/sav/test_c_alt2.res index c461eba905..1eb35c9cdf 100644 --- a/tests/sav/test_c_alt2.res +++ b/tests/sav/test_c_alt2.res @@ -1,2 +1,2 @@ -Runtime error: Assert failed (../lib/c/c.nit:38) +Runtime error: Assert 'expect(index >= 0 and index < length)' failed (../lib/core/collection/abstract_collection.nit:894) 0 diff --git a/tests/sav/test_c_alt3.res b/tests/sav/test_c_alt3.res index c461eba905..1eb35c9cdf 100644 --- a/tests/sav/test_c_alt3.res +++ b/tests/sav/test_c_alt3.res @@ -1,2 +1,2 @@ -Runtime error: Assert failed (../lib/c/c.nit:38) +Runtime error: Assert 'expect(index >= 0 and index < length)' failed (../lib/core/collection/abstract_collection.nit:894) 0 diff --git a/tests/sav/test_new_native_alt1.res b/tests/sav/test_new_native_alt1.res index 1af51e89dc..f5dba16f41 100644 --- a/tests/sav/test_new_native_alt1.res +++ b/tests/sav/test_new_native_alt1.res @@ -1,4 +1,4 @@ -Runtime error: Cast failed. Expected `E`, got `Bool` (../lib/core/collection/array.nit:991) +Runtime error: Cast failed. Expected `E`, got `Bool` (../lib/core/collection/array.nit:992) CString 78 Nit diff --git a/tests/sav/test_toolcontext_args1.res b/tests/sav/test_toolcontext_args1.res index a04e1b8798..ad80c05ba5 100644 --- a/tests/sav/test_toolcontext_args1.res +++ b/tests/sav/test_toolcontext_args1.res @@ -5,7 +5,7 @@ _DUMMY_TOOL() COMPREPLY=() cur="${COMP_WORDS[COMP_CWORD]}" prev="${COMP_WORDS[COMP_CWORD-1]}" - opts="--warn --warning --quiet --stop-on-first-error --keep-going --no-color --log --log-dir --nit-dir --help --version --set-dummy-tool --verbose --bash-completion --stub-man --no-contract --full-contract --option-a --option-b" + opts="--warn --warning --quiet --stop-on-first-error --keep-going --no-color --log --log-dir --nit-dir --help --version --set-dummy-tool --verbose --bash-completion --stub-man --option-a --option-b" if [[ ${cur} == -* ]] ; then COMPREPLY=( $(compgen -W "${opts}" -- ${cur}) ) return 0 diff --git a/tests/sav/test_toolcontext_args2.res b/tests/sav/test_toolcontext_args2.res index 9d4104e7c6..f7e7da5a72 100644 --- a/tests/sav/test_toolcontext_args2.res +++ b/tests/sav/test_toolcontext_args2.res @@ -12,8 +12,6 @@ Test for ToolContext, try --bash-completion. -h, -?, --help Show Help (This screen) --version Show version and exit -v, --verbose Additional messages from the tool - --no-contract Disable the contracts usage - --full-contract Enable all contracts usage -a, --option-a option a, do nothing -b, --option-b option b, do nothing -c option c, do nothing