<commit_before>'''
Created on 2013-09-21

@author: gehan
'''
from abc import ABCMeta, abstractmethod
from .property import Property
import os
#from atomic_state_property import AtomicStateProperty

from disambiguate import Disambiguator
from core.himesis_utils import disjoint_model_union
from copy import deepcopy
from core.himesis_utils import graph_to_dot
from core.himesis_utils import load_class

from t_core.messages import Packet
from t_core.matcher import Matcher

import time
import PropertyVerification

from profiler import *

class StateProperty(Property):
    '''
    classdocs
    '''
    __metaclass__=ABCMeta
    hasDefaultVerifResult=None
    verifResult=None

    def __init__(self):
        Property.__init__(self)
        self.counterexamples = []


        self.NOT_CHECKED = "Not checked"
        self.NO_ISOLATED = "Isolated did not match"
        self.NO_CONNECTED = "Connected did not match"
        self.NO_COMPLETE = "Complete did not match"
        self.COMPLETE_FOUND = "The complete property was found"

        #detail the status of the property
        self.status = self.NOT_CHECKED

        self.disambig = Disambiguator(0)

    def SETverifResult (self, boolres):
        self.hasDefaultVerifResult= True
        self.verifResult=boolres
        
    def GETverifResult(self):
        return self.verifResult
    
    def GEThasDefaultVerifResult (self):
        return self.hasDefaultVerifResult
    
    def resetVerifResultToFalse (self):
        self.verifResult=False
        self.hasDefaultVerifResult=False
        
    @abstractmethod 
    def verify (self, state, StateSpace=None):
        #I added a second parameter with a default value of none because 
        #   the only subclass of StateProperty that will need this second parameter is AtomicStateProperty
        #   (its verify method will need StateSpace.verbosity and StateSpace.verifiedStateCache)
        pass
    
    @staticmethod
    def parseStateName2RuleNames (stateName):
        result=stateName.split('_')
        return result[1:]
      
    @staticmethod    
    def checkRuleReachability (ruleName2Check, StateSpace):

        ts0 = time.time()
        reachable=False
        for pathCond in StateSpace.get_path_conditions():
            rulesInPathCond=StateProperty.parseStateName2RuleNames(pathCond.name)
            if ruleName2Check in rulesInPathCond:
                reachable= True
                break
        ts1 = time.time()
        if reachable:
            print("\nRule "+ruleName2Check+ " is reachable through at least one path condition !")
        else:
            print("\nRule "+ruleName2Check+ " is not reachable through any path condition !")
        print("Time to verify reachability: " + str(ts1 - ts0))
        return reachable
        
    @staticmethod
    def getAllAtomicStatePropsInStateProp (sprop, listResult):
        result=listResult
        if isinstance(sprop, PropertyVerification.atomic_state_property.AtomicStateProperty) :
            result.append(sprop)
        else :
            operands= sprop.getAllOperands() #gets all operands, even if they are duplicates
            #AndStateProperty(AndStateProperty(atomic1,atomic2),atomic1).getAllOperands() returns a list of size 2 with an AndStateProperty and an AtomicStateProperty
            for op in operands:
                StateProperty.getAllAtomicStatePropsInStateProp(op,result)
        return result
    
    @staticmethod
    def twoOrMoreAtomicPropsAreTrue (atomicProps):
        if (len(atomicProps)>1):
            ctr=0
            for prop in atomicProps:
                if (prop.GETverifResult()==True) and (prop.GEThasDefaultVerifResult()==True) and (len(prop.get_matchesOfTotal())>0):
                    ctr=ctr+1
                    if (ctr == 2):
                        return True
        return False
    
    @staticmethod
    def CheckConsistencyFunc (atomicProps):
        listOfListsOfMatches=[]
        for prop in atomicProps:
            if ((len(prop.get_matchesOfTotal())>0) and (prop.GEThasDefaultVerifResult()==True) and (prop.GETverifResult()==True)):
                curlist=[]
                for dict1 in prop.get_matchesOfTotal():
                    curlist.append(dict1.values())
                listOfListsOfMatches.append(curlist)
        
        for atpropindex in range(len(listOfListsOfMatches)):
                curmatches = listOfListsOfMatches[atpropindex]
                for match in curmatches:
                    for anotherAtPropIndex in range(len(listOfListsOfMatches)):
                        if anotherAtPropIndex==atpropindex :
                            continue
                        foundoverlap=False
                        curMatchesInAnotherAtProp = listOfListsOfMatches[anotherAtPropIndex]
                        for matchInAnotherAtProp in curMatchesInAnotherAtProp:
                            if (len(set(match).intersection(set(matchInAnotherAtProp)))>0):
                                foundoverlap=True
                                break
                        if foundoverlap==False:
                            print('Pivots of the state property are not consistent :(')
                            return False    
        #print('Pivots of the state property are consistent :)')
        return True
    
    @staticmethod      
    def break_down_pc_name(pcName):
        nameList = []
        for token in pcName.split("_"):
            token = token.split("-")[0]
            nameList.append(token)
        return nameList


    @do_cprofile
    def verifyCompositeStateProperty(self, StateSpace, stateprop):
        """
        Inputs: 
        1- StateSpace: the complete state space to be iterated
        2- stateprop: the StateProperty that we'd like to prove "for all" states, 
                    i.e., proving that its true per state and that t its true for all states
        
        Steps performed by function:
        1- Gets all the composite AtomicStateProperties in stateprop.
        2- build the united graph from the symbolic state
        2- iterates on each state of StateSpace, & for each state the following steps are done:
            a- Build cacheIsolatedPatternMatches which is a lookup cache containing the name of each AtomiStateProperty retrieved from step 1, and whether or not their isolated patterns have a match in the current state or not.
            b- While building cacheIsolatedPatternMatches, set the default verification result of AtomicStateProperties in the verifiedStateCache or those that have no matches for their isolated patterns to true, 
                i.e. their verification result will be set to true without having to check their connected and complete patterns.
            c- After building cacheIsolatedPatternMatches, if non of the cache keys has a 'true' (i.e. non of the composite AtomicStateProperties have a match for their Isolated patterns), then do not collapse the state and call stateprop.verify function on the uncollapsed state. (For efficiency & because collapsing is expensive, we collapse the current state only if a match for IsolatedLHS exists for at least one of the composite AtomicStateProperties)
            d-     ...else, collapse the state into a resultant set of collapsed states. For each collapsed state in the resultant set of states, call stateprop.verify on the collapsed state. This time the verify function will match the connected pattern then the complete pattern.
            e- If the compositeStatePattern does not hold for one state then return false. Else, return true
        """        
        AtomicStatePropsInStateProp=StateProperty.getAllAtomicStatePropsInStateProp(stateprop,[])
        #print ("Started running function verifyCompositeStateProperty of class StateProperty")
        state_index = 0
        found_counterexample=False
        curVerifResult=False

        pcs_failed = []

        #ensure that the property's precondition matched at least one path condition
        #otherwise, there is an issue (different metamodels, ...)
        property_isolated_matched = False<commit_msg>Disable profiling.<commit_after>'''
Created on 2013-09-21

@author: gehan
'''
from abc import ABCMeta, abstractmethod
from .property import Property
import os
#from atomic_state_property import AtomicStateProperty

from disambiguate import Disambiguator
from core.himesis_utils import disjoint_model_union
from copy import deepcopy
from core.himesis_utils import graph_to_dot
from core.himesis_utils import load_class

from t_core.messages import Packet
from t_core.matcher import Matcher

import time
import PropertyVerification

from profiler import *

class StateProperty(Property):
    '''
    classdocs
    '''
    __metaclass__=ABCMeta
    hasDefaultVerifResult=None
    verifResult=None

    def __init__(self):
        Property.__init__(self)
        self.counterexamples = []


        self.NOT_CHECKED = "Not checked"
        self.NO_ISOLATED = "Isolated did not match"
        self.NO_CONNECTED = "Connected did not match"
        self.NO_COMPLETE = "Complete did not match"
        self.COMPLETE_FOUND = "The complete property was found"

        #detail the status of the property
        self.status = self.NOT_CHECKED

        self.disambig = Disambiguator(0)

    def SETverifResult (self, boolres):
        self.hasDefaultVerifResult= True
        self.verifResult=boolres
        
    def GETverifResult(self):
        return self.verifResult
    
    def GEThasDefaultVerifResult (self):
        return self.hasDefaultVerifResult
    
    def resetVerifResultToFalse (self):
        self.verifResult=False
        self.hasDefaultVerifResult=False
        
    @abstractmethod 
    def verify (self, state, StateSpace=None):
        #I added a second parameter with a default value of none because 
        #   the only subclass of StateProperty that will need this second parameter is AtomicStateProperty
        #   (its verify method will need StateSpace.verbosity and StateSpace.verifiedStateCache)
        pass
    
    @staticmethod
    def parseStateName2RuleNames (stateName):
        result=stateName.split('_')
        return result[1:]
      
    @staticmethod    
    def checkRuleReachability (ruleName2Check, StateSpace):

        ts0 = time.time()
        reachable=False
        for pathCond in StateSpace.get_path_conditions():
            rulesInPathCond=StateProperty.parseStateName2RuleNames(pathCond.name)
            if ruleName2Check in rulesInPathCond:
                reachable= True
                break
        ts1 = time.time()
        if reachable:
            print("\nRule "+ruleName2Check+ " is reachable through at least one path condition !")
        else:
            print("\nRule "+ruleName2Check+ " is not reachable through any path condition !")
        print("Time to verify reachability: " + str(ts1 - ts0))
        return reachable
        
    @staticmethod
    def getAllAtomicStatePropsInStateProp (sprop, listResult):
        result=listResult
        if isinstance(sprop, PropertyVerification.atomic_state_property.AtomicStateProperty) :
            result.append(sprop)
        else :
            operands= sprop.getAllOperands() #gets all operands, even if they are duplicates
            #AndStateProperty(AndStateProperty(atomic1,atomic2),atomic1).getAllOperands() returns a list of size 2 with an AndStateProperty and an AtomicStateProperty
            for op in operands:
                StateProperty.getAllAtomicStatePropsInStateProp(op,result)
        return result
    
    @staticmethod
    def twoOrMoreAtomicPropsAreTrue (atomicProps):
        if (len(atomicProps)>1):
            ctr=0
            for prop in atomicProps:
                if (prop.GETverifResult()==True) and (prop.GEThasDefaultVerifResult()==True) and (len(prop.get_matchesOfTotal())>0):
                    ctr=ctr+1
                    if (ctr == 2):
                        return True
        return False
    
    @staticmethod
    def CheckConsistencyFunc (atomicProps):
        listOfListsOfMatches=[]
        for prop in atomicProps:
            if ((len(prop.get_matchesOfTotal())>0) and (prop.GEThasDefaultVerifResult()==True) and (prop.GETverifResult()==True)):
                curlist=[]
                for dict1 in prop.get_matchesOfTotal():
                    curlist.append(dict1.values())
                listOfListsOfMatches.append(curlist)
        
        for atpropindex in range(len(listOfListsOfMatches)):
                curmatches = listOfListsOfMatches[atpropindex]
                for match in curmatches:
                    for anotherAtPropIndex in range(len(listOfListsOfMatches)):
                        if anotherAtPropIndex==atpropindex :
                            continue
                        foundoverlap=False
                        curMatchesInAnotherAtProp = listOfListsOfMatches[anotherAtPropIndex]
                        for matchInAnotherAtProp in curMatchesInAnotherAtProp:
                            if (len(set(match).intersection(set(matchInAnotherAtProp)))>0):
                                foundoverlap=True
                                break
                        if foundoverlap==False:
                            print('Pivots of the state property are not consistent :(')
                            return False    
        #print('Pivots of the state property are consistent :)')
        return True
    
    @staticmethod      
    def break_down_pc_name(pcName):
        nameList = []
        for token in pcName.split("_"):
            token = token.split("-")[0]
            nameList.append(token)
        return nameList


    #@do_cprofile
    def verifyCompositeStateProperty(self, StateSpace, stateprop):
        """
        Inputs: 
        1- StateSpace: the complete state space to be iterated
        2- stateprop: the StateProperty that we'd like to prove "for all" states, 
                    i.e., proving that its true per state and that t its true for all states
        
        Steps performed by function:
        1- Gets all the composite AtomicStateProperties in stateprop.
        2- build the united graph from the symbolic state
        2- iterates on each state of StateSpace, & for each state the following steps are done:
            a- Build cacheIsolatedPatternMatches which is a lookup cache containing the name of each AtomiStateProperty retrieved from step 1, and whether or not their isolated patterns have a match in the current state or not.
            b- While building cacheIsolatedPatternMatches, set the default verification result of AtomicStateProperties in the verifiedStateCache or those that have no matches for their isolated patterns to true, 
                i.e. their verification result will be set to true without having to check their connected and complete patterns.
            c- After building cacheIsolatedPatternMatches, if non of the cache keys has a 'true' (i.e. non of the composite AtomicStateProperties have a match for their Isolated patterns), then do not collapse the state and call stateprop.verify function on the uncollapsed state. (For efficiency & because collapsing is expensive, we collapse the current state only if a match for IsolatedLHS exists for at least one of the composite AtomicStateProperties)
            d-     ...else, collapse the state into a resultant set of collapsed states. For each collapsed state in the resultant set of states, call stateprop.verify on the collapsed state. This time the verify function will match the connected pattern then the complete pattern.
            e- If the compositeStatePattern does not hold for one state then return false. Else, return true
        """        
        AtomicStatePropsInStateProp=StateProperty.getAllAtomicStatePropsInStateProp(stateprop,[])
        #print ("Started running function verifyCompositeStateProperty of class StateProperty")
        state_index = 0
        found_counterexample=False
        curVerifResult=False

        pcs_failed = []

        #ensure that the property's precondition matched at least one path condition
        #otherwise, there is an issue (different metamodels, ...)
        property_isolated_matched = False
{'fraction_non_alphanumeric': 0.0594327990135635, 'fraction_numerical': 0.005055487053020962, 'mean_word_length': 2.4490750584733147, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4213264', 'n_tokens_mistral': 4210, 'n_tokens_neox': 4040, 'n_words': 1368}