feat(ase): concolic iteration widening

softwarelanguageslab · Dec 12, 2024 · 23f43b9 · 23f43b9
1 parent 3872292
commit 23f43b9
Show file tree

Hide file tree

Showing 6 changed files with 187 additions and 107 deletions.
diff --git a/analyses/simpleactor/programs/test/ase/simpleloop-anf-input.scm b/analyses/simpleactor/programs/test/ase/simpleloop-anf-input.scm
@@ -0,0 +1,10 @@
+(letrec ((loop
+         (lambda (y)
+           (letrec ((z (= y 0)))
+           (if z
+              #t
+            (letrec ((v (- y 1)))
+               (loop v)))))))
+
+ (letrec ((in (input)))
+    (loop in)))
diff --git a/analyses/simpleactor/src/Analysis/SimpleActor/Fixpoint.hs b/analyses/simpleactor/src/Analysis/SimpleActor/Fixpoint.hs
@@ -25,38 +25,24 @@ import Domain.Scheme.Class (PaiDom, VecDom, StrDom)
 import qualified Data.Map as Map
 import Data.Kind (Type, Constraint)
 import Domain.SimpleActor
-import Analysis.Symbolic.Monad (FormulaT)
+import Analysis.Symbolic.Monad
+    ( FormulaT )
 import Solver.Z3 (runZ3SolverWithSetup)
 import Solver
 import Symbolic.AST ( emptyPC, PC )
 import qualified Symbolic.SMT as SMT
-import Analysis.Store (CountingMap, Store)
-import Analysis.Monad.Store ()
+import Analysis.Store (CountingMap)
 import Data.Maybe
-import Syntax.Span
-import Analysis.Monad.Context (MCfaT)
-import Debug.Trace
 import Analysis.Context (emptyMcfaContext)
-import Control.Monad.IO.Class
-import Control.Monad (void)
-import Control.Monad.Trans
-import Control.Monad.Layer (MonadLayer)
-import Control.Monad.Reader (ReaderT (ReaderT))
-import Control.Monad.Join (MonadJoinable)
 import Control.Monad.State
-import Lattice (Joinable)
-import Domain (Address)
-import Analysis.Monad.Store (WidenedStoreT)
-import Analysis.Monad (evalWithWidenedStore)
-import Analysis.Symbolic.Monad (WidenedFormulaT, evalWithWidenedFormulaT, pathWideningPerComponent, pathWideningPerComponentEval)
 
 ------------------------------------------------------------
 -- Shortcuts
 ------------------------------------------------------------
 
 type K = [Span]
 type ActorRef = Pid Exp K
-type ActorVlu = ActorValue K
+type ActorVlu = ActorValue K (EnvAdr K)
 type ActorEnv = Map String (EnvAdr K)
 type ActorCmp = Key (IntraT Identity) Cmp
 type ActorRes = Val (IntraT Identity) ActorVlu
@@ -107,14 +93,14 @@ type MonadInter m =
       ( MapM ActorCmp ActorRes m,
         WorkListM m ActorCmp,
         ComponentTrackingM m ActorCmp,
-        DependsOn m ActorCmp '[ 
-            ActorCmp , 
-            EnvAdr K, 
-            Pid Exp K, 
-            PaiAdrE Exp K, 
-            VecAdrE Exp K, 
-            StrAdrE Exp K, 
-            In ActorCmp ActorSto, 
+        DependsOn m ActorCmp '[
+            ActorCmp ,
+            EnvAdr K,
+            Pid Exp K,
+            PaiAdrE Exp K,
+            VecAdrE Exp K,
+            StrAdrE Exp K,
+            In ActorCmp ActorSto,
             Out ActorCmp ActorSto ],
             -- In ActorCmp ActorPC,
             -- Out ActorCmp ActorPC ],
@@ -148,7 +134,7 @@ mainStore e = fromJust . Map.lookup (Out (initialCmp e))
 
 intra :: forall m . MonadInter m
  => ActorCmp -> m ()
-intra cmp = void 
+intra cmp = void
              (runFixT @(IntraT (IntraAnalysisT ActorCmp m)) eval' cmp
            & runAlloc @Ide @K @(EnvAdr K) EnvAdr
            & runAlloc @Exp @K @(PaiAdrE Exp K) PaiAdr