Merge pull request #313 from UQ-PAC/simplification-pass-sva

constraint generation

Author: sadrabt

src/main/scala/Main.scala

@@ -139,7 +139,9 @@ object Main {
       name = "no-irreducible-loops",
       doc = "Disable producing irreducible loops when --analyse is passed (does nothing without --analyse)"
     )
-    noIrreducibleLoops: Flag
+    noIrreducibleLoops: Flag,
+    @arg(name = "dsa", doc = "Perform Data Structure Analysis if no version is specified perform constraint generation (requires --simplify flag) (none|norm|field|set|all)")
+    dsaType: Option[String],
   )
 
   def main(args: Array[String]): Unit = {
@@ -205,6 +207,19 @@ object Main {
       None
     }
 
+    val dsa: Option[DSAConfig] =  if (conf.simplify.value) {
+      conf.dsaType match
+        case Some("set") => Some(DSAConfig(immutable.Set(DSAAnalysis.Set)))
+        case Some("field") => Some(DSAConfig(immutable.Set(DSAAnalysis.Field)))
+        case Some("norm") => Some(DSAConfig(immutable.Set(DSAAnalysis.Norm)))
+        case Some("all") =>  Some(DSAConfig(immutable.Set(DSAAnalysis.Set, DSAAnalysis.Field, DSAAnalysis.Norm)))
+        case Some("none") => Some(DSAConfig(immutable.Set.empty))
+        case None => None
+        case Some(_) => throw new IllegalArgumentException("Illegal option to dsa, allowed are: (none|set|field|norm|all)")
+    } else {
+      None
+    }
+
     val boogieMemoryAccessMode = if (conf.lambdaStores.value) {
       BoogieMemoryAccessMode.LambdaStoreSelect
     } else {
@@ -240,7 +255,8 @@ object Main {
       validateSimp = conf.validateSimplify.value,
       staticAnalysis = staticAnalysis,
       boogieTranslation = boogieGeneratorConfig,
-      outputPrefix = conf.outFileName
+      outputPrefix = conf.outFileName,
+      dsaConfig = dsa
     )
 
     RunUtils.run(q)

src/main/scala/analysis/data_structure_analysis/Constraints.scala

@@ -0,0 +1,122 @@
+package analysis.data_structure_analysis
+
+import ir.{CFGPosition, Call, DirectCall, Expr, IndirectCall, IntraProcIRCursor, LocalVar, MemoryLoad, MemoryStore, Procedure, Statement, Variable, computeDomain}
+import util.ConstGenLogger
+
+sealed trait Constraint {
+  def source: CFGPosition
+  val label: String
+  def eval(evaluator: Expr => Any = identity): String
+}
+
+def content(value: Any): String = s"[|${value.toString}|]}"
+
+case class ConstraintArg(value: Expr, contents: Boolean = false) {
+  override def toString: String = eval()
+  def ignoreContents: ConstraintArg = ConstraintArg(value)
+  def eval(evaluator: Expr => Any = identity): String = {
+    val evaluated = evaluator(value)
+    if contents then content(evaluated) else evaluated.toString
+  }
+}
+
+sealed trait BinaryConstraint extends Constraint {
+  val arg1: ConstraintArg
+  val arg2: ConstraintArg
+
+  private def name = this.getClass.getSimpleName
+  override def toString: String = eval()
+  override def eval(evaluator: Expr => Any = identity): String = s"(${arg1.eval(evaluator)} <==> ${arg2.eval(evaluator)}"
+}
+
+case class AssignmentConstraint(pos: CFGPosition, ar1: Expr, ar2: Expr) extends BinaryConstraint {
+  override def source: CFGPosition = pos
+  override val label: String = labelToPC(Some(pos.toString))
+  override val arg1: ConstraintArg = ConstraintArg(ar1)
+  override val arg2: ConstraintArg =  ConstraintArg(ar2)
+}
+
+sealed trait MemoryAccessConstraint[T <: MemoryStore | MemoryLoad](pos: T, index: Expr, value: Expr, val size: Int)
+  extends BinaryConstraint {
+  val label: String = labelToPC(pos.label)
+  override def source: T = pos
+
+  override val arg1: ConstraintArg = ConstraintArg(index, true)
+  override val arg2: ConstraintArg = ConstraintArg(value)
+
+  override def toString: String = eval()
+
+  override def eval(evaluator: Expr => Any = identity): String =
+    s"${this.getClass.getSimpleName}($label, size: $size): " + super.eval(evaluator)
+}
+
+case class MemoryReadConstraint(pos: MemoryLoad)
+  extends MemoryAccessConstraint[MemoryLoad](pos, pos.index, pos.lhs, pos.size/8)
+
+case class MemoryWriteConstraint(pos: MemoryStore)
+  extends MemoryAccessConstraint[MemoryStore](pos, pos.index, pos.value, pos.size/8)
+
+sealed trait CallConstraint[T <: Call, V <: Procedure | Variable](call: T)
+  extends Constraint {
+  val label: String = labelToPC(call.label)
+  def caller: Procedure = call.parent.parent
+  def target: V
+  val inParams: Map[LocalVar, Expr]
+  val outParmas: Map[LocalVar, LocalVar]
+  def inConstraints: Set[AssignmentConstraint] = inParams.map(pair => AssignmentConstraint(call, pair._1, pair._2)).toSet
+  def outConstraints: Set[AssignmentConstraint] = outParmas.map(pair => AssignmentConstraint(call, pair._1, pair._2)).toSet
+  override def source: T = call
+  override def toString: String = eval()
+
+  override def eval(evaluator: Expr => Any = identity): String = {
+    s"${this.getClass.getSimpleName}($label, Proc ${caller.name} calls $target" ++ s"\nIn Param Constraints: ${inConstraints.map(_.eval(evaluator))}"
+      ++ s"\nOut Param Constraints: ${outConstraints.map(_.eval(evaluator))}"
+  }
+}
+
+case class DirectCallConstraint(call: DirectCall)
+  extends CallConstraint[DirectCall, Procedure] (call) {
+  override def target: Procedure = call.target
+
+  override val inParams: Map[LocalVar, Expr] = call.actualParams
+  override val outParmas: Map[LocalVar, LocalVar] = call.outParams.view.mapValues(_.asInstanceOf[LocalVar]).toMap
+}
+
+case class IndirectCallConstraint(call: IndirectCall)
+  extends CallConstraint[IndirectCall, Variable](call)
+{
+
+  override def target: Variable = call.target
+
+  override val inParams: Map[LocalVar, Expr] = Map.empty
+  override val outParmas: Map[LocalVar, LocalVar] = Map.empty
+}
+
+def generateConstraints(proc: Procedure): Set[Constraint]  = {
+  ConstGenLogger.info(s"Generating Constraints for ${proc.name}")
+  val domain = computeDomain(IntraProcIRCursor, Set(proc))
+  var constraints: Set[Constraint] = Set.empty
+
+  domain.foreach {
+    case load: MemoryLoad =>
+      constraints += MemoryReadConstraint(load)
+    case write: MemoryStore =>
+      constraints += MemoryWriteConstraint(write)
+    case call: DirectCall =>
+      constraints += DirectCallConstraint(call)
+    case indirectCall: IndirectCall => constraints += IndirectCallConstraint(indirectCall)
+    case _ =>
+  }
+
+  constraints
+}
+
+case class SVAConstraints(sva: SymbolicValues, constraints: Set[Constraint]) {
+  def this(proc: Procedure) = {
+    this(getSymbolicValues(proc), generateConstraints(proc))
+  }
+  def exprToSymVal(expr: Expr): SymValueSet = sva.exprToSymValSet(expr)
+}
+object SVAConstraints {
+  def apply(proc: Procedure) = new SVAConstraints(proc)
+}