Skip to content

Commit 0bdd19b

Browse files
shaunazzopardishaunazzopardi
committed
repaired bug causing assertions to be propagated beyond their truth holding + added syntatic DEA reductions
1 parent 00f2193 commit 0bdd19b

File tree

6 files changed

+50
-46
lines changed

6 files changed

+50
-46
lines changed

‎src/Main-online-smt.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ main =
7070
acfas = map (\cfa -> abstract cfa (getEventsFromDEA dea)) outCFAs
7171
acfaText = (foldr (++) "" (map display (acfas)))
7272
amssText = (foldr (++) "" (map display amss))
73-
residualDEA = bothResiduals amss dea
73+
residualDEA = reachibilityReduction $ bothResiduals amss dea
7474
writeFile outFile cfaText
7575
`failWith` ("Cannot write to CFA file <"++outFile++">")
7676
putStrLn ("Created residual CFA file <"++outFile++">")

‎src/ResidualAnalysis.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,12 @@
1111
-- See the License for the specific language governing permissions and
1212
-- limitations under the License.
1313

14-
module ResidualAnalysis (module ResidualAnalysis.AbstractCFA, module ResidualAnalysis.IntraProceduralAbstractMonitoredSystem, module ResidualAnalysis.ResidualAnalysis) where
14+
module ResidualAnalysis (module ResidualAnalysis.AbstractCFA, module ResidualAnalysis.IntraProceduralAbstractMonitoredSystem, module ResidualAnalysis.ResidualAnalysis, module ResidualAnalysis.DEAResiduals) where
1515

1616
import ResidualAnalysis.IntraProceduralAbstractMonitoredSystem
1717
import ResidualAnalysis.AbstractCFA
1818
import ResidualAnalysis.ResidualAnalysis
19+
import ResidualAnalysis.DEAResiduals hiding (usesEvent)
1920

2021
import CFA
2122
import SMT

‎src/DEA/DEAResiduals.hs‎ renamed to ‎src/ResidualAnalysis/DEAResiduals.hs‎

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
1-
module StaticAnalysis.DEAResiduals where
1+
module ResidualAnalysis.DEAResiduals where
22

33
import qualified DEA.DEA as DEA
44
import qualified CFG.CFG as CFG
5-
import qualified StaticAnalysis.ICFG as ICFG
6-
import qualified StaticAnalysis.Util
75
import Solidity.Solidity
86
import Data.List
7+
import Debug.Trace
98

109

1110

@@ -54,11 +53,10 @@ module StaticAnalysis.DEAResiduals where
5453
usesEvent ((DEA.Transition q _ (DEA.GCL e _ _)):rest) q' e' = (q == q' && e == e') || (usesEvent (rest) q e)
5554

5655
reachibilityReduction :: DEA.DEA -> DEA.DEA
57-
reachibilityReduction dea = let statesReachableFromInitialState = statesAfter dea (DEA.initialStates dea)
58-
badAfterStates = [state | state <- statesReachableFromInitialState, badAfter dea state]
59-
goodEntryPointStates = [state | state <- statesReachableFromInitialState, goodEntryPoint dea state]
56+
reachibilityReduction dea = let badAfterStates = [state | state <- DEA.allStates dea, badAfter dea state]
57+
goodEntryPointStates = [state | state <- DEA.allStates dea, goodEntryPoint dea state]
6058
usefulStates = badAfterStates ++ goodEntryPointStates
61-
uselessStates = DEA.allStates dea \\ usefulStates
59+
uselessStates = (DEA.allStates dea \\ usefulStates)
6260
usefulTransitions = [transition | transition <- DEA.transitions dea, elem (DEA.src transition) usefulStates, elem (DEA.dst transition) usefulStates]
6361
in DEA.DEA{
6462
DEA.daeName = DEA.daeName dea,
@@ -70,23 +68,23 @@ module StaticAnalysis.DEAResiduals where
7068
}
7169

7270
badAfter :: DEA.DEA -> DEA.State -> Bool
73-
badAfter dea state = (pathBetween dea (head (DEA.initialStates dea)) state) && ((statesAfter dea [state]) \\ (DEA.badStates dea) /= [])
71+
badAfter dea state = (elem state (statesAfter dea (DEA.initialStates dea))) && ([b | b <- (DEA.badStates dea), elem b (statesAfter dea [state])] /= [])
7472

7573
goodEntryPoint :: DEA.DEA -> DEA.State -> Bool
76-
goodEntryPoint dea state = (pathBetween dea (head (DEA.initialStates dea)) state
77-
&& elem state (DEA.acceptanceStates dea))
78-
|| (not (badAfter dea state)
79-
&& [src | DEA.Transition src state _ <- DEA.transitions dea, badAfter dea state] /= [])
74+
goodEntryPoint dea state = (elem state (statesAfter dea (DEA.initialStates dea)))
75+
&& (elem state (DEA.acceptanceStates dea)
76+
|| (not (badAfter dea state)
77+
&& [DEA.src t | t <- DEA.transitions dea, badAfter dea (DEA.src t)] /= []))
8078

8179
pathBetween :: DEA.DEA -> DEA.State -> DEA.State -> Bool
82-
pathBetween dea q q' = elem q (statesAfter dea [q])
80+
pathBetween dea q qq = elem qq (statesAfter dea [q])
8381

8482
statesAfter :: DEA.DEA -> [DEA.State] -> [DEA.State]
8583
statesAfter dea [] = []
8684
statesAfter dea states = let afterOneStep = nub $ ((oneStep dea states) ++ states)
87-
in if(afterOneStep \\ (nub $ states) /= [])
85+
in if(afterOneStep \\ states /= [])
8886
then statesAfter dea afterOneStep
8987
else afterOneStep
9088

9189
oneStep :: DEA.DEA -> [DEA.State] -> [DEA.State]
92-
oneStep dea states = [dst | src <- states, DEA.Transition src dst _ <- DEA.transitions dea]
90+
oneStep dea states = [DEA.dst t | s <- states, t <- DEA.transitions dea, DEA.src t == s]

‎src/ResidualAnalysis/ResidualAnalysis.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ module ResidualAnalysis.ResidualAnalysis where
6060
guardAlwaysTrue' :: AMS -> DEA.Transition -> Bool
6161
guardAlwaysTrue' ams qt = let matches = [ev | ev <- evolutions ams, deaTrans ev == Just qt, (cfaTrans ev) /= Nothing]
6262
statesFromWhichQTIsNotTheOnlyPossibility = [(AMS.from ev, (outgoingAMSTransitions ams (AMS.from ev) (DEA.event $ label qt))) | ev <- matches, (length (outgoingAMSTransitions ams (AMS.from ev) (DEA.event $ label qt))) > 1]
63-
in trace (display qt ++ "__" ++ (show statesFromWhichQTIsNotTheOnlyPossibility)) (statesFromWhichQTIsNotTheOnlyPossibility == [])
63+
in (statesFromWhichQTIsNotTheOnlyPossibility == [])
6464

6565
outgoingAMSTransitions :: AMS -> AMSConfig -> DEA.Event -> [AMSTransition]
6666
outgoingAMSTransitions ams c event = [ev | ev <- evolutions ams, AMS.from ev == c, usesEvent ev event]

‎src/SMT/SMTLib2.hs‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ module SMT.SMTLib2 where
1414
import Text.Parsec.String
1515
import Data.Char hiding (DecimalNumber)
1616
import Data.List
17+
import Debug.Trace
1718

1819
import Parseable
1920
import Solidity.Solidity
@@ -32,6 +33,7 @@ module SMT.SMTLib2 where
3233
--------------------------------------------------------------------------------
3334

3435
data BoolVal = BoolVal String
36+
| BoolValRel GenericRelation
3537
| BoolVar String deriving (Eq, Ord, Show)
3638
-----------------
3739
--data GenericValues = Val String
@@ -44,17 +46,20 @@ module SMT.SMTLib2 where
4446

4547
instance Parseable BoolVal where
4648
display (BoolVal b) = b
49+
display (BoolValRel b) = display b
4750
display (BoolVar b) = b
4851
--------------------------------------------------------------------------------
4952
instance VarsOf BoolVal where
5053
varsOf (BoolVal b) = []
54+
varsOf (BoolValRel b) = varsOf b
5155
varsOf (BoolVar b) = [b]
5256
--------------------------------------------------------------------------------
5357

5458
--------------------------------------------------------------------------------
5559
--we should also allow HexVal
5660

57-
data NumVal = IntVal String
61+
data NumVal = NumValRel GenericRelation
62+
| IntVal String
5863
| RealVal String
5964
| IntVar String
6065
| RealVar String deriving (Eq, Ord, Show)
@@ -63,12 +68,14 @@ module SMT.SMTLib2 where
6368

6469
instance Parseable NumVal where
6570
-- parser = --whitespace *> (SolidityCode <$> parser) <* whitespace <* eof
71+
display (NumValRel i) = display i
6672
display (IntVal i) = i
6773
display (RealVal d) = d
6874
display (IntVar v) = v
6975
display (RealVar v) = v
7076
--------------------------------------------------------------------------------
7177
instance VarsOf NumVal where
78+
varsOf (NumValRel i) = varsOf i
7279
varsOf (IntVal i) = []
7380
varsOf (RealVal d) = []
7481
varsOf (IntVar v) = [v]
@@ -396,6 +403,8 @@ module SMT.SMTLib2 where
396403
-------------
397404
instance Parseable Assert where
398405
display (Assert rel) = "(assert " ++ display rel ++ ")"
406+
instance VarsOf Assert where
407+
varsOf (Assert rel) = varsOf rel
399408
--------------------------------------------------------------------------------
400409

401410
data Z3Construct = Z3Sort SortDeclaration | Z3Dec VarDeclaration | Z3Assert Assert deriving (Eq, Ord, Show)

0 commit comments

Comments
 (0)