more type inference. Works for basic usage, not for implicit casts (q…

…uite yet)
apl-cornell · Aug 4, 2021 · 80730aa · 80730aa
1 parent 9a5f533
commit 80730aa
Show file tree

Hide file tree

Showing 70 changed files with 1,525 additions and 640 deletions.
diff --git a/docs/inference.md b/docs/inference.md
@@ -0,0 +1,19 @@
+# Type inference
+
+This document describes what you can and can't expect from the type inference
+engine.
+
+# Implicit casting
+Implicit casting could be confusing to the programmer, so it is disabled by
+default. The "autocast" commandline option enables it, in which cast casts
+to higher bitwidths will be automatically inserted
+
+# Constants
+
+Integer constant types have two components: the bit width and the
+signedness. You can specify the signedness with a `u` in front of the constant,
+and the width is specified with angle brackets after. So if you want to write
+the number four as an unsigned, 16 bit number, it would be `u4<16>`
+
+You do not have to specify these types, as they can be inferred. However, if you
+have a multiplication of constants, one of them will need to be annotated
diff --git a/src/main/scala/pipedsl/Main.scala b/src/main/scala/pipedsl/Main.scala
@@ -26,8 +26,8 @@ object Main {
           case ("parse") => parse(debug = true, printOutput = true, config.file, config.out)
           case ("interpret") => interpret(config.maxIterations, config.memoryInput, config.file, config.out)
           case ("gen") => gen(config.out, config.file, config.printStageGraph,
-            config.debug, config.defaultAddrLock, config.memInit, config.port_warn)
-          case ("typecheck") => runPasses(printOutput = true, config.file, config.out, config.port_warn)
+            config.debug, config.defaultAddrLock, config.memInit, config.port_warn, config.autocast)
+          case ("typecheck") => runPasses(printOutput = true, config.file, config.out, config.port_warn, config.autocast)
           case _ =>
         }
       }
@@ -55,7 +55,7 @@ object Main {
     i.interp_prog(RemoveTimingPass.run(prog), MemoryInputParser.parse(memoryInputs), outputFile)
   }
 
-  def runPasses(printOutput: Boolean, inputFile: File, outDir: File, port_warn :Boolean): (Prog, ProgInfo) = {
+  def runPasses(printOutput: Boolean, inputFile: File, outDir: File, port_warn :Boolean, autocast :Boolean): (Prog, ProgInfo) = {
     if (!Files.exists(inputFile.toPath)) {
       throw new RuntimeException(s"File $inputFile does not exist")
     }
@@ -66,8 +66,8 @@ object Main {
     val pinfo = new ProgInfo(prog)
     try {
       val verifProg = AddVerifyValuesPass.run(prog)
-      val canonProg = new CanonicalizePass().run(verifProg)
-      /*val basetypes = */(new TypeInference).checkProgram(canonProg)
+      val canonProg1 = new CanonicalizePass().run(verifProg)
+      val canonProg = (new TypeInference(autocast)).checkProgram(canonProg1)
       val basetypes = BaseTypeChecker.check(canonProg, None)
       val nprog = new BindModuleTypes(basetypes).run(canonProg)
       TimingTypeChecker.check(nprog, Some(basetypes))
@@ -136,8 +136,8 @@ object Main {
   }
 
   def gen(outDir: File, inputFile: File, printStgInfo: Boolean = false, debug: Boolean = false,
-    addrLockMod: Option[String] = None, memInit: Map[String, String], port_warn :Boolean): Unit = {
-    val (prog_recv, prog_info) = runPasses(printOutput = false, inputFile, outDir, port_warn)
+    addrLockMod: Option[String] = None, memInit: Map[String, String], port_warn :Boolean, autocast :Boolean): Unit = {
+    val (prog_recv, prog_info) = runPasses(printOutput = false, inputFile, outDir, port_warn, autocast)
     val optstageInfo = getStageInfo(prog_recv, printStgInfo)
     //TODO better way to pass configurations to the BSInterfaces object
     //copies mem initialization to output directory

diff --git a/src/main/scala/pipedsl/common/CommandLineParser.scala b/src/main/scala/pipedsl/common/CommandLineParser.scala
@@ -17,6 +17,7 @@ object CommandLineParser {
     defaultAddrLock: Option[String] = None,
     memInit: Map[String, String] = Map(),
     port_warn: Boolean = false,
+    autocast :Boolean = false,
   )
 
   private def buildParser(): OParser[Unit, Config] = {
@@ -40,6 +41,9 @@ object CommandLineParser {
         opt[Unit]('p', "portwarn")
           .action((_, c) => c.copy(port_warn = true))
           .text("Throw errors for port conflicts between stages"),
+        opt[Unit]('a', "autocast")
+          .action((_, c) => c.copy(autocast = true))
+          .text("Insert casts to allow for subtyping of integers"),
         arg[File]("<file>...")
           .action((x, c) => c.copy(file = x))
           .text("pdl files to parse"),

diff --git a/src/main/scala/pipedsl/common/Syntax.scala b/src/main/scala/pipedsl/common/Syntax.scala
@@ -7,6 +7,7 @@ import pipedsl.common.Locks.{General, LockGranularity, LockState}
 import com.microsoft.z3.BoolExpr
 
 
+
 object Syntax {
   /**
    * Annotations added by the various passes of the type checker.
@@ -15,6 +16,7 @@ object Syntax {
     sealed trait TypeAnnotation {
       var typ: Option[Type] = None
     }
+
     sealed trait LabelAnnotation {
       var lbl: Option[Label] = None
     }
@@ -37,6 +39,11 @@ object Syntax {
     }
   }
 
+  sealed trait HasCopyMeta
+  {
+    val copyMeta : HasCopyMeta => HasCopyMeta = x => x
+  }
+
   object Latency extends Enumeration {
     type Latency = Value
     val Combinational: Latency = Value("c")
@@ -82,9 +89,15 @@ object Syntax {
 
   case class Id(v: String) extends Positional with TypeAnnotation {
     override def toString = s"$v"
+    def copyMeta(from :Id) :Id =
+      {
+        setPos(from.pos)
+        typ = from.typ
+        this
+      }
   }
 
-  sealed trait Type extends Positional with LabelAnnotation with SpeculativeAnnotation {
+  sealed trait Type extends Positional with LabelAnnotation with SpeculativeAnnotation with HasCopyMeta {
     override def toString: String = this match {
       case _: TVoid => "void"
       case _: TBool => "bool"
@@ -104,10 +117,21 @@ object Syntax {
       case TBitWidthLen(len) => len.toString
       case TBitWidthMax(b1, b2) => "max(" + b1 + ", " + b2 + ")"
       case TBitWidthVar(name) => "bitVar(" + name + ")"
-      case TSigned() => "signed"
-      case TUnsigned() => "unsigned"
-      case TSignVar(name) => "sign(" + name + ")"
+      case t :TSignedNess => t match
+      {
+        case TSigned() => "signed"
+        case TUnsigned() => "unsigned"
+        case TSignVar(name) => "sign(" + name + ")"
+      }
     }
+    override val copyMeta: HasCopyMeta => Type =
+      {
+        case from :Type =>
+          setPos(from.pos)
+          lbl = from.lbl
+          maybeSpec = from.maybeSpec
+          this
+      }
   }
   // Types that can be upcast to Ints
   sealed trait IntType
@@ -239,6 +263,7 @@ object Syntax {
     def copyMeta(from: Expr): Expr = {
       setPos(from.pos)
       typ = from.typ
+      portNum = from.portNum
       this
     }
   }
@@ -267,7 +292,17 @@ object Syntax {
   case class ECast(ctyp: Type, exp: Expr) extends Expr
 
 
-  sealed trait Command extends Positional with SMTPredicate with PortAnnotation
+  sealed trait Command extends Positional with SMTPredicate with PortAnnotation with HasCopyMeta
+  {
+    override val copyMeta: HasCopyMeta => Command =
+      {
+        case from :Command =>
+        setPos(from.pos)
+        portNum = from.portNum
+        predicateCtx = from.predicateCtx
+        this
+      }
+  }
   case class CSeq(c1: Command, c2: Command) extends Command
   case class CTBar(c1: Command, c2: Command) extends Command
   case class CIf(cond: Expr, cons: Command, alt: Command) extends Command
@@ -331,7 +366,17 @@ object Syntax {
     inputs: List[Param],
     modules: List[Param],
     ret: Option[Type],
-    body: Command) extends Definition with RecursiveAnnotation with SpeculativeAnnotation
+    body: Command) extends Definition with RecursiveAnnotation with SpeculativeAnnotation with HasCopyMeta
+    {
+      override val copyMeta: HasCopyMeta => ModuleDef =
+        {
+          case from :ModuleDef =>
+          maybeSpec = from.maybeSpec
+          isRecursive = from.isRecursive
+          pos = from.pos
+          this
+        }
+    }
 
   case class Param(name: Id, typ: Type) extends Positional
 

diff --git a/src/main/scala/pipedsl/common/Utilities.scala b/src/main/scala/pipedsl/common/Utilities.scala
@@ -316,7 +316,6 @@ object Utilities {
 
   private def typeMapExpr(e :Expr, f_opt : Option[Type] => Option[Type]) : Unit =
     {
-      println(s"setting ${e.typ} to ${f_opt(e.typ)}")
       e.typ = f_opt(e.typ)
       e match
       {
@@ -352,34 +351,38 @@ object Utilities {
         case _ => ()
       }
     }
-  private def typeMapCmd(c :Command, f_opt :Option[Type] => Option[Type]) :Unit = c match
-  {
-    case CSeq(c1, c2) => typeMapCmd(c1, f_opt); typeMapCmd(c2, f_opt)
-    case CTBar(c1, c2) => typeMapCmd(c1, f_opt); typeMapCmd(c2, f_opt)
-    case CIf(cond, cons, alt) => typeMapExpr(cond, f_opt); typeMapCmd(cons, f_opt); typeMapCmd(alt, f_opt)
-    case CAssign(lhs, rhs, _) => typeMapExpr(lhs, f_opt); typeMapExpr(rhs, f_opt)
-    case CRecv(lhs, rhs, _) => typeMapExpr(lhs, f_opt); typeMapExpr(rhs, f_opt)
-    case CSpecCall(handle, pipe, args) =>
-      typeMapExpr(handle, f_opt); typeMapId(pipe, f_opt); args.foreach(typeMapExpr(_, f_opt))
-    case CVerify(handle, args, preds) =>
-      typeMapExpr(handle, f_opt); args.foreach(typeMapExpr(_, f_opt)); preds.foreach(typeMapExpr(_, f_opt))
-    case CInvalidate(handle) => typeMapExpr(handle, f_opt)
-    case CPrint(args) => args.foreach(typeMapExpr(_, f_opt))
-    case COutput(exp) => typeMapExpr(exp, f_opt)
-    case CReturn(exp) => typeMapExpr(exp, f_opt)
-    case CExpr(exp) => typeMapExpr(exp, f_opt)
-    case CLockStart(mod) => typeMapId(mod, f_opt)
-    case CLockEnd(mod) => typeMapId(mod, f_opt)
-    case CLockOp(mem, _, _) =>
-      typeMapId(mem.id, f_opt);
-      mem.evar match
-      {case Some(value) => typeMapExpr(value, f_opt)
-      case None => ()}
-    case CSplit(cases, default) =>
-      cases.foreach(cs => {typeMapExpr(cs.cond, f_opt); typeMapCmd(cs.body, f_opt)})
-      typeMapCmd(default, f_opt)
-    case _ => ()
-  }
+  private def typeMapCmd(c :Command, f_opt :Option[Type] => Option[Type]) :Unit =
+    {
+      c match
+      {
+        case CSeq(c1, c2) => typeMapCmd(c1, f_opt); typeMapCmd(c2, f_opt)
+        case CTBar(c1, c2) => typeMapCmd(c1, f_opt); typeMapCmd(c2, f_opt)
+        case CIf(cond, cons, alt) => typeMapExpr(cond, f_opt); typeMapCmd(cons, f_opt); typeMapCmd(alt, f_opt)
+        case CAssign(lhs, rhs, _) => typeMapExpr(lhs, f_opt); typeMapExpr(rhs, f_opt)
+        case CRecv(lhs, rhs, _) => typeMapExpr(lhs, f_opt); typeMapExpr(rhs, f_opt)
+        case CSpecCall(handle, pipe, args) => typeMapExpr(handle, f_opt); typeMapId(pipe, f_opt); args.foreach(typeMapExpr(_, f_opt))
+        case CVerify(handle, args, preds) => typeMapExpr(handle, f_opt); args.foreach(typeMapExpr(_, f_opt)); preds.foreach(typeMapExpr(_, f_opt))
+        case CInvalidate(handle) => typeMapExpr(handle, f_opt)
+        case CPrint(args) => args.foreach(typeMapExpr(_, f_opt))
+        case COutput(exp) => typeMapExpr(exp, f_opt)
+        case CReturn(exp) => typeMapExpr(exp, f_opt)
+        case CExpr(exp) => typeMapExpr(exp, f_opt)
+        case CLockStart(mod) => typeMapId(mod, f_opt)
+        case CLockEnd(mod) => typeMapId(mod, f_opt)
+        case CLockOp(mem, _, _) => typeMapId(mem.id, f_opt);
+          mem.evar match
+          {
+            case Some(value) => typeMapExpr(value, f_opt)
+            case None => ()
+          }
+        case CSplit(cases, default) => cases.foreach(cs =>
+          {
+            typeMapExpr(cs.cond, f_opt); typeMapCmd(cs.body, f_opt)
+          })
+          typeMapCmd(default, f_opt)
+        case _ => ()
+      }
+    }
 
   private def typeMapId(i: Id, f_opt: Option[Type] => Option[Type]):Unit =
     {