Add Kiama as a dependency

build.sbt

@@ -9,6 +9,9 @@ libraryDependencies ++= Seq(
   "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2",
   "com.lihaoyi" %% "pprint" % "0.5.6",
 
+  // Language Processing
+  "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.4.0",
+
   // SMT Solving
   "io.github.tudo-aqua" % "z3-turnkey" % "4.8.7.1",
 

src/main/scala/pipedsl/Interpreter.scala

@@ -102,7 +102,7 @@ class Interpreter(val maxIterations: Int) {
                 interp_command(fbr, env)
             }
         }
-        case CAssign(lhs, rhs) => {
+        case CAssign(lhs, rhs, typ) => {
             val rval = interp_expr(rhs, env)
             lhs match {
                 case EVar(id) => {
@@ -114,7 +114,7 @@ class Interpreter(val maxIterations: Int) {
                 case _ => throw Errors.UnexpectedExpr(lhs)
             }
         }
-        case CRecv(lhs, rhs) => {
+        case CRecv(lhs, rhs, typ) => {
             val rval = interp_expr(rhs, env)
             lhs match {
                 case EVar(id) => {

src/main/scala/pipedsl/Main.scala

@@ -3,8 +3,10 @@ package pipedsl
 import java.io.{File, PrintWriter}
 import java.nio.file.{Files, Paths, StandardCopyOption}
 
+import com.microsoft.z3.Context
 import com.typesafe.scalalogging.Logger
 import org.apache.commons.io.FilenameUtils
+import pipedsl.analysis.{PredicateAnalysis, TimingAnalysis, TypeAnalysis, TypeInference}
 import pipedsl.codegen.bsv.{BSVPrettyPrinter, BluespecInterfaces}
 import pipedsl.codegen.bsv.BluespecGeneration.BluespecProgramGenerator
 import pipedsl.common.DAGSyntax.PStage
@@ -66,18 +68,19 @@ object Main {
     val pinfo = new ProgInfo(prog)
     try {
       val canonProg = CanonicalizePass.run(prog)
-      val basetypes = BaseTypeChecker.check(canonProg, None)
-      val nprog = new BindModuleTypes(basetypes).run(canonProg)
-      TimingTypeChecker.check(nprog, Some(basetypes))
-      MarkNonRecursiveModulePass.run(nprog)
-      val recvProg = SimplifyRecvPass.run(nprog)
-      LockRegionChecker.check(recvProg, None)
+      TypeInference.checkProgram(canonProg)
+      TypeAnalysis.get(canonProg).checkProg()
+      TimingAnalysis.get(canonProg).checkProg()
+      MarkNonRecursiveModulePass.run(canonProg)
+      val recvProg = SimplifyRecvPass.run(canonProg)
+      new LockRegionChecker(recvProg).check(recvProg, None)
       val lockWellformedChecker = new LockWellformedChecker()
       val locks = lockWellformedChecker.check(canonProg)
       pinfo.addLockInfo(lockWellformedChecker.getModLockTypeMap)
-      val lockChecker = new LockConstraintChecker(locks, lockWellformedChecker.getModLockTypeMap)
+      val ctx = new Context()
+      val lockChecker = new LockConstraintChecker(PredicateAnalysis.get(recvProg, ctx), locks, lockWellformedChecker.getModLockTypeMap, ctx)
       lockChecker.check(recvProg, None)
-      SpeculationChecker.check(recvProg, Some(basetypes))
+      //SpeculationChecker.check(recvProg, Some(basetypes))
       if (printOutput) {
         val writer = new PrintWriter(outputFile)
         writer.write("Passed")
@@ -103,7 +106,7 @@ object Main {
     //Run the transformation passes on the stage representation
     stageInfo map { case (n, stgs) =>
       //Change Recv statements into send + recv pairs
-      new ConvertAsyncPass(n).run(stgs)
+      new ConvertAsyncPass(n, TypeAnalysis.get(prog)).run(stgs)
       //Convert lock ops into ops that track explicit handles
       LockOpTranslationPass.run(stgs)
       //Add in extra conditionals to ensure address locks are not double acquired

src/main/scala/pipedsl/Parser.scala

@@ -143,14 +143,13 @@ class Parser extends RegexParsers with PackratParsers {
   lazy val lhs: Parser[Expr] = memAccess | variable
 
   lazy val simpleCmd: P[Command] = positioned {
-    typ.? ~ variable ~ "=" ~ expr ^^ { case t ~ n ~ _ ~ r => n.typ = t; CAssign(n, r) } |
-      typ.? ~ lhs ~ "<-" ~ expr ^^ { case t ~ l ~ _ ~ r => l.typ = t
-        CRecv(l, r)
+    typ.? ~ variable ~ "=" ~ expr ^^ { case t ~ n ~ _ ~ r => CAssign(n, r, t) } |
+      typ.? ~ lhs ~ "<-" ~ expr ^^ { case t ~ l ~ _ ~ r => CRecv(l, r, t)
       } |
       check |
       "start" ~> parens(iden) ^^ { i => CLockStart(i) } |
       "end" ~> parens(iden) ^^ { i => CLockEnd(i) } |
-      "acquire" ~> parens(lockArg) ^^ { i => CSeq(CLockOp(i, Reserved), CLockOp(i, Acquired)) } |
+      "acquire" ~> parens(lockArg) ^^ { i => CSeq(CLockOp(i, Reserved), CLockOp(copyLockArg(i), Acquired)) } |
       "reserve" ~> parens(lockArg) ^^ { i => CLockOp(i, Reserved)} |
       "block" ~> parens(lockArg) ^^ { i => CLockOp(i, Acquired) } |
       "release" ~> parens(lockArg) ^^ { i => CLockOp(i, Released)} |
@@ -160,6 +159,15 @@ class Parser extends RegexParsers with PackratParsers {
       expr ^^ (e => CExpr(e)) 
   }
 
+  private def copyLockArg(l: LockArg): LockArg = {
+    val evar = l.evar match {
+      case Some(e) => Some(e.copy(id = e.id.copy()))
+      case None => None
+    }
+    LockArg(l.id.copy(), evar)
+  }
+
+
   lazy val lockArg: P[LockArg] = positioned { 
     iden ~ brackets(variable).? ^^ {case i ~ v => LockArg(i, v)}
   }
@@ -171,7 +179,6 @@ class Parser extends RegexParsers with PackratParsers {
   lazy val speculate: P[Command] = positioned {
     "speculate" ~> parens(typ ~ variable ~ "=" ~ expr ~ "," ~ block ~ "," ~ block) ^^ {
       case t ~ v ~ _ ~ ev ~ _ ~ cv ~ _ ~ cs =>
-        v.typ = Some(t)
         CSpeculate(v, ev, cv, cs)
     }
   }
@@ -186,31 +193,31 @@ class Parser extends RegexParsers with PackratParsers {
     "default:" ~> block
   }
   lazy val split: P[Command] = positioned {
-    "split" ~> braces(rep(casestmt) ~ defaultcase.?) ^^ { case cl ~ dc => CSplit(cl, if (dc.isDefined) dc.get else CEmpty) }
+    "split" ~> braces(rep(casestmt) ~ defaultcase.?) ^^ { case cl ~ dc => CSplit(cl, if (dc.isDefined) dc.get else CEmpty()) }
   }
 
   lazy val block: P[Command] = {
-    braces(cmd.?) ^^ (c => c.getOrElse(CEmpty))
+    braces(cmd.?) ^^ (c => c.getOrElse(CEmpty()))
   }
 
   lazy val conditional: P[Command] = positioned {
     "if" ~> parens(expr) ~ block ~ ("else" ~> blockCmd).? ^^ {
-      case cond ~ cons ~ alt => CIf(cond, cons, if (alt.isDefined) alt.get else CEmpty)
+      case cond ~ cons ~ alt => CIf(cond, cons, if (alt.isDefined) alt.get else CEmpty())
     }
   }
 
-  lazy val seqCmd: P[Command] = {
+  lazy val seqCmd: P[Command] = { 
     simpleCmd ~ ";" ~ seqCmd ^^ { case c1 ~ _ ~ c2 => CSeq(c1, c2) } |
       blockCmd ~ seqCmd ^^ { case c1 ~ c2 => CSeq(c1, c2) } |
-      simpleCmd <~ ";" | blockCmd | "" ^^ { _ => CEmpty }
+      simpleCmd <~ ";" | blockCmd | "" ^^ { _ => CEmpty() }
   }
 
   lazy val cmd: P[Command] = positioned {
     seqCmd ~ "---" ~ cmd ^^ { case c1 ~ _ ~ c2 => CTBar(c1, c2) } |
       seqCmd
   }
 
-  lazy val sizedInt: P[Type] = "int" ~> angular(posint) ^^ { bits => TSizedInt(bits, unsigned = true) }
+  lazy val sizedInt: P[Type] = "int" ~> angular(posint) ^^ { bits => TSizedInt(TBitWidthLen(bits), unsigned = true) }
   lazy val latency: P[Latency.Latency] = "c" ^^ { _ => Latency.Combinational } |
     "s" ^^ { _ => Latency.Sequential } |
     "a" ^^ { _ => Latency.Asynchronous }
@@ -234,7 +241,6 @@ class Parser extends RegexParsers with PackratParsers {
   lazy val typeName: P[Type] = iden ^^ { i => TNamedType(i) }
 
   lazy val param: P[Param] = iden ~ ":" ~ (typ | typeName) ^^ { case i ~ _ ~ t =>
-    i.typ = Some(t)
     Param(i, t)
   }
 

src/main/scala/pipedsl/analysis/AnalysisProvider.scala

@@ -0,0 +1,9 @@
+package pipedsl.analysis
+
+import pipedsl.common.Syntax.Prog
+
+trait AnalysisProvider[Analysis] {
+
+  def get(program: Prog): Analysis
+
+}

src/main/scala/pipedsl/analysis/PredicateAnalysis.scala

@@ -0,0 +1,109 @@
+package pipedsl.analysis
+
+import com.microsoft.z3.{AST => Z3AST, BoolExpr => Z3BoolExpr, Context => Z3Context, Expr => Z3Expr}
+import org.bitbucket.inkytonik.kiama.attribution.Attribution
+import org.bitbucket.inkytonik.kiama.relation.Tree
+import pipedsl.common.Syntax
+import pipedsl.common.Syntax.{BoolOp, BoolUOp, CIf, CSeq, CSplit, CaseObj, Command, EVar, EqOp, Expr, ModuleDef, Prog, ProgramNode}
+import pipedsl.common.Utilities.{mkAnd, mkOr}
+
+class PredicateAnalysis(program: Tree[ProgramNode, Prog], typeAnalysis: TypeAnalysis, ctx: Z3Context) extends Attribution{
+
+  private val intArray = ctx.mkArraySort(ctx.getIntSort, ctx.getIntSort)
+  private var incrementer = 0
+
+  val increment: Unit => Int = {
+    _ =>
+      incrementer += 1
+      incrementer
+  }
+
+  private def addPredicate(cond: Expr): Z3Expr = abstractInterp(cond) match {
+    case Some(value) => value
+    case None => ctx.mkEq(ctx.mkBoolConst("__TOPCONSTANT__" + increment()), ctx.mkTrue())
+  }
+
+  // Gives the condition for a branch
+  val branchCond: ProgramNode => Z3BoolExpr = attr {
+    case program.prev.pair(p: Command, program.parent.pair(prev: Expr, c@CIf(cond, cons, alt))) => 
+      addPredicate(cond).asInstanceOf[Z3BoolExpr]
+    case program.prev.pair(p: Command, program.parent.pair(prev: Command, c@CIf(cond, cons, alt)))  => 
+      ctx.mkNot(branchCond(prev))
+    case program.prev.pair(c@CaseObj(_, _), prev@CaseObj(_, _)) => mkAnd(ctx, ctx.mkNot(runningConds(prev)), caseCond(c))
+    case program.prev.pair(default: Command, prev@CaseObj(_, _)) => ctx.mkNot(runningConds(prev))
+    case program.parent.pair(c@CaseObj(_, _), p@CSplit(_, _)) => caseCond(c)
+  }
+
+  val caseCond: CaseObj => Z3BoolExpr = attr {
+    case c@CaseObj(cond, body) => addPredicate(cond).asInstanceOf[Z3BoolExpr]
+  }
+
+  val runningConds: CaseObj => Z3BoolExpr = attr {
+    case program.prev.pair(c@CaseObj(_,_), cprev@CaseObj(_, _)) => mkOr(ctx, runningConds(cprev), caseCond(c))
+    case c: CaseObj => caseCond(c)
+  }
+
+  //TODO: Add error in case of unexpected case, this is only called in lock constraint checker though
+  val predicate: ProgramNode => Z3BoolExpr = {
+    attr {
+      case program.parent.pair(c: Command, cif@CIf(_, _, _)) => mkAnd(ctx, predicate(cif), branchCond(c))
+      case program.parent.pair(p, c: CSplit) => mkAnd(ctx, predicate(c), branchCond(p))
+      case program.parent(_:ModuleDef) => ctx.mkTrue()
+      case program.parent(p) => predicate(p)
+    }
+  }
+
+  val abstractInterp: Expr => Option[Z3Expr] = 
+    attr {
+      case evar: EVar => Some(declareConstant(evar))
+      case Syntax.EInt(v, base, bits) => Some(ctx.mkInt(v))
+      case Syntax.EBool(v) => if (v) Some(ctx.mkTrue()) else Some(ctx.mkFalse())
+      case Syntax.EUop(op, ex) =>
+        val absex = abstractInterp(ex)
+        (op, absex) match {
+          case (BoolUOp(o), Some(v)) if o == "!" => Some(ctx.mkNot(v.asInstanceOf[Z3BoolExpr]))
+          case _ => None
+        }
+      case Syntax.EBinop(op, e1, e2) =>
+        val abse1 = abstractInterp(e1)
+        val abse2 = abstractInterp(e2)
+        (op, abse1, abse2) match {
+          case (EqOp(o), Some(v1), Some(v2)) if o == "==" => Some(ctx.mkEq(v1, v2))
+          case (EqOp(o), Some(v1), Some(v2)) if o == "!=" => Some(ctx.mkNot(ctx.mkEq(v1, v2)))
+          case (BoolOp(o, _), Some(v1), Some(v2)) if o == "&&" =>
+            Some(ctx.mkAnd(v1.asInstanceOf[Z3BoolExpr], v2.asInstanceOf[Z3BoolExpr]))
+          case (BoolOp(o, _), Some(v1), Some(v2)) if o == "||" =>
+            Some(ctx.mkOr(v1.asInstanceOf[Z3BoolExpr], v2.asInstanceOf[Z3BoolExpr]))
+          case _ => None
+        }
+      case Syntax.ETernary(cond, tval, fval) =>
+        val abscond = abstractInterp(cond)
+        val abstval = abstractInterp(tval)
+        val absfval = abstractInterp(fval)
+        (abscond, abstval, absfval) match {
+          case (Some(vcond), Some(vtval), Some(vfval)) =>
+            Some(ctx.mkITE(vcond.asInstanceOf[Z3BoolExpr], vtval, vfval))
+          case _ =>
+            None
+        }
+      case _ => None
+  }
+
+  def declareConstant(evar: EVar): Z3Expr =
+    typeAnalysis.typeCheck(evar) match {
+        case _: Syntax.TSizedInt => ctx.mkIntConst(evar.id.v);
+        case _: Syntax.TBool => ctx.mkBoolConst(evar.id.v)
+        case _: Syntax.TMemType => ctx.mkConst(evar.id.v, intArray)
+        case _ => throw new RuntimeException("Unexpected type")
+    }
+}
+object PredicateAnalysis extends Attribution {
+  val instance: Z3Context => Prog => PredicateAnalysis =
+    paramAttr {
+      ctx => {
+        case p => new PredicateAnalysis(new Tree[ProgramNode, Prog](p), TypeAnalysis.get(p), ctx)
+      }
+    }
+  def get(program: Prog, ctx: Z3Context): PredicateAnalysis = instance(ctx)(program)
+}
+