Ticket #243: suppress-invariants.patch

Source/CommandLine.cobra

@@ -194 +194 @@
         },
         {
             'name': 'copy-core',
+            'synonyms': ['cc'],
             'type': 'bool',
             'description': 'Copy the Cobra.Core library to the same location as the resulting executable which will insulate the executable from newer Cobra installations.',
             'default': 'no',

Source/BackEndClr/SharpGenerator.cobra

@@ -1149 +1149 @@
     def writeSharpInvariantMethod(sw as CurlyWriter)
         if .compiler.options['contracts'] <> 'none'
             sw.write('\nint _ih_invariantGuard;\n\n')
+            ##For minimal and correct invariant checks put the guard only on first cobra defined baseclass class derived fm a native class 
+            ## this would still be incorrect for cobra defined classes used out of libraries 
+            ## *and* I think it will incorrectly fail to invoke on doubly and more nested methods
+            ## so suppress and rely on developer explicitly tagging methods outside invariant checking with
+            ##  SuppressInvariantCheck Attribute.
+            #if this inherits Struct
+            #   sw.write('\nint _ih_invariantGuard;\n\n')
+            #else if not .baseClass or .baseClass.isFromBinaryLibrary
+            #   sw.write('\nprotected int _ih_invariantGuard;\n\n')
+                
         if .compiler.options['contracts'] <> 'methods'
             return
         sw.write('\n[.sharpInvariantVisibility] void invariant_[.rootName]() {\n')
@@ -1715 +1725 @@
                     if param.isOut
                         sharpInit = param.type.sharpInit
                         if not sharpInit.length
-                            # TODO/HACK: yes we need something like this (or a way to convice C# that the out param reference in `finally` really is okay),
+                            # TODO/HACK: yes we need something like this (or a way to convince C# that the out param reference in `finally` really is okay),
                             # but it should be something less hackish, like an attribute
                             sharpInit = 'DateTime.Today'
                         sw.write('[param.sharpName] = [sharpInit];')
@@ -1731 +1741 @@
                     continue
                 stmt.writeSharpStmt(sw)
             if willEnsure
-                if not stmt inherits ReturnStmt and not stmt inherits ThrowStmt
-                    sw.write('_lh_canEnsure = true;\n')
-                sw.dedentAndWrite('} finally { // ensure\n')
-                sw.indentAndWrite('if (_lh_canEnsure) {\n')
-                sw.indent
-                _ensurePart.writeSharpDef(sw)
-                sw.dedentAndWrite('}\n')
-                sw.dedentAndWrite('}\n')
+                suppressInvariantCheck = any for a in .attributes get a.name == 'SuppressInvariantCheckAttribute' 
+                if suppressInvariantCheck
+                    sw.dedentAndWrite('} finally { // ensure\n')
+                    sw.indentAndWrite('// Invariant Check suppressed by Cobra.Core.SuppressInvariantCheckAttribute\n')
+                    sw.dedentAndWrite('}\n')
+                else
+                    if not stmt inherits ReturnStmt and not stmt inherits ThrowStmt
+                        sw.write('_lh_canEnsure = true;\n')
+                    sw.dedentAndWrite('} finally { // ensure\n')
+                    sw.indentAndWrite('if (_lh_canEnsure) {\n')
+                    sw.indent
+                    _ensurePart.writeSharpDef(sw)
+                    sw.dedentAndWrite('}\n') # if
+                    sw.dedentAndWrite('}\n') # finally
+                    
             if .compiler.hasDetailedStackTraceOption
                 .writeDSTTail(sw)
             .writeSharpImpFooter(sw)
@@ -1747 +1764 @@
             sw.write('\n')
         finally
             .compiler.codeMemberStack.pop
-
+            
     def writeSharpImpHeader(sw as CurlyWriter)
         pass
         

Source/Cobra.Core/Misc.cobra

@@ -45 +45 @@
         has AttributeUsage(AttributeTargets.Method, allowMultiple=false)
         pass
 
+    class SuppressInvariantCheckAttribute inherits Attribute
+        has AttributeUsage(AttributeTargets.Method, allowMultiple=false)
+        """
+        Use to suppress Invariant checking on a method.
+        Place on invariant or initializer helper methods to suppress invariant checking when invariant
+        checking is unnecessary or invariant not yet established.
+        """
+        pass
+        
     class CobraDirectString is extern
         """
         Used internally for assert, require and ensure to encode strings that should not be passed to CobraCore.toTechString.

Tests/340-contracts/932-invariant-calls-suppressed.cobra

@@ +1 @@
+# Chking that SuppressInvariantCheck Attribute is working
+# put on any methods (invariant helpers and initializer helpers) that
+# should not have the invariants checked after their execution
+class Base
+    var icb = 0
+    var countB = 0
+    
+    cue init
+        base.init
+        .countB = 1
+        print 'end init of Base'
+
+    def _m1 as bool has SuppressInvariantCheck
+        print 'helper invariant of Base (_m1)'
+        .icb += 1
+        return true
+
+    invariant
+        _m1
+        .icb == .countB
+
+class Derived inherits Base
+    var icd = 0
+    var countD = 0
+    
+    cue init
+        base.init
+        assert .icb == 1
+        assert .icd == 0
+        .chk
+        assert .icb == 1
+        assert .icd == 0
+        .countD = 1
+        .countB = 2
+        print 'end init of Derived'
+        
+    def chk has SuppressInvariantCheck
+        print 'in initHelper'
+        
+    def _m2 as bool has SuppressInvariantCheck
+        print 'helper invariant of Derived (_m2)'
+        .icd += 1
+        return true
+
+    invariant
+        _m2
+        .icd == .countD
+        
+class P     
+    def main is shared
+        Derived()

Tests/340-contracts/930-invariant-calls-notSuppressed.cobra

@@ +1 @@
+# Chking base behaviour without invariant suppression
+# put on any methods (invariant helpers and initializer helpers) that
+# should not have the invariants checked after their execution
+class Base
+    var icb = 0
+    var countB = 0
+    
+    cue init
+        base.init
+        .countB = 1
+        print 'end init of Base'
+
+    def _m1 as bool 
+        print 'helper invariant of Base (_m1)'
+        .icb += 1
+        return true
+
+    invariant
+        _m1
+        .icb == .countB
+
+class Derived inherits Base
+    var icd = 0
+    var countD = 0
+    
+    cue init
+        base.init
+        assert .icb == 1
+        assert .icd == 0
+        .countB = 3
+        .countD = 1
+        .chk
+        assert .icb == 3
+        assert .icd == 1
+        .countD = 2
+        .countB = 5
+        print 'end init of Derived'
+        
+    def chk 
+        print 'in initHelper'
+        
+    def _m2 as bool 
+        print 'helper invariant of Derived (_m2)'
+        .icd += 1
+        return true
+
+    invariant
+        _m2
+        .icd == .countD
+        
+class P     
+    def main is shared
+        Derived()