feat: added level methode to compute and which height we are in the lattice

bramvdbogaerde · bramvdbogaerde · commit 0c1d573529a3 · 2026-02-25T14:46:22.000+01:00
diff --git a/build.sbt b/build.sbt
@@ -14,7 +14,7 @@ lazy val maf = crossProject(JVMPlatform, JSPlatform)
     name := "maf",
     organization := "soft",
     version := "2.0",
-    scalaVersion := "3.1.0",
+    scalaVersion := "3.3.7",
     //crossScalaVersions ++= Seq("2.13.6", "3.1.0"),
     /** Dependencies */
     libraryDependencies += "org.scala-lang.modules" %%% "scala-parser-combinators" % "2.0.0",
diff --git a/code/jvm/src/main/scala/maf/cli/experiments/incremental/IncrementalExperiment.scala b/code/jvm/src/main/scala/maf/cli/experiments/incremental/IncrementalExperiment.scala
@@ -18,8 +18,10 @@ trait IncrementalExperiment[E <: Expression]:
     // Analysis construction.
     def analysis(e: E, config: IncrementalConfiguration): Analysis
 
+    protected var dynamicConfigurations: List[IncrementalConfiguration] = List()
+    
     // The analysis configurations to use.
-    var configurations: List[IncrementalConfiguration] = List()
+    def configurations: List[IncrementalConfiguration] = dynamicConfigurations
 
     // Parsing.
     def parse(string: String): E
@@ -42,7 +44,8 @@ trait IncrementalExperiment[E <: Expression]:
     def createOutput(): String
 
     // Can be used for debugging.
-    var catchErrors: Boolean = true
+    protected var catchErrorsDynamic = true
+    def catchErrors: Boolean = catchErrorsDynamic
 
     // Runs measurements on the benchmarks in a given trait, or uses specific benchmarks if passed as an argument.
     def measure(bench: Set[String]): Unit =
@@ -76,8 +79,8 @@ trait IncrementalExperiment[E <: Expression]:
     /** Runs the benchmarks. Returns the path to the output file. */
     def execute(bench: Set[String], args: IncArgs): String =
         if executed then throw new Exception("Evaluation using this instance already executed. Create new instance of evaluation class.")
-        if args.stopOnError then catchErrors = false
-        if args.config.nonEmpty then configurations = List(args.config.get) else configurations = allConfigurations // Allows to override the default list of configurations of a setup.
+        if args.stopOnError then catchErrorsDynamic = false
+        if args.config.nonEmpty then dynamicConfigurations = List(args.config.get) else dynamicConfigurations = allConfigurations // Allows to override the default list of configurations of a setup.
         if args.timeout >= 0 then minutes = args.timeout
         executed = true
         val (writer, file): (Writer, String) = openTimeStampedGetName(outputDir + s"$minutes MIN " + outputFile)
diff --git a/code/jvm/src/main/scala/maf/cli/experiments/precision/PrecisionBenchmarks.scala b/code/jvm/src/main/scala/maf/cli/experiments/precision/PrecisionBenchmarks.scala
@@ -11,11 +11,8 @@ import maf.modular.scheme._
 import maf.util._
 import maf.util.benchmarks.Timeout
 import maf.language.scheme.interpreter.EmptyIO
+import maf.core.address.*
 
-sealed trait BaseAddr extends Address { def printable = true; def idn: Identity }
-case class VarAddr(vrb: Identifier) extends BaseAddr { def idn: Identity = vrb.idn; override def toString = s"<variable $vrb>" }
-case class PtrAddr(exp: Expression) extends BaseAddr { def idn = exp.idn; override def toString = s"<pointer $exp>" }
-case class PrmAddr(nam: String) extends BaseAddr { def idn: Identity = Identity.none; override def toString = s"<primitive $nam>" }
 
 abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolLattice, Chr: CharLattice, Str: StringLattice, Smb: SymbolLattice]:
 
@@ -29,9 +26,9 @@ abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolL
     implicit def cpAnalysis(anl: ModularSchemeDomain): Analysis = anl.asInstanceOf[Analysis]
 
     private def convertAddr(addr: Address): BaseAddr = addr match
-        case maf.modular.scheme.VarAddr(vrb, _) => VarAddr(vrb)
-        case maf.modular.scheme.PtrAddr(exp, _) => PtrAddr(exp)
-        case maf.modular.scheme.PrmAddr(nam)    => PrmAddr(nam)
+        case maf.modular.scheme.VarAddr(vrb, _) => maf.core.address.VarAddr(vrb)
+        case maf.modular.scheme.PtrAddr(exp, _) => maf.core.address.PtrAddr(exp)
+        case maf.modular.scheme.PrmAddr(nam)    => maf.core.address.PrmAddr(nam)
         case a: maf.modular.scheme.aam.AAMScheme#SchemeAddress => a.toBaseAddr
 
     val baseDomain = new ModularSchemeLattice[BaseAddr, Str, Bln, Num, Rea, Chr, Smb]
@@ -61,9 +58,9 @@ abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolL
         case analysis.modularLatticeWrapper.modularLattice.Elements(vs) => baseDomain.Elements(vs.map(convertV(analysis)))
 
     private def convertConcreteAddr(addr: ConcreteValues.Addr): BaseAddr = addr._2 match
-        case ConcreteValues.AddrInfo.VarAddr(v) => VarAddr(v)
-        case ConcreteValues.AddrInfo.PtrAddr(p) => PtrAddr(p)
-        case ConcreteValues.AddrInfo.PrmAddr(p) => PrmAddr(p)
+        case ConcreteValues.AddrInfo.VarAddr(v) => maf.core.address.VarAddr(v)
+        case ConcreteValues.AddrInfo.PtrAddr(p) => maf.core.address.PtrAddr(p)
+        case ConcreteValues.AddrInfo.PrmAddr(p) => maf.core.address.PrmAddr(p)
 
     protected def convertConcreteValue(value: ConcreteValues.Value): BaseValue = value match
         case ConcreteValues.Value.Nil          => baseLattice.nil
diff --git a/code/jvm/src/main/scala/maf/cli/experiments/scv/CountFalsePositives.scala b/code/jvm/src/main/scala/maf/cli/experiments/scv/CountFalsePositives.scala
@@ -82,7 +82,7 @@ object CountFalsePositives:
                     case Error =>
                         (List(), table.add(name, s"${analysis}_blames", "ERROR"))
 
-                val remainingMetrics = metrics.map(_.name).toSet -- addedMetrics.toSet
+                val remainingMetrics = metrics.map(_.toString).toSet -- addedMetrics.toSet
 
                 remainingMetrics.foldLeft(resTable)((table, metric) => table.add(name, s"${analysis}_${metric}", "-"))
 
diff --git a/code/shared/src/main/scala/maf/aam/scheme/SchemeAAMSemantics.scala b/code/shared/src/main/scala/maf/aam/scheme/SchemeAAMSemantics.scala
@@ -106,6 +106,7 @@ trait BaseSchemeAAMSemantics(prog: SchemeExp) extends maf.aam.AAMAnalysis[Scheme
             case V(v1) => s"V($v1)"
             case K(k1) => s"K($k1)"
         def refs(x: Storable): Set[Address] = throw new Exception("NYI -- storableLattice.refs(x)")
+        def level(x: Storable): Int = ???
 
     /**
      * An address under which a continuation is stored. To preserve call-return semantics, this address should be (e, p) where e is the call targets
diff --git a/code/shared/src/main/scala/maf/core/BaseAddr.scala b/code/shared/src/main/scala/maf/core/BaseAddr.scala
@@ -0,0 +1,9 @@
+package maf.core
+
+package address {
+
+  sealed trait BaseAddr extends Address { def printable = true; def idn: Identity }
+  case class VarAddr(vrb: Identifier) extends BaseAddr { def idn: Identity = vrb.idn; override def toString = s"<variable $vrb>" }
+  case class PtrAddr(exp: Expression) extends BaseAddr { def idn = exp.idn; override def toString = s"<pointer $exp>" }
+  case class PrmAddr(nam: String) extends BaseAddr { def idn: Identity = Identity.none; override def toString = s"<primitive $nam>" }
+}
diff --git a/code/shared/src/main/scala/maf/core/Lattice.scala b/code/shared/src/main/scala/maf/core/Lattice.scala
@@ -37,6 +37,14 @@ trait Lattice[L] extends PartialOrdering[L] with Show[L] with Serializable:
     /** For PartialOrdering[L]: a lattice has a partial order, defined by subsumes... */
     final def lteq(x: L, y: L): Boolean = subsumes(y, x)
 
+    /** Computes the number of levels upto the current value */
+    def level(v: L): Int
+    /** Computes the number of levels to the top value if one exists,
+        otherwise Int.MAX_INT is returned */
+    def levelToTop(v: L): Int =
+        try level(top) - level(v)
+        catch { case _ => Int.MaxValue }
+
     /** ...and elements of the lattice can be compared */
     final def tryCompare(x: L, y: L): Option[Int] = (subsumes(x, y), subsumes(y, x)) match
         case (true, true)   => Some(0) // x >= y and y >= x => x = y
@@ -55,6 +63,7 @@ object Lattice:
         def subsumes(x: Set[A], y: => Set[A]): Boolean = y.subsetOf(x)
         def eql[B: BoolLattice](x: Set[A], y: Set[A]) = ???
         def ceq(x: Set[A], y: => Set[A]): Boolean = x == y
+        def level(v: Set[A]): Int = v.size // the number of levels is the amount of elements in the size
 
     implicit def setLattice[A: Show]: Lattice[Set[A]] = new SetLattice[A]
 
@@ -65,6 +74,7 @@ object Lattice:
         def join(x: Unit, y: => Unit): Unit = ()
         def subsumes(x: Unit, y: => Unit): Boolean = true
         def eql[B: BoolLattice](x: Unit, y: Unit): B = BoolLattice[B].inject(true)
+        def level(v: Unit): Int = 1
 
     def foldMapL[X, L: Lattice](xs: Iterable[X], f: X => L): L =
         if xs.isEmpty then Lattice[L].bottom
diff --git a/code/shared/src/main/scala/maf/language/scheme/lattices/ModularSchemeLattice.scala b/code/shared/src/main/scala/maf/language/scheme/lattices/ModularSchemeLattice.scala
@@ -91,6 +91,7 @@ class ModularSchemeLattice[A <: Address, S: StringLattice, B: BoolLattice, I: In
 
         // TODO: this in ad-hoc lattice, we should make a PairLattice instead somewhere
         val lattice: Lattice[Abstract] = new Lattice[Abstract] {
+            def level(v: (L, L)): scala.Int = Lattice[L].level(v._1) * Lattice[L].level(v._2)
             def show(v: (L, L)): String = s"(${v._1},${v._2})"
             def top = throw LatticeTopUndefined
             def bottom = ???
@@ -108,6 +109,14 @@ class ModularSchemeLattice[A <: Address, S: StringLattice, B: BoolLattice, I: In
         override def extract(v: Vec) = v
         // TODO: ad-hoc implementation, should create a VectorLattice
         val lattice: Lattice[Vec] = new Lattice[Vec] {
+            def level(v: Vec): scala.Int =
+                Lattice[I]
+                    .level(v.size) *
+                    v.elements.keys.map(Lattice[I].level).foldLeft(1)(_ * _) *
+                    v.elements.values
+                        .map(Lattice[L].level)
+                        .foldLeft(1)(_ * _)
+
             def show(v: Vec) = v.toString
             def top = throw LatticeTopUndefined
             def bottom = Vec(IntLattice[I].bottom, Map())
@@ -271,8 +280,7 @@ class ModularSchemeLattice[A <: Address, S: StringLattice, B: BoolLattice, I: In
         def typeName = "PNTR"
         val tpy = PointerT
         override def toString: String =
-            if ptrs.size > 3
-            then s"{${ptrs.size} pointers}"
+            if ptrs.size > 3 then s"{${ptrs.size} pointers}"
             else ptrs.mkString("Pointers{", ", ", "}")
 
     case class Cons(car: L, cdr: L) extends Value:
@@ -927,6 +935,7 @@ class ModularSchemeLattice[A <: Address, S: StringLattice, B: BoolLattice, I: In
 
     // TODO: field SchemeLattice only exists for backwards compatibility reasons, but for the sake of simplification should also be removed, and the methods be included within the class itself
     val schemeLattice: SchemeLattice[L, A] = new SchemeLattice[L, A] { lat =>
+        def level(x: L): scala.Int = x.keys.map(key => x.getAbstract(key).map(key.lattice.level(_)).foldLeft(1)(_ * _)).foldLeft(1)(_ * _)
         def show(x: L): String = x.toString /* TODO[easy]: implement better */
         def isTrue(x: L): Boolean = x.elements[Value].foldMap(Value.isTrue(_))(boolOrMonoid)
         def isFalse(x: L): Boolean = x.elements[Value].foldMap(Value.isFalse(_))(boolOrMonoid)
diff --git a/code/shared/src/main/scala/maf/language/scheme/lattices/Product2SchemeLattice.scala b/code/shared/src/main/scala/maf/language/scheme/lattices/Product2SchemeLattice.scala
@@ -40,6 +40,7 @@ class Product2ModularSchemeLattice[
             PL(f(left), right)
 
     def product2Lattice: Product2SchemeLattice[PL, O, A] = new Product2SchemeLattice:
+        def level(v: PL): scala.Int = Lattice[L].level(v.left) * Lattice[O].level(v.right)
         def show(x: PL): String = x.toString
         def refs(x: PL): Set[Address] = schemeLattice.refs(x.left)
         def isTrue(x: PL): Boolean = schemeLattice.isTrue(x.left)
diff --git a/code/shared/src/main/scala/maf/language/symbolic/lattices/SymbolicLattice.scala b/code/shared/src/main/scala/maf/language/symbolic/lattices/SymbolicLattice.scala
@@ -70,6 +70,7 @@ object SymbolicLattice:
  * used in an actual analysis. Such a widening operation is implemented in the `widen` function
  */
 class SymbolicLattice[B: BoolLattice] extends Lattice[Set[Symbolic]]:
+    def level(v: Set[Symbolic]) = v.size
     type L = Set[Symbolic]
     def bottom: L = Set()
     override def isBottom(x: L): Boolean = x.isEmpty
diff --git a/code/shared/src/main/scala/maf/lattice/ConcreteLattice.scala b/code/shared/src/main/scala/maf/lattice/ConcreteLattice.scala
@@ -65,6 +65,7 @@ class ConcreteLattice:
                 content.foldLeft(Lattice[Y].bottom)((acc, v) => Lattice[Y].join(acc, f(v)))
 
         implicit val stringConcrete: StringLattice[S] = new BaseInstance[String]("Str") with StringLattice[S] {
+            def level(s: S): Int = ???
             def inject(x: String): S = makeValues(Set(x))
             def length[I2: IntLattice](s: S): I2 = s.foldMap(s => IntLattice[I2].inject(s.length))
             def append(s1: S, s2: S): S = (s1, s2) match
@@ -141,6 +142,7 @@ class ConcreteLattice:
                     }
         }
         implicit val boolConcrete: BoolLattice[B] = new BaseInstance[Boolean]("Bool") with BoolLattice[B] {
+            def level(v: B): Int = ???
             def inject(x: Boolean): B = makeValues(Set(x))
             def isTrue(b: B): Boolean = b match
                 case Top             => true
@@ -154,6 +156,7 @@ class ConcreteLattice:
         }
 
         implicit val intConcrete: IntLattice[I] = new BaseInstance[BigInt]("Int") with IntLattice[I] {
+            def level(i: I) = ???
             def inject(x: BigInt): I = makeValues(Set(x))
 
             def toReal[R2: RealLattice](n: I): R2 = n match
@@ -207,6 +210,7 @@ class ConcreteLattice:
         }
 
         implicit val realConcrete: RealLattice[R] = new BaseInstance[Double]("Real") with RealLattice[R] {
+            def level(v: R): Int = ???
             def inject(x: Double): R = makeValues(Set(x))
             def toInt[I2: IntLattice](n: R): I2 = n.foldMap(n => IntLattice[I2].inject(n.toInt))
             def ceiling(n: R): R = n.map(_.ceil)
@@ -235,6 +239,7 @@ class ConcreteLattice:
                 n.foldMap(n => StringLattice[S2].inject(n.toString))
         }
         implicit val charConcrete: CharLattice[C] = new BaseInstance[Char]("Char") with CharLattice[C] {
+            def level(v: C): Int = ???
             def inject(x: Char): C = makeValues(Set(x))
             def downCase(c: C): C = c.map(_.toLower)
             def upCase(c: C): C = c.map(_.toUpper)
@@ -258,6 +263,7 @@ class ConcreteLattice:
             }
         }
         implicit val symConcrete: SymbolLattice[Sym] = new BaseInstance[String]("Sym")(Show.symShow) with SymbolLattice[Sym] {
+            def level(s: Sym): Int = ???
             def inject(x: String): Sym = makeValues(Set(x))
             def toString[S2: StringLattice](s: Sym): S2 = s.foldMap(s => StringLattice[S2].inject(s))
         }
diff --git a/code/shared/src/main/scala/maf/lattice/ConstantPropagationLattice.scala b/code/shared/src/main/scala/maf/lattice/ConstantPropagationLattice.scala
@@ -16,6 +16,10 @@ object ConstantPropagation:
     case object Bottom extends L[Nothing]
 
     abstract class BaseInstance[A: Show](typeName: String) extends Lattice[L[A]]:
+        def level(v: L[A]): scala.Int = v match
+            case Top         => 3
+            case Constant(v) => 2
+            case Bottom      => 1
         def show(x: L[A]): String = x match
             case Top         => typeName
             case Constant(x) => x.toString
diff --git a/code/shared/src/main/scala/maf/lattice/HMapLattice.scala b/code/shared/src/main/scala/maf/lattice/HMapLattice.scala
@@ -80,6 +80,9 @@ case class HMap(contents: Map[HMapKey, Any]):
           )
         )
 
+    /** Returns all the keys in the HMap */
+    def keys: Iterable[HMapKey] = this.contents.keys
+
     /** Checks subsumptions of `this` with y */
     def subsumes(y: HMap): Boolean =
         val x = this
@@ -140,3 +143,4 @@ object HMap:
         def join(x: HMap, y: => HMap): HMap = x.join(y)
         def subsumes(x: HMap, y: => HMap): Boolean = x.subsumes(y)
         def eql[B: BoolLattice](x: HMap, y: HMap): B = ???
+        def level(x: HMap): scala.Int = x.keys.map(key => x.getAbstract(key).map(key.lattice.level(_)).foldLeft(1)(_ * _)).foldLeft(1)(_ * _)
diff --git a/code/shared/src/main/scala/maf/lattice/TaintLattice.scala b/code/shared/src/main/scala/maf/lattice/TaintLattice.scala
@@ -16,6 +16,9 @@ object TaintLattice:
     case object MayBeTainted extends TL
 
     class TaintLattice extends Lattice[TL]:
+        def level(v: TL): Int = v match
+            case Untainted    => 1
+            case MayBeTainted => 2
         val bottom: TL = Untainted
         override def isBottom(x: TL): Boolean = x == Untainted
         val top: TL = MayBeTainted
diff --git a/code/shared/src/main/scala/maf/lattice/TypeLattice.scala b/code/shared/src/main/scala/maf/lattice/TypeLattice.scala
@@ -12,6 +12,9 @@ object Type:
     case object Bottom extends T
 
     abstract class BaseInstance(typeName: String) extends Lattice[T]:
+        def level(x: T): Int = x match
+            case Top    => 2
+            case Bottom => 1
         def show(x: T): String = x match
             case Top    => typeName
             case Bottom => s"$typeName.⊥"
diff --git a/code/shared/src/main/scala/maf/modular/incremental/scheme/lattice/IncrementalModularSchemeLattice.scala b/code/shared/src/main/scala/maf/modular/incremental/scheme/lattice/IncrementalModularSchemeLattice.scala
@@ -64,6 +64,7 @@ class IncrementalModularSchemeLattice[
 
     /** The actual lattice implementation for AL and A. */
     val incrementalSchemeLattice: IncrementalSchemeLattice[AL, A] = new IncrementalSchemeLattice[AL, A] {
+        def level(x: AL): scala.Int = Lattice[L].level(x.toL())
 
         //private var implicitFlows: Set[A] = Set()
         //def setContext(addr: Set[A]): Unit = implicitFlows = addr
@@ -199,5 +200,6 @@ class IncrementalModularSchemeLattice[
             table.prettyString(columns = List("diff", xname, yname))
     }
 
+
     object AL:
         implicit val lattice: IncrementalSchemeLattice[AL, A] = incrementalSchemeLattice
diff --git a/code/shared/src/main/scala/maf/modular/scheme/aam/AAMScheme.scala b/code/shared/src/main/scala/maf/modular/scheme/aam/AAMScheme.scala
@@ -1,6 +1,7 @@
 package maf.modular.scheme.aam
 
-import maf.core.* 
+import maf.core.*
+import maf.core.address.*
 import maf.language.scheme.*
 import maf.language.scheme.lattices.*
 import maf.language.scheme.primitives.*
@@ -52,20 +53,20 @@ abstract class AAMScheme(prg: SchemeExp) extends ModAnalysis[SchemeExp](prg):
     // addresses
 
     sealed trait SchemeAddress extends Address:
-        def toBaseAddr: maf.cli.experiments.precision.BaseAddr 
+        def toBaseAddr: maf.core.address.BaseAddr 
 
     case class NAdr(nat: String) extends SchemeAddress:
         def idn = Identity.none
         def printable = false
-        def toBaseAddr = maf.cli.experiments.precision.PrmAddr(nat)
+        def toBaseAddr = maf.core.address.PrmAddr(nat)
     case class VAdr(vrb: Var, ctx: Ctx) extends SchemeAddress:
         def idn = vrb.idn
         def printable = true 
-        def toBaseAddr = maf.cli.experiments.precision.VarAddr(vrb)
+        def toBaseAddr = maf.core.address.VarAddr(vrb)
     case class PAdr(exp: Exp, ctx: Ctx) extends SchemeAddress:
         def idn = exp.idn
         def printable = true
-        def toBaseAddr = maf.cli.experiments.precision.PtrAddr(exp)
+        def toBaseAddr = maf.core.address.PtrAddr(exp)
     trait KAdr extends Address:
         def printable = false
     case class KA(ev: Ev, sto: Sto) extends KAdr:
@@ -309,4 +310,4 @@ abstract class AAMScheme(prg: SchemeExp) extends ModAnalysis[SchemeExp](prg):
     def finalValues: Set[Val] = 
         visited.collect { case State(Ko(v), _, _, HaltAddr) => v }
     def finalValue: Val = 
-        lattice.join(finalValues)
+        lattice.join(finalValues)
diff --git a/project/build.properties b/project/build.properties
@@ -1 +1 @@
-sbt.version=1.10.11
+sbt.version=1.12.4
