prepare for benchmarking again

softwarelanguageslab · Dec 27, 2024 · 1248715 · 1248715
1 parent 4bd71d9
commit 1248715
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 42 deletions.
diff --git a/analyses/simpleactor/app/ASE/Benchmark.hs b/analyses/simpleactor/app/ASE/Benchmark.hs
@@ -59,40 +59,40 @@ benchmarkCmd (BenchmarkOptions { .. }) = do
 
 benchmarkPrograms :: [String]
 benchmarkPrograms = [
-      --"benchmarks-out/games_snake.rkt",
-      --"benchmarks-out/games_tetris.rkt",
-      --"benchmarks-out/games_zombie.rkt",
-      --"benchmarks-out/mochi_fold-div.rkt",
-      --"benchmarks-out/mochi_hors.rkt",
-      --"benchmarks-out/mochi_hrec.rkt",
-      --"benchmarks-out/mochi_l-zipunzip.rkt",
-      --"benchmarks-out/mochi_map-foldr.rkt",
-      --"benchmarks-out/mochi_mappend.rkt",
-      --"benchmarks-out/mochi_mem.rkt",
-      --"benchmarks-out/mochi_mult.rkt",
-      --"benchmarks-out/mochi_neg.rkt",
-      --"benchmarks-out/mochi_nth0.rkt",
-      --"benchmarks-out/mochi_r-file.rkt",
-      --"benchmarks-out/mochi_r-lock.rkt",
-      --"benchmarks-out/mochi_reverse.rkt",
-      --"benchmarks-out/mochi_sum.rkt",
-      --"benchmarks-out/mochi_zip.rkt",
-      --"benchmarks-out/sergey_blur.rkt",
-      --"benchmarks-out/sergey_eta.rkt",
-      --"benchmarks-out/sergey_kcfa2.rkt",
-      --"benchmarks-out/sergey_kcfa3.rkt",
-      --"benchmarks-out/sergey_loop2.rkt",
-      --"benchmarks-out/sergey_mj09.rkt",
-      --"benchmarks-out/sergey_sat.rkt",
-      --"benchmarks-out/softy_append.rkt",
-      --"benchmarks-out/softy_cpstak.rkt",
-      --"benchmarks-out/softy_last-pair.rkt",
-      --"benchmarks-out/softy_last.rkt",
-      --"benchmarks-out/softy_length-acc.rkt",
-      --"benchmarks-out/softy_length.rkt",
-      --"benchmarks-out/softy_member.rkt",
-      --"benchmarks-out/softy_recursive-div2.rkt",
-      --"benchmarks-out/softy_subst.rkt",
+      "benchmarks-out/games_snake.rkt",
+      "benchmarks-out/games_tetris.rkt",
+      "benchmarks-out/games_zombie.rkt",
+      "benchmarks-out/mochi_fold-div.rkt",
+      "benchmarks-out/mochi_hors.rkt",
+      "benchmarks-out/mochi_hrec.rkt",
+      "benchmarks-out/mochi_l-zipunzip.rkt",
+      "benchmarks-out/mochi_map-foldr.rkt",
+      "benchmarks-out/mochi_mappend.rkt",
+      "benchmarks-out/mochi_mem.rkt",
+      "benchmarks-out/mochi_mult.rkt",
+      "benchmarks-out/mochi_neg.rkt",
+      "benchmarks-out/mochi_nth0.rkt",
+      "benchmarks-out/mochi_r-file.rkt",
+      "benchmarks-out/mochi_r-lock.rkt",
+      "benchmarks-out/mochi_reverse.rkt",
+      "benchmarks-out/mochi_sum.rkt",
+      "benchmarks-out/mochi_zip.rkt",
+      "benchmarks-out/sergey_blur.rkt",
+      "benchmarks-out/sergey_eta.rkt",
+      "benchmarks-out/sergey_kcfa2.rkt",
+      "benchmarks-out/sergey_kcfa3.rkt",
+      "benchmarks-out/sergey_loop2.rkt",
+      "benchmarks-out/sergey_mj09.rkt",
+      "benchmarks-out/sergey_sat.rkt",
+      "benchmarks-out/softy_append.rkt",
+      "benchmarks-out/softy_cpstak.rkt",
+      "benchmarks-out/softy_last-pair.rkt",
+      "benchmarks-out/softy_last.rkt",
+      "benchmarks-out/softy_length-acc.rkt",
+      "benchmarks-out/softy_length.rkt",
+      "benchmarks-out/softy_member.rkt",
+      "benchmarks-out/softy_recursive-div2.rkt",
+      "benchmarks-out/softy_subst.rkt",
       "benchmarks-out/softy_tak.rkt"
    ]
 
@@ -146,9 +146,9 @@ instance Common.IsAnalysisResult AnalysisResult where
 
 analysisConfigurations :: [(String, Exp -> IO AnalysisResult)]
 analysisConfigurations = concatMap (\k -> [
-      ("smallstep;" ++ show k, fmap AnalysisResult . SmallStep.analyze k),
+      --("smallstep;" ++ show k, fmap AnalysisResult . SmallStep.analyze k),
       ("widened per state;" ++ show k, fmap AnalysisResult . SmallStepWidened.analyze k),
-      ("global widening;"++show k, fmap AnalysisResult . SmallStepWidened.analyzeGlobal k)
+      --("global widening;"++show k, fmap AnalysisResult . SmallStepWidened.analyzeGlobal k)
    ]) [1..5]
 
 

diff --git a/analyses/simpleactor/src/Analysis/ASE/WidenedStates.hs b/analyses/simpleactor/src/Analysis/ASE/WidenedStates.hs
@@ -31,7 +31,7 @@ import Control.Monad.Join (cond, condsCP, fromBL)
 
 import Syntax (SpanOf(..))
 import Analysis.Store (Store(..))
-import RIO ( runIdentity, Identity, liftIO )
+import RIO ( runIdentity, Identity, liftIO, hFlush, stdout )
 import Solver ( CachedSolver, runCachedSolver )
 import Domain.Core.AbstractCount (AbstractCount(CountInf, CountOne))
 import Solver.Z3 (Z3Solver, runZ3SolverWithSetup)
@@ -43,7 +43,7 @@ import Lattice.BottomLiftedLattice (lowerBottom, BottomLifted)
 import GHC.Generics (Generic)
 import Control.DeepSeq
 import Data.Kind (Type)
-import Data.Foldable (foldrM)
+import Data.Foldable (foldrM, foldlM)
 import qualified Debug.Trace as Debug
 import qualified Analysis.Environment as Environment
 import qualified Lattice.BottomLiftedLattice as BL
@@ -288,6 +288,7 @@ step' (State { control = Err _ }) _ = return (Set.empty, emptyDelta)
 step :: (Ord (f State), Applicative f,  SmallstepM State m) => Shared f -> State -> m (SharedStepDelta, Set State)
 step shared inn = do
    (successors, delta) <- step' inn (fromJust $ Map.lookup (pure inn) shared)
+   -- liftIO (putStr ".") >> hFlush stdout
    registerSuccessor (SuccessorMap $ Map.singleton inn successors)
    return (delta, successors)
 
@@ -314,9 +315,11 @@ isStuckState succs st =
 
 collect' :: (Applicative f, Ord (f State), SmallstepM State m) => Shared f -> Set State -> Set State ->  m (Shared f, Set State)
 collect' shared nxt ss = do
-      (shared', nxt') <- foldrM merge (shared, Set.empty) nxt
+      (shared', nxt') <- foldlM (flip merge) (shared, Set.empty) nxt
       let ss' = Set.union ss nxt'
-      liftIO (putStrLn $ "number of discovered states " ++ show (Set.size ss'))
+      --liftIO (putStrLn "")
+      --liftIO (putStrLn $ "number of discovered states " ++ show (Set.size ss'))
+      --liftIO (putStrLn $ "number of next states " ++ show (Set.size nxt))
       -- mapM_ (\state -> liftIO $ putStrLn $ "discovered state " ++ show state) (Set.difference ss' ss)
       if (Set.size ss' > 1000 && False) || (shared', ss') == (shared, ss) then
          return (shared', ss')
@@ -325,7 +328,7 @@ collect' shared nxt ss = do
    where merge inn (shared', ss') = do
             (delta, successors) <- step shared inn
             let originalSharedStep = fromMaybe Lat.bottom (Map.lookup (pure inn) shared')
-            return (Map.unionWith Lat.join (Map.fromList $ map ((,applyDeltaJoin originalSharedStep delta) . pure) (Set.toList successors)) shared', ss' `Set.union` successors)
+            successors `deepseq` return (Map.unionWith Lat.join (Map.fromList $ map ((,applyDeltaJoin originalSharedStep delta) . pure) (Set.toList successors)) shared', ss' `Set.union` successors)
 
 -- | Compute the set of successors for the given list of states
 collect :: (Applicative f, Ord (f State), SmallstepM State m) => Shared f -> Set State -> m (Shared f, Set State)
@@ -336,7 +339,7 @@ collect shared ss = do
    where merge inn (shared', ss') = do
             (delta, successors) <- step shared inn
             let originalSharedStep = fromMaybe Lat.bottom (Map.lookup (pure inn) shared')
-            return (Map.union (Map.fromList $ map ((,applyDeltaJoin originalSharedStep delta) . pure) (Set.toList successors)) shared', ss' `Set.union` successors)
+            successors `deepseq` (return (Map.union (Map.fromList $ map ((,applyDeltaJoin originalSharedStep delta) . pure) (Set.toList successors)) shared', ss' `Set.union` successors))
 
 -- | Incremental computation of the least fixed point by only considering the 
 -- successors states produced in the previous iteration for the next iteration