Wiki

Ticket #243: suppress-invariants.patch

File suppress-invariants.patch, 6.9 KB (added by hopscc, 4 years ago)
  • Source/CommandLine.cobra

     
    194194        }, 
    195195        { 
    196196            'name': 'copy-core', 
     197            'synonyms': ['cc'], 
    197198            'type': 'bool', 
    198199            'description': 'Copy the Cobra.Core library to the same location as the resulting executable which will insulate the executable from newer Cobra installations.', 
    199200            'default': 'no', 
  • Source/BackEndClr/SharpGenerator.cobra

     
    11491149    def writeSharpInvariantMethod(sw as CurlyWriter) 
    11501150        if .compiler.options['contracts'] <> 'none' 
    11511151            sw.write('\nint _ih_invariantGuard;\n\n') 
     1152            ##For minimal and correct invariant checks put the guard only on first cobra defined baseclass class derived fm a native class  
     1153            ## this would still be incorrect for cobra defined classes used out of libraries  
     1154            ## *and* I think it will incorrectly fail to invoke on doubly and more nested methods 
     1155            ## so suppress and rely on developer explicitly tagging methods outside invariant checking with 
     1156            ##  SuppressInvariantCheck Attribute. 
     1157            #if this inherits Struct 
     1158            #   sw.write('\nint _ih_invariantGuard;\n\n') 
     1159            #else if not .baseClass or .baseClass.isFromBinaryLibrary 
     1160            #   sw.write('\nprotected int _ih_invariantGuard;\n\n') 
     1161                 
    11521162        if .compiler.options['contracts'] <> 'methods' 
    11531163            return 
    11541164        sw.write('\n[.sharpInvariantVisibility] void invariant_[.rootName]() {\n') 
     
    17151725                    if param.isOut 
    17161726                        sharpInit = param.type.sharpInit 
    17171727                        if not sharpInit.length 
    1718                             # TODO/HACK: yes we need something like this (or a way to convice C# that the out param reference in `finally` really is okay), 
     1728                            # TODO/HACK: yes we need something like this (or a way to convince C# that the out param reference in `finally` really is okay), 
    17191729                            # but it should be something less hackish, like an attribute 
    17201730                            sharpInit = 'DateTime.Today' 
    17211731                        sw.write('[param.sharpName] = [sharpInit];') 
     
    17311741                    continue 
    17321742                stmt.writeSharpStmt(sw) 
    17331743            if willEnsure 
    1734                 if not stmt inherits ReturnStmt and not stmt inherits ThrowStmt 
    1735                     sw.write('_lh_canEnsure = true;\n') 
    1736                 sw.dedentAndWrite('} finally { // ensure\n') 
    1737                 sw.indentAndWrite('if (_lh_canEnsure) {\n') 
    1738                 sw.indent 
    1739                 _ensurePart.writeSharpDef(sw) 
    1740                 sw.dedentAndWrite('}\n') 
    1741                 sw.dedentAndWrite('}\n') 
     1744                suppressInvariantCheck = any for a in .attributes get a.name == 'SuppressInvariantCheckAttribute'  
     1745                if suppressInvariantCheck 
     1746                    sw.dedentAndWrite('} finally { // ensure\n') 
     1747                    sw.indentAndWrite('// Invariant Check suppressed by Cobra.Core.SuppressInvariantCheckAttribute\n') 
     1748                    sw.dedentAndWrite('}\n') 
     1749                else 
     1750                    if not stmt inherits ReturnStmt and not stmt inherits ThrowStmt 
     1751                        sw.write('_lh_canEnsure = true;\n') 
     1752                    sw.dedentAndWrite('} finally { // ensure\n') 
     1753                    sw.indentAndWrite('if (_lh_canEnsure) {\n') 
     1754                    sw.indent 
     1755                    _ensurePart.writeSharpDef(sw) 
     1756                    sw.dedentAndWrite('}\n') # if 
     1757                    sw.dedentAndWrite('}\n') # finally 
     1758                     
    17421759            if .compiler.hasDetailedStackTraceOption 
    17431760                .writeDSTTail(sw) 
    17441761            .writeSharpImpFooter(sw) 
     
    17471764            sw.write('\n') 
    17481765        finally 
    17491766            .compiler.codeMemberStack.pop 
    1750  
     1767             
    17511768    def writeSharpImpHeader(sw as CurlyWriter) 
    17521769        pass 
    17531770         
  • Source/Cobra.Core/Misc.cobra

    
            
     
    4545        has AttributeUsage(AttributeTargets.Method, allowMultiple=false) 
    4646        pass 
    4747 
     48    class SuppressInvariantCheckAttribute inherits Attribute 
     49        has AttributeUsage(AttributeTargets.Method, allowMultiple=false) 
     50        """ 
     51        Use to suppress Invariant checking on a method. 
     52        Place on invariant or initializer helper methods to suppress invariant checking when invariant 
     53        checking is unnecessary or invariant not yet established. 
     54        """ 
     55        pass 
     56         
    4857    class CobraDirectString is extern 
    4958        """ 
    5059        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 
     2# put on any methods (invariant helpers and initializer helpers) that 
     3# should not have the invariants checked after their execution 
     4class Base 
     5    var icb = 0 
     6    var countB = 0 
     7     
     8    cue init 
     9        base.init 
     10        .countB = 1 
     11        print 'end init of Base' 
     12 
     13    def _m1 as bool has SuppressInvariantCheck 
     14        print 'helper invariant of Base (_m1)' 
     15        .icb += 1 
     16        return true 
     17 
     18    invariant 
     19        _m1 
     20        .icb == .countB 
     21 
     22class Derived inherits Base 
     23    var icd = 0 
     24    var countD = 0 
     25     
     26    cue init 
     27        base.init 
     28        assert .icb == 1 
     29        assert .icd == 0 
     30        .chk 
     31        assert .icb == 1 
     32        assert .icd == 0 
     33        .countD = 1 
     34        .countB = 2 
     35        print 'end init of Derived' 
     36         
     37    def chk has SuppressInvariantCheck 
     38        print 'in initHelper' 
     39         
     40    def _m2 as bool has SuppressInvariantCheck 
     41        print 'helper invariant of Derived (_m2)' 
     42        .icd += 1 
     43        return true 
     44 
     45    invariant 
     46        _m2 
     47        .icd == .countD 
     48         
     49class P      
     50    def main is shared 
     51        Derived() 
  • Tests/340-contracts/930-invariant-calls-notSuppressed.cobra

     
     1# Chking base behaviour without invariant suppression 
     2# put on any methods (invariant helpers and initializer helpers) that 
     3# should not have the invariants checked after their execution 
     4class Base 
     5    var icb = 0 
     6    var countB = 0 
     7     
     8    cue init 
     9        base.init 
     10        .countB = 1 
     11        print 'end init of Base' 
     12 
     13    def _m1 as bool  
     14        print 'helper invariant of Base (_m1)' 
     15        .icb += 1 
     16        return true 
     17 
     18    invariant 
     19        _m1 
     20        .icb == .countB 
     21 
     22class Derived inherits Base 
     23    var icd = 0 
     24    var countD = 0 
     25     
     26    cue init 
     27        base.init 
     28        assert .icb == 1 
     29        assert .icd == 0 
     30        .countB = 3 
     31        .countD = 1 
     32        .chk 
     33        assert .icb == 3 
     34        assert .icd == 1 
     35        .countD = 2 
     36        .countB = 5 
     37        print 'end init of Derived' 
     38         
     39    def chk  
     40        print 'in initHelper' 
     41         
     42    def _m2 as bool  
     43        print 'helper invariant of Derived (_m2)' 
     44        .icd += 1 
     45        return true 
     46 
     47    invariant 
     48        _m2 
     49        .icd == .countD 
     50         
     51class P      
     52    def main is shared 
     53        Derived()