Skip to content

Commit 590a520

Browse files
bramvdbogaerdebramvdbogaerde
committed
misc(simpleactor): some debugging + limit graphToSet abstraction so that it does not keep using the graphs
1 parent d364c81 commit 590a520

12 files changed

Lines changed: 123 additions & 62 deletions

File tree

‎analyses/simpleactor/programs/benchmarks/actors/erlang/soter/safe_send.erl‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
-module(safe_send).
2-
-epxort([main/0]).
2+
-export([main/0]).
33

44
-uncoverable("assert_actor_reference_failed > 0").
55

66
main() ->
7+
monarch:debug(here),
78
ME = self(),
9+
monarch:debug(ME),
810
S = spawn(fun()-> receive {_,X} -> ME ! ok, server(X) end end),
911
S ! {init, zero},
1012
receive ok -> ok end,
@@ -14,7 +16,8 @@ main() ->
1416

1517
server(State) ->
1618
receive
17-
{X, P} -> monarch:assert_actor_reference(P, assert_actor_reference_failed),
19+
{X, P} -> monarch:debug(P),
20+
monarch:assert_actor_reference(P, assert_actor_reference_failed),
1821
P ! State, % This call would throw an exception if matching P=zero.
1922
server(X);
2023
bye -> monarch:label(stop_server), ok

‎analyses/simpleactor/programs/benchmarks/actors/erlang/soter/stutter.erl‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
-module(stutter).
2+
23
-export([main/0]).
34

4-
-uncoverable("abonormal_a > 0").
5+
-uncoverable("abnormal_a > 0").
56

67
main() ->
78
P = spawn(fun()-> stutter(fun(Msg)-> dosmt(Msg) end) end),

‎analyses/simpleactor/src/Analysis/SimpleActor/ErlangPrimitives.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ import Domain.Core.PairDomain (cons)
4949
import Analysis.Monad.AbstractCount (countIncrement, MonadAbstractCount (currentCount))
5050
import Control.Monad.IO.Class (liftIO)
5151
import Lattice.ConstantPropagationLattice (CP)
52+
import Data.List (intercalate)
5253

5354
------------------------------------------------------------
5455
-- Monadic contexts
@@ -157,7 +158,7 @@ erlangPrimitives =
157158
-- Debugging monarch
158159
("monarch:debug_label/2", prim $ const $ prim2 $ \v -> return . symbols >=> mapM_ (liftIO . putStrLn . ((("count>>" ++ " " ++ show v) ++) . show) <=< currentCount . MailboxLabel) >=> const (return nil)),
159160
("monarch:debug/1", prim $ const $ prim1 $ \v -> liftIO $ putStrLn ("debug>> " ++ show v) $> v),
160-
161+
("monarch:fail_analysis_missing_export/1", prim $ const $ prim1 $ \v -> error $ "analysis failed: missing export, one of these: " ++ intercalate "," (map show $ Set.toList (symbols v))),
161162
-- I/O primitives
162163
("io:format/2", prim $ const $ const $ return nil),
163164
("io:format/1", prim $ const $ const $ return nil)

‎analyses/simpleactor/src/Analysis/SimpleActor/Fixpoint/Common.hs‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -77,23 +77,30 @@ newtype ActorResOut = ActorResOut ActorRef deriving (Ord, Eq, Show)
7777
------------------------------------------------------------
7878

7979
-- | Context for address allocations, function calls and actor references.
80-
data AdrCtx = AdrCtx [Span] -- k-cfa call sites
81-
Int -- ^ max number of elements in k-cfa
82-
ActorCtx -- ^ actor specific context sensitivity
83-
deriving (Ord, Eq, Show)
80+
data AdrCtx = AdrCtx [Span] -- k-cfa call sites
81+
Int -- ^ max number of elements in k-cfa
82+
ActorCtx -- ^ actor specific context sensitivity
83+
| InsensitiveCtx -- context insensitive analysis
84+
deriving (Ord, Eq, Show)
8485

8586
-- | Context specific to the actor analysis
86-
data ActorCtx = ActorCtx ActorRef | Empty deriving (Ord, Eq, Show)
87+
data ActorCtx = ActorCtx ActorRef
88+
| Empty
89+
deriving (Ord, Eq, Show)
8790

8891
-- | k-cfa instance for 'SimpleActorContext'
8992
instance SimpleActorContext AdrCtx where
9093
pushCallSite s (AdrCtx callsites maxCallsites actCtx) = AdrCtx callsites' maxCallsites actCtx
9194
where callsites' = take maxCallsites (s : callsites)
95+
pushCallSite _ InsensitiveCtx = InsensitiveCtx
9296

9397
-- | The initial context
9498
initialContext :: Int -> AdrCtx
9599
initialContext maxCallsites = AdrCtx [] maxCallsites Empty
96100

101+
-- | An initial context for a context insensitive analysis
102+
insensitiveContext :: AdrCtx
103+
insensitiveContext = InsensitiveCtx
97104

98105
------------------------------------------------------------
99106
-- Initial dynamic environment

‎analyses/simpleactor/src/Analysis/SimpleActor/Fixpoint/ModularModConc.hs‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,8 @@ spawnWL :: (Ord cmp, ComponentTrackingM m cmp, WorkListM m cmp) => cmp -> m ()
5959
spawnWL cmp = ifM (Set.member cmp <$> C.components) (return ()) (C.spawn cmp >> add cmp)
6060

6161
instance (Monad m, ComponentTrackingM m ActorRef, WorkListM m ActorRef) => MonadSpawn ActorVlu K (StateT AnalysisState m) where
62-
spawn expr env ctx = (modify (over pidToProcess (Map.insert pid (expr, env'))) $> pid) <* spawnWL pid
63-
where pid = Pid expr ctx
62+
spawn expr env _ = (modify (over pidToProcess (Map.insert pid (expr, env'))) $> pid) <* spawnWL pid
63+
where pid = Pid expr InsensitiveCtx
6464
env' = env -- HashMap.restrictKeys env (fv expr)
6565

6666

@@ -165,11 +165,11 @@ analyze' labelCounts maxSteps expr = fmap toAnalysisResult $ inter labelCounts m
165165
& runStoreT @ActorSto @ActorAdr @(StoreVal ActorVlu) initialGlobalStore
166166
& runWithMapping @ActorResOut @ActorRes
167167
& runWithMapping @Sequential.CountMax @LabelCounts
168-
& runWithDependencyTracking @ActorRef @ActorVarAdr
169-
& runWithDependencyTracking @ActorRef @ActorRef
170-
& runWithDependencyTracking @ActorRef @ActorResOut
171-
& runWithDependencyTracking @ActorRef @Sequential.CountMax
172-
& runWithDependencyTracking @ActorRef @(MailboxDep ActorRef PMB)
168+
& runWithDependencyTracingTracking @ActorRef @ActorVarAdr
169+
& runWithDependencyTracingTracking @ActorRef @ActorRef
170+
& runWithDependencyTracingTracking @ActorRef @ActorResOut
171+
& runWithDependencyTracingTracking @ActorRef @Sequential.CountMax
172+
& runWithDependencyTracingTracking @ActorRef @(MailboxDep ActorRef PMB)
173173
& runWithDependencyTriggerTrackingT @ActorRef @ActorRef
174174
& runWithDependencyTriggerTrackingT @ActorRef @Sequential.CountMax
175175
& runWithDependencyTriggerTrackingT @ActorRef @ActorVarAdr

‎analyses/simpleactor/src/Analysis/SimpleActor/Fixpoint/SequentialModConc.hs‎

Lines changed: 39 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ type SequentialT m = MonadStack '[
9191
type UncachedSequentialT m =
9292
MonadStack '[
9393
AbstractCountT MailboxLabel BoundedCount,
94-
AbstractCountT SequentialCmp AbstractCount,
94+
-- AbstractCountT SequentialCmp AbstractCount,
9595
JoinT
9696
] m
9797

@@ -107,8 +107,8 @@ type InterAnalysisM m = (MonadSchemeStore m,
107107
-- To accurately track these, abstract counts related to components
108108
-- need to be tracked. And if component count > 1 then the label
109109
-- count needs to be marked infinite as well. (otherwise the result is unsound)
110-
MapM CmpCountIn (CountMap' SequentialCmp AbstractCount) m,
111-
MapM CmpCountOut (CountMap' SequentialCmp AbstractCount) m,
110+
-- MapM CmpCountIn (CountMap' SequentialCmp AbstractCount) m,
111+
-- MapM CmpCountOut (CountMap' SequentialCmp AbstractCount) m,
112112
WorkListM m SequentialCmp,
113113
ComponentTrackingM m SequentialCmp,
114114
DependsOn m SequentialCmp '[
@@ -117,8 +117,8 @@ type InterAnalysisM m = (MonadSchemeStore m,
117117
Pid Exp K,
118118
CountIn,
119119
CountOut,
120-
CmpCountIn,
121-
CmpCountOut
120+
CmpCountIn
121+
-- CmpCountOut
122122
],
123123
-- MonadMailbox ActorVlu m,
124124
MonadMailbox' ActorRef PMB m,
@@ -142,8 +142,12 @@ instance (CtxM m K, MonadActorLocal ActorVlu m, Monad m) => CtxM (LocalMailboxT
142142
withCtx f m = do
143143
ctx <- getCtx
144144
lowerM (withCtx (const (f ctx))) m
145-
getCtx = do (AdrCtx callSites maxCallSites _) <- upperM getCtx
146-
AdrCtx callSites maxCallSites . ActorCtx <$> getSelf
145+
getCtx = do ctx <- upperM getCtx
146+
case ctx of
147+
(AdrCtx callSites maxCallSites _) ->
148+
AdrCtx callSites maxCallSites . ActorCtx <$> getSelf
149+
InsensitiveCtx ->
150+
return InsensitiveCtx
147151

148152
------------------------------------------------------------
149153
-- Actor modular requirements
@@ -198,45 +202,47 @@ type LabelCount = CountMap' MailboxLabel BoundedCount
198202

199203
-- | Add flow-sensitive counting of mailbox labels
200204
counting :: (MonadAbstractCount MailboxLabel BoundedCount m,
201-
MonadAbstractCount SequentialCmp AbstractCount m,
205+
-- MonadAbstractCount SequentialCmp AbstractCount m,
202206
MapM CountIn LabelCount m,
203207
MapM CountOut LabelCount m,
204-
MapM CmpCountIn SeqCmpCount m,
205-
MapM CmpCountOut SeqCmpCount m,
208+
-- MapM CmpCountIn SeqCmpCount m,
209+
-- MapM CmpCountOut SeqCmpCount m,
206210
MonadBottom m,
207211
MonadCache m,
212+
-- MonadIO m,
208213
Key m Cmp ~ SequentialCmp)
209214
=> SequentialCmp
210215
-> (Cmp -> AroundT Cmp ActorVlu m ActorVlu)
211216
-> Cmp -> AroundT Cmp ActorVlu m ActorVlu
212217
counting outerCmp inner cmp = do
213218
k <- upperM $ key cmp
214219
counts <- getCounts
215-
cmpCounts <- getCounts
220+
-- cmpCounts <- getCounts
216221

217222
_ <- MapM.get (CountIn k) -- TODO: this seems to be necessary for a correct result, it could be related to dependency tracking which means that some things are not triggered correctly,
218223
-- if so this is just a bandaid...
219224
outCount <- fromMaybe CountMap.emptyCountMap <$> MapM.get (CountOut outerCmp)
220225

221226
-- TODO: it should actually be an invariant that the outCount is actually
222227
-- always smaller or equal, otherwise we are overwriting data.
223-
-- Normally the semantics of the analysis ensure this, but this does not seem
228+
-- Normally the semantics of the analysis ensures this, but this does not seem
224229
-- to be the case here, perhaps due to branching? So for now always keep the biggest
225230
-- one which should be sound.
226231
if not (leq (CountingMap counts) outCount)
227232
then MapM.put (CountOut outerCmp) (CountingMap counts)
228233
else return ()
229234

230235
MapM.joinWith (CountIn k) (CountingMap counts)
231-
MapM.joinWith (CmpCountIn k) (CountingMap cmpCounts)
236+
-- MapM.joinWith (CmpCountIn k) (CountingMap cmpCounts)
232237

238+
-- liftIO (putStrLn $ "Analyzing inner " ++ show cmp)
233239
v <- inner cmp
234240

235241
countOut <- maybe mbottom return =<< MapM.get (CountOut k)
236-
cmpCountOut <- maybe mbottom return =<< MapM.get (CmpCountOut k)
242+
-- cmpCountOut <- maybe mbottom return =<< MapM.get (CmpCountOut k)
237243

238244
putCounts (getCountingMap countOut)
239-
putCounts (getCountingMap cmpCountOut)
245+
-- putCounts (getCountingMap cmpCountOut)
240246
return v
241247

242248

@@ -253,25 +259,25 @@ type IntraT m = SequentialT (UncachedSequentialT (IntraAnalysisT SequentialCmp m
253259
intra :: forall m . InterAnalysisM m => ActorRef -> SequentialCmp -> m ()
254260
intra _ cmp = do
255261
countIn <- fromJust <$> MapM.get (CountIn cmp)
256-
cmpCountIn <- fromJust <$> MapM.get (CmpCountIn cmp)
257-
MapM.put (CmpCountIn cmp) (CountMap.increment cmp cmpCountIn)
262+
-- cmpCountIn <- fromJust <$> MapM.get (CmpCountIn cmp)
263+
-- MapM.put (CmpCountIn cmp) (CountMap.increment cmp cmpCountIn)
258264
result <- runFixT @(IntraT m)
259265
(runAroundT
260266
(counting cmp)
261267
.
262268
(eval @_ @_ @_ @Partition @MB))
263269
cmp
264-
& runAlloc VarAdr -- TODO: use the actual context
265-
& runAlloc PtrAdr -- problem: current context is infinite
270+
& runAlloc (const . flip VarAdr InsensitiveCtx) -- TODO: use the actual context
271+
& runAlloc (const . flip PtrAdr InsensitiveCtx) -- problem: current context is infinite
266272
& runAbstractCountT @MailboxLabel countIn
267-
& runAbstractCountT @SequentialCmp cmpCountIn
273+
-- & runAbstractCountT @SequentialCmp cmpCountIn
268274
& runJoinT
269275
& runIntraAnalysis cmp
270276
case result of
271277
BL.Bottom -> return ()
272-
BL.Value (((), count'), cmpCount') -> do
278+
BL.Value ((), count') -> do
273279
MapM.put (CountOut cmp) count'
274-
MapM.put (CmpCountOut cmp) cmpCount'
280+
-- MapM.put (CmpCountOut cmp) cmpCount'
275281

276282

277283
-- | Inter-analysis
@@ -284,7 +290,7 @@ inter :: InterAnalysisM m
284290
-> m ()
285291
inter labelCounts exp environment ref mb = do
286292
MapM.put (CountIn initialCmp) (CountingMap labelCounts)
287-
MapM.put (CmpCountIn initialCmp) CountMap.emptyCountMap
293+
-- MapM.put (CmpCountIn initialCmp) CountMap.emptyCountMap
288294
iterateWL' initialCmp (intra ref)
289295
where initialCmp = ActorExp exp -- component to analyze
290296
<+> environment -- initial lexical environment
@@ -311,16 +317,16 @@ analyze labelCounts exp env ref = do
311317
& runWithMapping @SequentialCmp @SequentialRes
312318
& runWithMapping @CountIn @LabelCount
313319
& runWithMapping @CountOut @LabelCount
314-
& runWithMapping @CmpCountIn @SeqCmpCount
320+
-- & runWithMapping @CmpCountIn @SeqCmpCount
315321
& runWithMapping @CmpCountOut @SeqCmpCount
316322
& runWithComponentTracking @SequentialCmp
317-
& runWithDependencyTracking @SequentialCmp @SequentialCmp
318-
& runWithDependencyTracking @SequentialCmp @(SchemeAdr Exp K)
319-
& runWithDependencyTracking @SequentialCmp @ActorRef
320-
& runWithDependencyTracking @SequentialCmp @CountIn
321-
& runWithDependencyTracking @SequentialCmp @CountOut
322-
& runWithDependencyTracking @SequentialCmp @CmpCountIn
323-
& runWithDependencyTracking @SequentialCmp @CmpCountOut
323+
& runWithDependencyTracingTracking @SequentialCmp @SequentialCmp
324+
& runWithDependencyTracingTracking @SequentialCmp @(SchemeAdr Exp K)
325+
& runWithDependencyTracingTracking @SequentialCmp @ActorRef
326+
& runWithDependencyTracingTracking @SequentialCmp @CountIn
327+
& runWithDependencyTracingTracking @SequentialCmp @CountOut
328+
& runWithDependencyTracingTracking @SequentialCmp @CmpCountIn
329+
& runWithDependencyTracingTracking @SequentialCmp @CmpCountOut
324330
-- & runWithWorklistProfilingT @SequentialCmp
325331
& runWithWorkList @(LIFOWorklist SequentialCmp)
326332
& runDebugIntraAnalysis ref
@@ -329,6 +335,6 @@ analyze labelCounts exp env ref = do
329335

330336
MapM.put (ActorResOut ref) (extractVal res)
331337
MapM.put (CountMax ref) (maxCount res)
332-
where extractVal (_ ::*:: res ::*:: _ ::*:: _ ::*:: _ ::*:: _) = ActorRes res
333-
maxCount (_ ::*:: _ ::*:: _ ::*:: counter ::*:: _ ::*:: _) =
338+
where extractVal (_ ::*:: res ::*:: _ ::*:: _ ::*:: _) = ActorRes res
339+
maxCount (_ ::*:: _ ::*:: _ ::*:: counter ::*:: _) =
334340
foldr (Map.unionWith Count.max . getCountingMap) Map.empty $ Map.elems counter

‎analyses/simpleactor/src/Syntax/SimpleActor/CoreToSimpleActor.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ import Syntax.Ide (Ide(..))
1313
import Syntax.Span (Span, pattern Span, SpanOf(..), Position(..))
1414
import Control.Monad.State
1515
import Data.Foldable
16+
import qualified Debug.Trace as Debug
1617

1718
------------------------------------------------------------
1819
-- Translation Monad
@@ -291,12 +292,13 @@ translate annMod =
291292
translateModule :: Ann Module -> Exp
292293
translateModule annMod =
293294
let bds = translate annMod
294-
exports = moduleExports annMod
295+
exports = Debug.traceShowId $ moduleExports annMod
295296
exportPats = map (\(nam, arity) -> ValuePat (Symbol $ nam ++ "/" ++ show arity) dummySpan) exports
296297
exportNames = map (\(nam, arity) -> Var (Ide (nam ++ "/" ++ show arity) dummySpan)) exports
297298
in Letrec bds (Lam [Ide "$funname" (spanOf annMod)]
298299
(Match (Var (Ide "$funname" dummySpan))
299-
(zip exportPats exportNames)
300+
( zip exportPats exportNames
301+
++ [(IdePat (Ide "x" dummySpan), App (Var (Ide "monarch:fail_analysis_missing_export/1" dummySpan)) [Var (Ide "x" dummySpan)] dummySpan)] )
300302
dummySpan)
301303
dummySpan)
302304
dummySpan

‎maf2-analysis/src/Analysis/Actors/Mailbox/Class.hs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,5 +30,4 @@ class (Ord m, Eq m) => Mailbox m msg | m -> msg where
3030
hasMessage msg = isTrue @(BottomLifted (CP Bool)) . hasMessage' msg
3131

3232
-- | Applies the given function over the mailbox contens
33-
mapMessages :: (msg -> msg) -> m -> m
34-
33+
mapMessages :: (msg -> msg) -> m -> m

‎maf2-analysis/src/Analysis/Actors/Mailbox/Graph.hs‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ module Analysis.Actors.Mailbox.Graph(
33
GraphMailbox(..),
44
messages,
55
toDot,
6+
numberOfUniqueGraphs,
7+
numberOfMessages
68
) where
79

810
import Analysis.Actors.Mailbox hiding (hasMessage)
@@ -107,6 +109,17 @@ instance (Ord msg) => Mailbox (GraphMailbox msg) msg where
107109
messages :: Ord msg => GraphMailbox msg -> Set msg
108110
messages = foldMap graphMessages . getMessageGraphs
109111

112+
-- | Returns the number of unique message graphs
113+
numberOfUniqueGraphs :: GraphMailbox msg -> Int
114+
numberOfUniqueGraphs = Set.size . getMessageGraphs
115+
116+
-- | Returns the number of abstract messages in this graph.
117+
-- Note that the actual number of messages in the concrete mailbox might
118+
-- be different as a single message might correspond to multiple
119+
-- concrete messages if the mailbox has lost its multiplicity information.
120+
numberOfMessages :: Ord msg => GraphMailbox msg -> Int
121+
numberOfMessages = Set.size . messages
122+
110123
-----------------------------------------------------------
111124
-- DOT graph visualization
112125
-----------------------------------------------------------

‎maf2-analysis/src/Analysis/Actors/Mailbox/GraphToSet.hs‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,11 @@ import qualified Data.Set as Set
1010
import Lattice.Class
1111
import Lattice.Trace
1212

13+
-- | The maximum number of graphs in a `GraphAbstraction` until
14+
-- it is turned into a set for performance reasons (they are probably equivalent in precision anyways past this limit)
15+
maxUniqueGraphs :: Int
16+
maxUniqueGraphs = 100
17+
1318
data GraphToSet msg = SetAbstraction (Set msg)
1419
| GraphAbstraction (GraphMailbox msg)
1520
deriving (Ord, Eq, Show)
@@ -34,12 +39,15 @@ instance BottomLattice (GraphToSet msg) where
3439
bottom = GraphAbstraction bottom
3540

3641
instance (Ord msg) => Mailbox (GraphToSet msg) msg where
37-
enqueue msg = \case SetAbstraction s -> SetAbstraction $ enqueue msg s
42+
enqueue msg =
43+
44+
\case SetAbstraction s -> SetAbstraction $ enqueue msg s
45+
self@(GraphAbstraction s) | numberOfUniqueGraphs s > maxUniqueGraphs -> graphToSet self
3846
GraphAbstraction s -> GraphAbstraction $ enqueue msg s
3947
dequeue = \case SetAbstraction s -> Set.map (fmap SetAbstraction) $ dequeue s
4048
GraphAbstraction s -> Set.map (fmap GraphAbstraction) $ dequeue s
4149
peek = \case SetAbstraction s -> peek s
42-
GraphAbstraction s -> peek s
50+
GraphAbstraction s -> peek s
4351
empty = GraphAbstraction empty
4452
hasMessage' msg = \case SetAbstraction s -> hasMessage' msg s
4553
GraphAbstraction s -> hasMessage' msg s

0 commit comments

Comments
 (0)