Merge pull request #4 from edgarsvitolins/meilers_bugfixes

Meilers bugfixes

src/nagini_translation/analyzer.py

@@ -576,6 +576,7 @@ def visit_ClassDef(self, node: ast.ClassDef) -> None:
 
         # check if a class is complex (when it or one of its parents had a @Complex class decorator)
         # complex class instance attributes are stored in __dict__
+        # ME: Set to true to make all classes complex by default and test if things still work.
         cls.is_complex = self.is_complex_class(node)
 
         for member in node.body:

src/nagini_translation/lib/program_nodes.py

@@ -384,6 +384,7 @@ def __init__(self, name: str, superscope: PythonScope,
         self.is_adt = name == 'ADT' # This flag is set when the class is
         # defining an algebraic data type or one of its constructors.
         # This flag is set transitively across subclasses.
+        # ME: Set to true to make all classes complex by default and test if things still work.
         self.is_complex = False
         self.illegal_attribute_names = set()
 

src/nagini_translation/resources/str.sil

@@ -75,17 +75,21 @@ method keydict___init__(self: Ref)
     ensures forall key: Ref :: {keydict___item__(self, key)} acc(keydict___item__(self, key).keydict_val) && !keydict___contains__(self, key)
 
 function keydict___item__(self: Ref, key: Ref): Ref
+    decreases _
     ensures keydict___item__inv(self, result) == key
 
 function keydict___item__inv(self: Ref, val_ref: Ref): Ref
+    decreases _
 
 function keydict___contains__(self: Ref, key: Ref) : Bool
+    decreases _
     requires acc(keydict___item__(self, key).keydict_val, wildcard)
 {
   keydict___item__(self, key).keydict_val.isSome
 }
 
 function keydict___getitem__(self: Ref, key: Ref) : Ref
+    decreases _
     requires acc(keydict___item__(self, key).keydict_val, wildcard)
     requires keydict___contains__(self, key)
 {
@@ -105,20 +109,24 @@ method keydict___setitem__(self: Ref, key: Ref, item: Ref)
 
 // Of all possible keys, which have been set in the keydict
 function keydict_keys(self:Ref ): Set[Ref]
+    decreases _
     requires forall key: Ref :: {keydict___item__(self, key)} acc(keydict___item__(self, key).keydict_val, wildcard)
     ensures forall key: Ref :: {keydict___contains__(self, key)} {key in result} keydict___contains__(self, key) == (key in result)
 
 // Of the keys in the Set[Ref], which have been set in the keydict
 function keydict_keys_specific(self: Ref, keys: Set[Ref]): Set[Ref]
+    decreases _
     requires forall key: Ref :: {key in keys} key in keys ==> acc(keydict___item__(self, key).keydict_val, wildcard)
     ensures forall key: Ref :: {key in keys} key in keys ==> keydict___contains__(self, key) == (key in result)
 
 function keydict_values(self: Ref): Set[Ref]
+    decreases _
     requires forall key: Ref :: {keydict___item__(self, key)} acc(keydict___item__(self, key).keydict_val, wildcard)
     ensures forall value: Ref :: {value in result}
     (exists key:Ref :: {keydict___contains__(self, key)} (keydict___contains__(self, key) && (keydict___getitem__(self, key) == value))) == value in result
 
 
 function keydict___len__(self: Ref): Int
+    decreases _
     requires forall key: Ref :: {keydict___item__(self, key)} acc(keydict___item__(self, key).keydict_val, wildcard)
     ensures result == |keydict_keys(self)|

src/nagini_translation/translators/expression.py

@@ -873,7 +873,7 @@ def translate_Attribute(self, node: ast.Attribute,
                 if isinstance(field, PythonGlobalVar):
                     field_func = self.translate_static_field_access(field, receiver,
                                                                     node, ctx)
-                    return [], field_func
+                    return stmt, field_func
                 if isinstance(field, PythonMethod):
                     # This is a reference to a property, so we translate it to a call of
                     # the property getter function.
@@ -937,15 +937,17 @@ def translate_Attribute(self, node: ast.Attribute,
                             recv_getattr = self._get_function_call(recv_type, func_name, args, arg_types, node, ctx,
                                                                    position)
 
-                            ret = ([], recv_getattr)
+                            # ret = (stmt, recv_getattr)
+                            ret_stmt = []
+                            ret_val = recv_getattr
                         else:
-                            ret = self.get_complex_attr(node,
+                            ret_stmt, ret_val = self.get_complex_attr(node,
                                                         self.translate_string(node.attr, None, ctx),
                                                         receiver,
                                                         recv_type,
                                                         ctx,
                                                         position)
-                        return ret
+                        return stmt + ret_stmt, ret_val
             return (stmt, self.viper.FieldAccess(receiver, field.sil_field,
                                                  position, self.no_info(ctx)))
 
@@ -1203,8 +1205,9 @@ def translate_Compare(self, node: ast.Compare,
         else:
             raise UnsupportedException(node.ops[0])
         if left_type.get_function(compare_func):
-            if getattr(left_type, 'is_complex', False) and getattr(right_type, 'is_complex', False):
-                comparison = self.viper.EqCmp(left, right, position, info)
+            if (getattr(left_type, 'is_complex', False) and getattr(right_type, 'is_complex', False) and
+                    (isinstance(node.ops[0], ast.Eq) or isinstance(node.ops[0], ast.Is))) and not left_type.interface and not right_type.interface:
+                comparison = self.viper.EqCmp(left, right, position, info)  # ME: Why are we doing this?
             else:
                 comparison = self.get_function_call(left_type, compare_func,
                                                     [left, right],

src/nagini_translation/translators/obligation/method_node.py

@@ -291,7 +291,7 @@ def _add_caller_leak_check(self) -> None:
                     self._python_method.interface_dict):
                 exhale = self._obligation_info.caller_measure_map.check(
                     sil.RefVar(self._obligation_info.current_thread_var),
-                    sil.RawIntExpression(1))
+                    sil.RawIntExpression(0))
             else:
                 exhale = sil.BigAnd([termination_leak_check, leak_check])
         else:

src/nagini_translation/translators/obligation/types/must_terminate.py

@@ -293,7 +293,7 @@ def generate_axiomatized_preconditions(
         if self.is_interface_method_terminating(interface_dict):
             cthread = sil.RefVar(obligation_info.current_thread_var)
             check = obligation_info.caller_measure_map.check(
-                cthread, sil.RawIntExpression(1))
+                cthread, sil.RawIntExpression(0))
             return [check]
         else:
             return []

tests/functional/verification/issues/00112.py

@@ -8,7 +8,6 @@
 
 def newlist() -> List[int]:
     Requires(MustTerminate(1))
-    #:: ExpectedOutput(leak_check.failed:caller.has_unsatisfied_obligations)
     res = []  # type: List[int]
     return res