diff --git a/docs/inference.md b/docs/inference.md new file mode 100644 index 00000000..dfa53536 --- /dev/null +++ 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 index ba145c29..1817bdb6 100644 --- 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 index a25876ef..a05f3bb3 100644 --- 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]("...") .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 index 288df447..2c0c0133 100644 --- 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 index 02655493..bf1fe8d5 100644 --- 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 = { diff --git a/src/main/scala/pipedsl/passes/CanonicalizePass.scala b/src/main/scala/pipedsl/passes/CanonicalizePass.scala index 8d571f8f..c9f5d252 100644 --- a/src/main/scala/pipedsl/passes/CanonicalizePass.scala +++ b/src/main/scala/pipedsl/passes/CanonicalizePass.scala @@ -13,322 +13,154 @@ import pipedsl.passes.Passes.{CommandPass, FunctionPass, ModulePass, ProgPass} * and remove problems with implicit casting in the generated code. */ class CanonicalizePass() extends CommandPass[Command] with ModulePass[ModuleDef] - with FunctionPass[FuncDef] with ProgPass[Prog] { + with FunctionPass[FuncDef] with ProgPass[Prog] + { - var usedNames: Set[String] = Set() - var counter = 0 + var usedNames: Set[String] = Set() + var counter = 0 - private def freshTmp(e: Expr): CAssign = { - var name = "_tmp_" + counter - while (usedNames.contains(name)) { - counter += 1 - name = "_tmp_" + counter - } - usedNames = usedNames + name - val evar = EVar(Id(name).setPos(e.pos)).setPos(e.pos) - evar.typ = e.typ - CAssign(evar, e, e.typ).setPos(e.pos) - } - - override def run(c: Command): Command = { - usedNames = getAllVarNames(c).map(i => i.v) - val nc = extractCastVars(c) - removeCEmpty(nc) - } + private def freshTmp(e: Expr): CAssign = + { + var name = "_tmp_" + counter + while (usedNames.contains(name)) + { + counter += 1 + name = "_tmp_" + counter + } + usedNames = usedNames + name + val evar = EVar(Id(name).setPos(e.pos)).setPos(e.pos) + evar.typ = e.typ + CAssign(evar, e, e.typ).setPos(e.pos) + } - override def run(m: ModuleDef): ModuleDef = m.copy(body = run(m.body)).setPos(m.pos) + override def run(c: Command): Command = + { + usedNames = getAllVarNames(c).map(i => i.v) + val nc = extractCastVars(c) + removeCEmpty(nc) + } - override def run(f: FuncDef): FuncDef = f.copy(body = run(f.body)).setPos(f.pos) + override def run(m: ModuleDef): ModuleDef = m.copy(body = run(m.body)).setPos(m.pos) - override def run(p: Prog): Prog = p.copy(moddefs = p.moddefs.map(m => run(m)), - fdefs = p.fdefs.map(f => run(f))).setPos(p.pos) + override def run(f: FuncDef): FuncDef = f.copy(body = run(f.body)).setPos(f.pos) + override def run(p: Prog): Prog = p.copy(moddefs = p.moddefs.map(m => run(m)), fdefs = p.fdefs.map(f => run(f))).setPos(p.pos) - /** - * Removes all of the unnecessary CSeq commands that connect empty statements. - * We can't do the same for CTBar since having a time barrier potentially has meaning, even if one - * of the sides is empty. - * @param c The command to clean up - * @return The same command with no cseqs to/from empty commands - */ - def removeCEmpty(c: Command): Command = c match { - case CSeq(CEmpty(), CEmpty()) => CEmpty() - case CSeq(c1, CEmpty()) => removeCEmpty(c1) - case CSeq(CEmpty(), c2) => removeCEmpty(c2) - case CSeq(c1, c2) => CSeq(removeCEmpty(c1), removeCEmpty(c2)).setPos(c.pos) - case CTBar(c1, c2) => CTBar(removeCEmpty(c1), removeCEmpty(c2)).setPos(c.pos) - case CIf(cond, cons, alt) => CIf(cond, removeCEmpty(cons), removeCEmpty(alt)).setPos(c.pos) - case _ => c - } - def extractCastVars(c: Command): Command = c match { - case CSeq(c1, c2) => CSeq(extractCastVars(c1), extractCastVars(c2)).setPos(c.pos) - case CTBar(c1, c2) => CTBar(extractCastVars(c1), extractCastVars(c2)).setPos(c.pos) - case CIf(cond, cons, alt) => - val (ncond, nassgns) = extractCastVars(cond) - val nif = CIf(ncond, extractCastVars(cons), extractCastVars(alt)).setPos(c.pos) - CSeq(nassgns, nif).setPos(c.pos) - case CSplit(cases, default) => - val ndef = extractCastVars(default) - var assngs: Command = CEmpty() - val ncases = cases.foldLeft(List[CaseObj]())((l, cobj) => { - val (ncond, nassgns) = extractCastVars(cobj.cond) - val nbody = extractCastVars(cobj.body) - assngs = CSeq(assngs, nassgns).setPos(c.pos) - l :+ CaseObj(ncond, nbody).setPos(cobj.pos) - }) - CSeq(assngs, CSplit(ncases, ndef).setPos(c.pos)).setPos(c.pos) - case CAssign(lhs, rhs, typ) => - val (nrhs, nassgns) = extractCastVars(rhs) - val nc = CAssign(lhs, nrhs, typ).setPos(c.pos) - CSeq(nassgns, nc).setPos(c.pos) - case CRecv(lhs, rhs, typ) => - val (nrhs, na1) = extractCastVars(rhs) - val (nlhs, na2) = extractCastVars(lhs) - val nassgns = CSeq(na1, na2).setPos(c.pos) - CSeq(nassgns, CRecv(nlhs, nrhs, typ).setPos(c.pos)).setPos(c.pos) - case CSpecCall(handle, pipe, args) => - val (nargs, nc) = extractCastVars(args) - CSeq(nc, CSpecCall(handle, pipe, nargs).setPos(c.pos)).setPos(c.pos) - case CCheckSpec(_) => c - case CVerify(handle, args, preds) => - val (nargs, nc) = extractCastVars(args) - val (npreds, nc2) = extractCastVars(preds) - CSeq(nc, CSeq(nc2, CVerify(handle, nargs, npreds) - .setPos(c.pos)).setPos(c.pos)).setPos(c.pos) - case CInvalidate(_) => c - case CPrint(_) => c - case COutput(exp) => - val (nexp, nasgn) = extractCastVars(exp) - CSeq(nasgn, COutput(nexp).setPos(c.pos)).setPos(c.pos) - case CReturn(exp) => - val (nexp, nasgn) = extractCastVars(exp) - CSeq(nasgn, CReturn(nexp).setPos(c.pos)).setPos(c.pos) - case CExpr(exp) => - val (nexp, nasgn) = extractCastVars(exp) - CSeq(nasgn, CExpr(nexp).setPos(c.pos)).setPos(c.pos) - case CLockStart(_) => c - case CLockEnd(_) => c - case CLockOp(_, _, _) => c - case CEmpty() => c - case _: InternalCommand => c - } + /** + * Removes all of the unnecessary CSeq commands that connect empty statements. + * We can't do the same for CTBar since having a time barrier potentially has meaning, even if one + * of the sides is empty. + * + * @param c The command to clean up + * @return The same command with no cseqs to/from empty commands */ + def removeCEmpty(c: Command): Command = c match + { + case CSeq(CEmpty(), CEmpty()) => CEmpty() + case CSeq(c1, CEmpty()) => removeCEmpty(c1) + case CSeq(CEmpty(), c2) => removeCEmpty(c2) + case CSeq(c1, c2) => CSeq(removeCEmpty(c1), removeCEmpty(c2)).setPos(c.pos) + case CTBar(c1, c2) => CTBar(removeCEmpty(c1), removeCEmpty(c2)).setPos(c.pos) + case CIf(cond, cons, alt) => CIf(cond, removeCEmpty(cons), removeCEmpty(alt)).setPos(c.pos) + case _ => c + } - def extractCastVars(es: Iterable[Expr]): (List[Expr], Command) = { - es.foldLeft[(List[Expr],Command)]((List[Expr](), CEmpty()))((t, e) => { - val l = t._1 - val c = t._2 - val (nl, nc) = extractCastVars(e) - (l :+ nl, CSeq(c, nc).setPos(e.pos)) - }) - } + def extractCastVars(c: Command): Command = c match + { + case CSeq(c1, c2) => CSeq(extractCastVars(c1), extractCastVars(c2)).setPos(c.pos) + case CTBar(c1, c2) => CTBar(extractCastVars(c1), extractCastVars(c2)).setPos(c.pos) + case CIf(cond, cons, alt) => val (ncond, nassgns) = extractCastVars(cond) + val nif = CIf(ncond, extractCastVars(cons), extractCastVars(alt)).setPos(c.pos) + CSeq(nassgns, nif).setPos(c.pos) + case CSplit(cases, default) => val ndef = extractCastVars(default) + var assngs: Command = CEmpty() + val ncases = cases.foldLeft(List[CaseObj]())((l, cobj) => + { + val (ncond, nassgns) = extractCastVars(cobj.cond) + val nbody = extractCastVars(cobj.body) + assngs = CSeq(assngs, nassgns).setPos(c.pos) + l :+ CaseObj(ncond, nbody).setPos(cobj.pos) + }) + CSeq(assngs, CSplit(ncases, ndef).setPos(c.pos)).setPos(c.pos) + case CAssign(lhs, rhs, typ) => val (nrhs, nassgns) = extractCastVars(rhs) + val nc = CAssign(lhs, nrhs, typ).setPos(c.pos) + CSeq(nassgns, nc).setPos(c.pos) + case CRecv(lhs, rhs, typ) => val (nrhs, na1) = extractCastVars(rhs) + val (nlhs, na2) = extractCastVars(lhs) + val nassgns = CSeq(na1, na2).setPos(c.pos) + CSeq(nassgns, CRecv(nlhs, nrhs, typ).setPos(c.pos)).setPos(c.pos) + case CSpecCall(handle, pipe, args) => val (nargs, nc) = extractCastVars(args) + CSeq(nc, CSpecCall(handle, pipe, nargs).setPos(c.pos)).setPos(c.pos) + case CCheckSpec(_) => c + case CVerify(handle, args, preds) => val (nargs, nc) = extractCastVars(args) + val (npreds, nc2) = extractCastVars(preds) + CSeq(nc, CSeq(nc2, CVerify(handle, nargs, npreds).setPos(c.pos)).setPos(c.pos)).setPos(c.pos) + case CInvalidate(_) => c + case CPrint(_) => c + case COutput(exp) => val (nexp, nasgn) = extractCastVars(exp) + CSeq(nasgn, COutput(nexp).setPos(c.pos)).setPos(c.pos) + case CReturn(exp) => val (nexp, nasgn) = extractCastVars(exp) + CSeq(nasgn, CReturn(nexp).setPos(c.pos)).setPos(c.pos) + case CExpr(exp) => val (nexp, nasgn) = extractCastVars(exp) + CSeq(nasgn, CExpr(nexp).setPos(c.pos)).setPos(c.pos) + case CLockStart(_) => c + case CLockEnd(_) => c + case CLockOp(_, _, _) => c + case CEmpty() => c + case _: InternalCommand => c + } - /** - * Extract any subexpressions which are casts - * and return assignments to them as new variables. - * Also return a new expression which references the new variables. - * @param e - * @return - */ - def extractCastVars(e: Expr): (Expr, Command) = e match { - case EIsValid(ex) => - val (ne, nc) = extractCastVars(ex) - (EIsValid(ne).setPos(e.pos), nc) - case EFromMaybe(ex) => - val (ne, nc) = extractCastVars(ex) - (EFromMaybe(ne).setPos(e.pos), nc) - case EToMaybe(ex) => - val (ne, nc) = extractCastVars(ex) - (EToMaybe(ne).setPos(e.pos), nc) - case EUop(op, ex) => - val (ne, nc) = extractCastVars(ex) - (EUop(op, ne).setPos(e.pos), nc) - case EBinop(op, e1, e2) => - val (ne1, nc1) = extractCastVars(e1) - val (ne2, nc2) = extractCastVars(e2) - (EBinop(op, ne1, ne2).setPos(e.pos), CSeq(nc1, nc2).setPos(nc1.pos)) - case EMemAccess(mem, index, Some(mask)) => - val (ne, nc) = extractCastVars(index) - val (nm, ncm) = extractCastVars(mask) - (EMemAccess(mem, ne, Some(nm)).setPos(e.pos), - CSeq(nc, ncm).setPos(e.pos)) - case EMemAccess(mem, index, None) => - val (ne, nc) = extractCastVars(index) - (EMemAccess(mem, ne, None).setPos(e.pos), nc) - case EBitExtract(num, start, end) => - val (ne, nc) = extractCastVars(num) - (EBitExtract(ne, start, end).setPos(e.pos), nc) - case ETernary(cond, tval, fval) => - val (ncond, nc) = extractCastVars(cond) - val (net, nct) = extractCastVars(tval) - val (nef, ncf) = extractCastVars(fval) - (ETernary(ncond, net, nef).setPos(e.pos), - CSeq(CSeq(nc, nct).setPos(e.pos), ncf).setPos(e.pos)) - case EApp(func, args) => - val (nargs, nc) = extractCastVars(args) - (EApp(func, nargs).setPos(e.pos), nc) - case ECall(mod, args) => - val (nargs, nc) = extractCastVars(args) - (ECall(mod, nargs).setPos(e.pos), nc) - case ECast(ctyp, e) => - val (ne, nc) = extractCastVars(e) - val ncast = ECast(ctyp, ne) - ncast.typ = Some(ctyp) - val nassgn = freshTmp(ncast) - (nassgn.lhs, CSeq(nc, nassgn).setPos(e.pos)) - case _ => (e, CEmpty()) - } - /*this code was intended to do a limited CSE on combinational reads*/ - /*it turns out this is hard because of the way conditional expressions work*/ - /*so it is turned off for now. This would be better implemented later*/ - /*when we have the pipeline stages separated*/ + def extractCastVars(es: Iterable[Expr]): (List[Expr], Command) = + { + es.foldLeft[(List[Expr], Command)]((List[Expr](), CEmpty()))((t, e) => + { + val l = t._1 + val c = t._2 + val (nl, nc) = extractCastVars(e) + (l :+ nl, CSeq(c, nc).setPos(e.pos)) + }) + } -// def csemem_mod(moduleDef: ModuleDef): ModuleDef = -// moduleDef.copy(body = -// {val (bodp, _) = csemem_cmd(moduleDef.body, Map()); bodp}) -// .setPos(moduleDef.pos) -// -// /** -// * -// * @param c -// * @param env is a mapping from memories and their indices to IDs -// * @return -// */ -// def csemem_cmd(c: Command, env: Map[(Id, Id), Id]) -//: (Command, Map[(Id, Id), Id]) = c match -// { -// case CSeq(c1, c2) => -// val (c1p, nenv) = csemem_cmd(c1, env) -// val (c2p, fenv) = csemem_cmd(c2, nenv) -// (CSeq(c1p, c2p), fenv) -// case CTBar(c1, c2) => -// val (c1p, nenv) = csemem_cmd(c1, env) -// val (c2p, fenv) = csemem_cmd(c2, nenv) -// (CTBar(c1p, c2p), fenv) -// case CIf(cond, cons, alt) => -// val (defs, condp, nenv) = csemem_expr(cond, env) -// val (consp, _) = csemem_cmd(cons, env) -// val (altp, _) = csemem_cmd(alt, env) -// (CSeq(defs, CIf(condp, consp, altp)), nenv) -// case Syntax.CAssign(lhs@EVar(id), EMemAccess(mem, EVar(idx), _)) => -// env.get((mem, idx)) match -// { -// case Some(mapped) => (CAssign(lhs, EVar(mapped)), env) -// case None => (c, env + ((mem, idx) -> id)) -// } -// case Syntax.CAssign(lhs, rhs) => -// val (defs, rhsp, nenv) = csemem_expr(rhs, env) -// (CSeq(defs, CAssign(lhs, rhsp)), nenv) -// case Syntax.CRecv(lhs@EVar(id), EMemAccess(mem, EVar(idx), _)) => -// mem.typ.get match -// { -// case TLockedMemType(TMemType(_, _, readLatency, _, _, _), _, _) => -// readLatency match -// { -// case pipedsl.common.Syntax.Latency.Combinational => -// env.get((mem, idx)) match -// { -// case Some(mapped) => (CRecv(lhs, EVar(mapped)), env) -// case None => (c, env + ((mem, idx) -> id)) -// } -// case _ => (c, env) -// } -// } -// case Syntax.CSpecCall(handle, pipe, args) => -// val (fenv, defs, argsp) = -// args.foldLeft((env, CEmpty():Command, List.empty[Expr]))( -// (acc, arg) => -// { -// val (cmd, argp, nenv) = csemem_expr(arg, acc._1) -// (nenv, CSeq(cmd, acc._2), argp::acc._3) -// }) -// (CSeq(defs, CSpecCall(handle, pipe, argsp.reverse)), fenv) -// case Syntax.CVerify(handle, args, preds) => -// val (fenv, defs, argsp) = -// args.foldLeft((env, CEmpty():Command, List.empty[Expr]))( -// (acc, arg) => -// { -// val (cmd, argp, nenv) = csemem_expr(arg, acc._1) -// (nenv, CSeq(cmd, acc._2), argp::acc._3) -// }) -// (CSeq(defs, CVerify(handle, argsp.reverse, preds)), fenv) -// case Syntax.COutput(exp) => -// val (defs, expp, nenv) = csemem_expr(exp, env) -// (CSeq(defs, COutput(expp)), nenv) -// case Syntax.CReturn(exp) => -// val (defs, expp, nenv) = csemem_expr(exp, env) -// (CSeq(defs, CReturn(expp)), nenv) -// case Syntax.CExpr(exp) => -// val (defs, expp, nenv) = csemem_expr(exp, env) -// (CSeq(defs, CExpr(expp)), nenv) -// case Syntax.CSplit(cases, default) => -// (CSplit(cases.map(cs => -// { -// val (bodp, _) = csemem_cmd(cs.body, env) -// CaseObj(cs.cond, bodp) -// }), {val (defp, _) = csemem_cmd(default, env); defp}), env) -// case command: Syntax.InternalCommand => (c, env) -// case _ => (c, env) -// } -// -// def csemem_expr(e: Syntax.Expr, env: Map[(Id, Id), Id]) -//: (Command, Syntax.Expr, Map[(Id, Id), Id]) = e match -// { -// case EIsValid(ex) => -// val (defs, nexp, nenv) = csemem_expr(ex, env) -// (defs, EIsValid(nexp), nenv) -// case EFromMaybe(ex) => -// val (defs, nexp, nenv) = csemem_expr(ex, env) -// (defs, EFromMaybe(nexp), nenv) -// case EToMaybe(ex) => -// val (defs, nexp, nenv) = csemem_expr(ex, env) -// (defs, EToMaybe(nexp), nenv) -// case EUop(op, ex) => -// val (defs, nexp, nenv) = csemem_expr(ex, env) -// (defs, EUop(op, nexp), nenv) -// case EBinop(op, e1, e2) => -// val (defs1, ne1, nenv) = csemem_expr(e1, env) -// val (defs2, ne2, fenv) = csemem_expr(e2, nenv) -// (CSeq(defs1, defs2), EBinop(op, ne1, ne2), fenv) -// case ERecAccess(rec, fieldName) => -// val (defs, nrec, nenv) = csemem_expr(rec, env) -// (defs, ERecAccess(nrec, fieldName), nenv) -// case EMemAccess(mem, EVar(idx), _) => env.get((mem, idx)) match -// { -// case Some(id) => (CEmpty(), EVar(id), env) -// case None => -// val defs = freshTmp(e) -// val frsh = defs match {case CAssign(lhs, _) => lhs} -// (defs, frsh, env + ((mem, idx) -> frsh.id)) -// } -// case EBitExtract(num, start, end) => -// val (defs, nump, nenv) = csemem_expr(num, env) -// (defs, EBitExtract(nump, start, end), nenv) -// case ETernary(cond, tval, fval) => -// val (defs, condp, nenv) = csemem_expr(cond, env) -// (defs, ETernary(condp, tval, fval), nenv) -// case EApp(func, args) => -// val (fenv, defs, argsp) = -// args.foldLeft((env, CEmpty():Command, List.empty[Expr]))( -// (acc, arg) => -// { -// val (cmd, argp, nenv) = csemem_expr(arg, acc._1) -// (nenv, CSeq(cmd, acc._2), argp::acc._3) -// }) -// (defs, EApp(func, argsp.reverse), fenv) -// case ECall(mod, args) => -// val (fenv, defs, argsp) = -// args.foldLeft((env, CEmpty():Command, List.empty[Expr]))( -// (acc, arg) => -// { -// val (cmd, argp, nenv) = csemem_expr(arg, acc._1) -// (nenv, CSeq(cmd, acc._2), argp::acc._3) -// }) -// (defs, ECall(mod, argsp.reverse), fenv) -// case ECast(ctyp, exp) => -// val (defs, nexp, nenv) = csemem_expr(exp, env) -// (defs, ECast(ctyp, nexp), nenv) -// case expr: CirExpr =>(CEmpty(), e, env) -// case _ => (CEmpty(), e, env) -// } + /** + * Extract any subexpressions which are casts + * and return assignments to them as new variables. + * Also return a new expression which references the new variables. + * + * @param e + * @return */ + def extractCastVars(e: Expr): (Expr, Command) = e match + { + case EIsValid(ex) => val (ne, nc) = extractCastVars(ex) + (EIsValid(ne).setPos(e.pos), nc) + case EFromMaybe(ex) => val (ne, nc) = extractCastVars(ex) + (EFromMaybe(ne).setPos(e.pos), nc) + case EToMaybe(ex) => val (ne, nc) = extractCastVars(ex) + (EToMaybe(ne).setPos(e.pos), nc) + case EUop(op, ex) => val (ne, nc) = extractCastVars(ex) + (EUop(op, ne).setPos(e.pos), nc) + case EBinop(op, e1, e2) => val (ne1, nc1) = extractCastVars(e1) + val (ne2, nc2) = extractCastVars(e2) + (EBinop(op, ne1, ne2).setPos(e.pos), CSeq(nc1, nc2).setPos(nc1.pos)) + case EMemAccess(mem, index, Some(mask)) => val (ne, nc) = extractCastVars(index) + val (nm, ncm) = extractCastVars(mask) + (EMemAccess(mem, ne, Some(nm)).setPos(e.pos), CSeq(nc, ncm).setPos(e.pos)) + case EMemAccess(mem, index, None) => val (ne, nc) = extractCastVars(index) + (EMemAccess(mem, ne, None).setPos(e.pos), nc) + case EBitExtract(num, start, end) => val (ne, nc) = extractCastVars(num) + (EBitExtract(ne, start, end).setPos(e.pos), nc) + case ETernary(cond, tval, fval) => val (ncond, nc) = extractCastVars(cond) + val (net, nct) = extractCastVars(tval) + val (nef, ncf) = extractCastVars(fval) + (ETernary(ncond, net, nef).setPos(e.pos), CSeq(CSeq(nc, nct).setPos(e.pos), ncf).setPos(e.pos)) + case EApp(func, args) => val (nargs, nc) = extractCastVars(args) + (EApp(func, nargs).setPos(e.pos), nc) + case ECall(mod, args) => val (nargs, nc) = extractCastVars(args) + (ECall(mod, nargs).setPos(e.pos), nc) + case ECast(ctyp, e) => val (ne, nc) = extractCastVars(e) + val ncast = ECast(ctyp, ne) + ncast.typ = Some(ctyp) + val nassgn = freshTmp(ncast) + (nassgn.lhs, CSeq(nc, nassgn).setPos(e.pos)) + case _ => (e, CEmpty()) + } } \ No newline at end of file diff --git a/src/main/scala/pipedsl/typechecker/TypeInferenceWrapper.scala b/src/main/scala/pipedsl/typechecker/TypeInferenceWrapper.scala index 9bb8c90b..db2045de 100644 --- a/src/main/scala/pipedsl/typechecker/TypeInferenceWrapper.scala +++ b/src/main/scala/pipedsl/typechecker/TypeInferenceWrapper.scala @@ -5,7 +5,7 @@ import pipedsl.common.Syntax._ import pipedsl.typechecker.Subtypes.{areEqual, canCast, isSubtype} import pipedsl.common.Errors import pipedsl.common.Syntax.Latency.{Asynchronous, Combinational, Sequential} -import pipedsl.common.Utilities.{defaultReadPorts, defaultWritePorts, opt_func, typeMapModule} +import pipedsl.common.Utilities.{defaultReadPorts, defaultWritePorts, opt_func, typeMapFunc, typeMapModule} import pipedsl.typechecker.Environments.{Environment, TypeEnv} import scala.collection.mutable @@ -13,29 +13,36 @@ import scala.collection.mutable object TypeInferenceWrapper { type Subst = List[(Id, Type)] + type bool = Boolean def apply_subst_typ(subst: Subst, t: Type): Type = subst.foldLeft[Type](t)((t1, s) => subst_into_type(s._1, s._2, t1)) private def subst_into_type(typevar: Id, toType: Type, inType: Type): Type = inType match { - case t@TMemType(elem, addrSize, readLatency, writeLatency, readPorts, writePorts) => t.copy(elem = subst_into_type(typevar, toType, elem)) - case t1@TLockedMemType(t2@TMemType(elem, _, _, _, _, _), _, _) => t1.copy(t2.copy(elem = subst_into_type(typevar, toType, elem))) + case t@TMemType(elem, _, _, _, _, _) => + t.copy(elem = subst_into_type(typevar, toType, elem)).setPos(t.pos) + case t1@TLockedMemType(t2@TMemType(elem, _, _, _, _, _), _, _) => + t1.copy(t2.copy(elem = subst_into_type(typevar, toType, elem))).setPos(t1.pos) case TSizedInt(len, signedness) => TSizedInt(subst_into_type(typevar, toType, len).asInstanceOf[TBitWidth], - subst_into_type(typevar, toType, signedness).asInstanceOf[TSignedNess]) + subst_into_type(typevar, toType, signedness).asInstanceOf[TSignedNess]).setPos(inType.pos) case TString() => inType case TBool() => inType case TVoid() => inType case TSigned() => inType case TUnsigned() => inType - case TFun(args, ret) => TFun(args.map(a => subst_into_type(typevar, toType, a)), subst_into_type(typevar, toType, ret)) + case TFun(args, ret) => + TFun(args.map(a => subst_into_type(typevar, toType, a)), + subst_into_type(typevar, toType, ret)).setPos(inType.pos) case TNamedType(name) => if (name == typevar) toType else inType case TSignVar(name) => if (name == typevar) toType else inType - case TModType(inputs, refs, retType, name) => TModType(inputs.map(i => subst_into_type(typevar, toType, i)), refs.map(r => subst_into_type(typevar, toType, r)), retType match + case TModType(inputs, refs, retType, name) => + TModType(inputs.map(i => subst_into_type(typevar, toType, i)), + refs.map(r => subst_into_type(typevar, toType, r)), retType match { case Some(value) => Some(subst_into_type(typevar, toType, value)) case None => None - }, name) + }, name).setPos(inType.pos) case t: TBitWidth => t match { @@ -44,28 +51,40 @@ object TypeInferenceWrapper case TBitWidthAdd(b1, b2) => val t1 = TBitWidthAdd(subst_into_type(typevar, toType, b1).asInstanceOf[TBitWidth], subst_into_type(typevar, toType, b2).asInstanceOf[TBitWidth]) (t1.b1, t1.b2) match { - case (TBitWidthLen(len1), TBitWidthLen(len2)) => TBitWidthLen(len1 + len2) - case _ => t1 + case (TBitWidthLen(len1), TBitWidthLen(len2)) => TBitWidthLen(len1 + len2).setPos(inType.pos) + case _ => t1.setPos(inType.pos) } case TBitWidthMax(b1, b2) => val t1 = TBitWidthMax(subst_into_type(typevar, toType, b1).asInstanceOf[TBitWidth], subst_into_type(typevar, toType, b2).asInstanceOf[TBitWidth]) (t1.b1, t1.b2) match { - case (TBitWidthLen(len1), TBitWidthLen(len2)) => TBitWidthLen(len1.max(len2)) - case (TBitWidthLen(len), _ :TBitWidthVar) => TBitWidthLen(len) - case (_ :TBitWidthVar, TBitWidthLen(len)) => TBitWidthLen(len) - case _ => t1 + case (TBitWidthLen(len1), TBitWidthLen(len2)) => TBitWidthLen(len1.max(len2)).setPos(inType.pos) + case (TBitWidthLen(len), _ :TBitWidthVar) => TBitWidthLen(len).setPos(inType.pos) + case (_ :TBitWidthVar, TBitWidthLen(len)) => TBitWidthLen(len).setPos(inType.pos) + case _ => t1.setPos(inType.pos) } } } + private def type_subst_map(t :Type, tp_mp :mutable.HashMap[Id, Type]) :Type = t match { - case TSignVar(nm) => type_subst_map(tp_mp.getOrElse(nm, t), tp_mp) + case TSignVar(nm) => tp_mp.get(nm) match + { + case Some(value) => type_subst_map(value, tp_mp) + case None => t + } case sz@TSizedInt(len, sign) => - sz.copy(len = type_subst_map(len, tp_mp).asInstanceOf[TBitWidth], - sign = type_subst_map(sign, tp_mp).asInstanceOf[TSignedNess]) - case f@TFun(args, ret) => f.copy(args = args.map(type_subst_map(_, tp_mp)), ret = type_subst_map(ret, tp_mp)) +// println(len) +// println(sign) + val tmp = sz.copy(len = type_subst_map(len, tp_mp).copyMeta(sz).asInstanceOf[TBitWidth], + + sign = type_subst_map(sign, tp_mp).asInstanceOf[TSignedNess]) +// println(tmp.len) +// println(tmp.sign) + tmp + case f@TFun(args, ret) => + f.copy(args = args.map(type_subst_map(_, tp_mp)), ret = type_subst_map(ret, tp_mp)).copyMeta(f) case r@TRecType(name, fields) => r.copy(fields = fields.map((idtp) => (idtp._1, type_subst_map(idtp._2, tp_mp)))) case m@TMemType(elem, addrSize, readLatency, writeLatency, readPorts, writePorts) => m.copy(elem = type_subst_map(elem, tp_mp)) @@ -73,150 +92,159 @@ object TypeInferenceWrapper m.copy(inputs = inputs.map(type_subst_map(_, tp_mp)), refs = refs.map(type_subst_map(_, tp_mp))) case l@TLockedMemType(mem, idSz, limpl) => l.copy(mem = type_subst_map(mem, tp_mp).asInstanceOf[TMemType]) - case TNamedType(name) => type_subst_map(tp_mp.getOrElse(name, t), tp_mp) + case TNamedType(name) => tp_mp.get(name) match + { + case Some(value) => type_subst_map(value, tp_mp) + case None => t + } case m@TMaybe(btyp) => m.copy(btyp = type_subst_map(btyp, tp_mp)) case TBitWidthAdd(b1, b2) => val tmp = TBitWidthLen(type_subst_map(b1, tp_mp).asInstanceOf[TBitWidthLen].len + type_subst_map(b2, tp_mp).asInstanceOf[TBitWidthLen].len) - println(s"mapping $b1 + $b2 to ${tmp.len}") +// println(s"mapping $b1 + $b2 to ${tmp.len}") tmp case TBitWidthMax(b1, b2) => TBitWidthLen(Math.max(type_subst_map(b1, tp_mp).asInstanceOf[TBitWidthLen].len, type_subst_map(b2, tp_mp).asInstanceOf[TBitWidthLen].len)) - case TBitWidthVar(name) => type_subst_map(tp_mp.getOrElse(name, t), tp_mp) + case TBitWidthVar(name) => tp_mp.get(name) match + { + case Some(value) => type_subst_map(value, tp_mp) + case None => t + } case _ => t } - class TypeInference + class TypeInference(autocast :bool) { private var currentDef: Id = Id("-invalid-") private var counter = 0 - def checkProgram(p: Prog): Environment[Id, Type] = + def checkProgram(p: Prog): Prog = { - val funcEnvs = p.fdefs.foldLeft[Environment[Id, Type]](TypeEnv())((env, f) => + val (funcEnvs, newFuncs) = + p.fdefs.foldLeft[(Environment[Id, Type], List[FuncDef])]((TypeEnv(), List.empty[FuncDef]))((envNlst :(Environment[Id, Type], List[FuncDef]), f) => { + val env = envNlst._1 + val lst = envNlst._2 currentDef = f.name - checkFunc(f, env.asInstanceOf[TypeEnv]) + val (nenv, nfunc) = checkFunc(f, env.asInstanceOf[TypeEnv]) + (nenv, lst.prepended(nfunc)) }) - val modEnvs = p.moddefs.foldLeft[Environment[Id, Type]](funcEnvs)((env, m) => + val (modEnvs, newMods) = p.moddefs.foldLeft[(Environment[Id, Type], List[ModuleDef])]((funcEnvs, List.empty[ModuleDef]))((envNlst, m) => { + val env = envNlst._1 + val lst = envNlst._2 currentDef = m.name - checkModule(m, env.asInstanceOf[TypeEnv]) + val (nenv, nmod) = checkModule(m, env.asInstanceOf[TypeEnv]) + (nenv, lst.prepended(nmod)) }) - checkCircuit(p.circ, modEnvs) + val (_, newCirc) = checkCircuit(p.circ, modEnvs) + p.copy(fdefs = newFuncs.reverse, moddefs = newMods.reverse, circ = newCirc) } - def checkCircuit(c: Circuit, tenv: Environment[Id, Type]): Environment[Id, Type] = c match + def checkCircuit(c: Circuit, tenv: Environment[Id, Type]): (Environment[Id, Type], Circuit) = c match { - case CirSeq(c1, c2) => - { - val e1 = checkCircuit(c1, tenv) - checkCircuit(c2, e1) - } - case CirConnect(name, c) => val (t, env2) = checkCirExpr(c, tenv) - env2.add(name, t) - case CirExprStmt(ce) => checkCirExpr(ce, tenv)._2 + case cs@CirSeq(c1, c2) => + val (e1, nc1) = checkCircuit(c1, tenv) + val (e2, nc2) = checkCircuit(c2, e1) + (e2, cs.copy(c1 = nc1, c2 = nc2)) + case cc@CirConnect(name, ce) => + val (t, env2, nce) = checkCirExpr(ce, tenv) + (env2.add(name, t), cc.copy(c = nce)) + case ces@CirExprStmt(ce) => + val (_, nv, nce) = checkCirExpr(ce, tenv) + (nv, ces.copy(ce = nce)) } - private def checkCirExpr(c: CirExpr, tenv: Environment[Id, Type]): (Type, Environment[Id, Type]) = c match + private def checkCirExpr(c: CirExpr, tenv: Environment[Id, Type]): (Type, Environment[Id, Type], CirExpr) = c match { case CirMem(elemTyp, addrSize, numPorts) => - { if (numPorts > 2) throw TooManyPorts(c.pos, 2) val mtyp = TMemType(elemTyp, addrSize, Asynchronous, Asynchronous, numPorts, numPorts) - (mtyp, tenv) - } - case CirLock(mem, impl, _) => val mtyp: TMemType = tenv(mem).matchOrError(mem.pos, "lock instantiation", "memory") + c.typ = Some(mtyp) + (mtyp, tenv, c) + case CirLock(mem, impl, _) => + val mtyp: TMemType = tenv(mem).matchOrError(mem.pos, "lock instantiation", "memory") { case c: TMemType => c } mem.typ = Some(mtyp) val newtyp = TLockedMemType(mtyp, None, impl) c.typ = Some(newtyp) - (newtyp, tenv) - case CirLockMem(elemTyp, addrSize, impl, _, numPorts) => val mtyp = TMemType(elemTyp, addrSize, Asynchronous, Asynchronous, numPorts, numPorts) + (newtyp, tenv, c) + case CirLockMem(elemTyp, addrSize, impl, _, numPorts) => + val mtyp = TMemType(elemTyp, addrSize, Asynchronous, Asynchronous, numPorts, numPorts) val ltyp = TLockedMemType(mtyp, None, impl) c.typ = Some(ltyp) - (ltyp, tenv) + (ltyp, tenv, c) case CirRegFile(elemTyp, addrSize) => val mtyp = TMemType(elemTyp, addrSize, Combinational, Sequential, defaultReadPorts, defaultWritePorts) c.typ = Some(mtyp) - (mtyp, tenv) - case CirLockRegFile(elemTyp, addrSize, impl, szParams) => val mtyp = TMemType(elemTyp, addrSize, Combinational, Sequential, defaultReadPorts, defaultWritePorts) + (mtyp, tenv, c) + case CirLockRegFile(elemTyp, addrSize, impl, szParams) => + val mtyp = TMemType(elemTyp, addrSize, Combinational, Sequential, defaultReadPorts, defaultWritePorts) val idsz = szParams.headOption val ltyp = TLockedMemType(mtyp, idsz, impl) c.typ = Some(ltyp) - (ltyp, tenv) + (ltyp, tenv, c) case CirNew(mod, mods) => val mtyp = tenv(mod) mtyp match { case TModType(_, refs, _, _) => if (refs.length != mods.length) - { throw ArgLengthMismatch(c.pos, mods.length, refs.length) - } refs.zip(mods).foreach { case (reftyp, mname) => - if (!(isSubtype(tenv(mname), reftyp))) - { - throw UnexpectedSubtype(mname.pos, mname.toString, reftyp, tenv(mname)) - } - } - (mtyp, tenv) + if (!isSubtype(tenv(mname), reftyp)) + throw UnexpectedSubtype(mname.pos, mname.toString, reftyp, tenv(mname)) } + (mtyp, tenv, c) case x => throw UnexpectedType(c.pos, c.toString, "Module Type", x) } - case CirCall(mod, inits) => - { + case cc@CirCall(mod, inits) => val mtyp = tenv(mod) mtyp match { case TModType(ityps, _, _, _) => - { if (ityps.length != inits.length) - { throw ArgLengthMismatch(c.pos, inits.length, ityps.length) - } - ityps.zip(inits).foreach + val fixed_args = ityps.zip(inits).map { case (expectedT, arg) => - { - val (subst, atyp, aenv) = infer(tenv.asInstanceOf[TypeEnv], arg) - if (!isSubtype(atyp, expectedT)) - { - throw UnexpectedSubtype(arg.pos, arg.toString, expectedT, atyp) - } - } + val (subst, atyp, aenv, a_fixed) = infer(tenv.asInstanceOf[TypeEnv], arg) + if (!isSubtype(atyp, expectedT)) + throw UnexpectedSubtype(arg.pos, arg.toString, expectedT, atyp) + a_fixed } - (mtyp, tenv) - } + (mtyp, tenv, cc.copy(args = fixed_args)) case x => throw UnexpectedType(c.pos, c.toString, "Module Type", x) } - } } - def checkModule(m: ModuleDef, env: TypeEnv): Environment[Id, Type] = + def checkModule(m: ModuleDef, env: TypeEnv): (Environment[Id, Type], ModuleDef) = { val inputTypes = m.inputs.map(p => p.typ) val modTypes = m.modules.map(m => replaceNamedType(m.typ, env)) val modEnv = env.add(m.name, TModType(inputTypes, modTypes, m.ret, Some(m.name))) val inEnv = m.inputs.foldLeft[Environment[Id, Type]](modEnv)((env, p) => env.add(p.name, p.typ)) val pipeEnv = m.modules.zip(modTypes).foldLeft[Environment[Id, Type]](inEnv)((env, m) => env.add(m._1.name, m._2)) - val (_, subst) = checkCommand(m.body, pipeEnv.asInstanceOf[TypeEnv], List()) + val (fixed_cmd, _, subst) = checkCommand(m.body, pipeEnv.asInstanceOf[TypeEnv], List()) val hash = mutable.HashMap.from(subst) typeMapModule(m, opt_func(type_subst_map(_, hash))) - println("SUBSTITUTIONS:\n" + subst) - modEnv + (modEnv, m.copy(body = fixed_cmd).copyMeta(m)) } - def checkFunc(f: FuncDef, env: TypeEnv): Environment[Id, Type] = + def checkFunc(f: FuncDef, env: TypeEnv): (Environment[Id, Type], FuncDef) = { val inputTypes = f.args.map(a => a.typ) val funType = TFun(inputTypes, f.ret) val funEnv = env.add(f.name, funType) val inEnv = f.args.foldLeft[Environment[Id, Type]](funEnv)((env, a) => env.add(a.name, a.typ)) - checkCommand(f.body, inEnv.asInstanceOf[TypeEnv], List()) - funEnv + val (fixed_cmd, _, subst) = checkCommand(f.body, inEnv.asInstanceOf[TypeEnv], List()) + val hash = mutable.HashMap.from(subst) + typeMapFunc(f, opt_func(type_subst_map(_, hash))) +// println("SUBSTITUTIONS:\n" + subst) + //TODO this is filler + (funEnv, f.copy(body = fixed_cmd).setPos(f.pos)) } private def replaceNamedType(t: Type, tenv: TypeEnv): Type = t match @@ -228,7 +256,7 @@ object TypeInferenceWrapper /*INVARIANTS Transforms the argument sub by composing any additional substitution Transforms the argument env by subbing in the returned substitution and adding any relevatn variables */ - def checkCommand(c: Command, env: TypeEnv, sub: Subst): (TypeEnv, Subst) = + def checkCommand(c: Command, env: TypeEnv, sub: Subst): (Command, TypeEnv, Subst) = { /*println(c) println(c.pos)*/ @@ -239,82 +267,92 @@ object TypeInferenceWrapper { case t@TMemType(elem, addrSize, readLatency, writeLatency, readPorts, writePorts) => mem.evar match { - case Some(value) => val (s, t, e) = infer(env, value) + case Some(value) => val (s, t, e, _) = infer(env, value) val tempSub = compose_subst(sub, s) val tNew = apply_subst_typ(tempSub, t) - val newSub = compose_subst(tempSub, unify(tNew, TSizedInt(TBitWidthLen(addrSize), TUnsigned()/*unsigned = true*/))) - (e.apply_subst_typeenv(newSub), newSub) - case None => (env, sub) + val newSub = compose_subst(tempSub, unify(tNew, TSizedInt(TBitWidthLen(addrSize), TUnsigned()))._1) + (c, e.apply_subst_typeenv(newSub), newSub) + case None => (c, env, sub) } case TLockedMemType(TMemType(_, addrSize, _, _, _, _), idSz, limpl) => mem.evar match { - case Some(value) => val (s, t, e) = infer(env, value) + case Some(value) => val (s, t, e, _) = infer(env, value) val tempSub = compose_subst(sub, s) val tNew = apply_subst_typ(tempSub, t) - val newSub = compose_subst(tempSub, unify(tNew, TSizedInt(TBitWidthLen(addrSize), TUnsigned()/*unsigned = true*/))) - (e.apply_subst_typeenv(newSub), newSub) - case None => (env, sub) + val newSub = compose_subst(tempSub, unify(tNew, TSizedInt(TBitWidthLen(addrSize), TUnsigned()/*unsigned = true*/))._1) + (c, e.apply_subst_typeenv(newSub), newSub) + case None => (c, env, sub) } case TModType(inputs, refs, retType, name) => if (mem.evar.isDefined) throw MalformedLockTypes("Pipeline modules can not have specific locks") - (env, sub) + (c, env, sub) case b => throw UnexpectedType(mem.id.pos, c.toString, "Memory or Module Type", b) } - case CEmpty() => (env, sub) - case CReturn(exp) => val (s, t, e) = infer(env, exp) + case CEmpty() => (c, env, sub) + case cr@CReturn(exp) => val (s, t, e, fixed) = infer(env, exp) val tempSub = compose_subst(sub, s) val tNew = apply_subst_typ(tempSub, t) val funT = env(currentDef) funT match { - case TFun(args, ret) => val retSub = compose_subst(tempSub, unify(tNew, ret)) - (e.apply_subst_typeenv(retSub), retSub) + case TFun(args, ret) => + val (subst, cast) = unify(tNew, ret) + /*TODO insert cast*/ + val retSub = compose_subst(tempSub, subst) + (cr.copy(exp = fixed).copyMeta(cr), e.apply_subst_typeenv(retSub), retSub) case b => throw UnexpectedType(c.pos, c.toString, funT.toString, b) } case CLockStart(mod) => if (!(env(mod).isInstanceOf[TMemType] || env(mod).isInstanceOf[TModType] || env(mod).isInstanceOf[TLockedMemType])) { throw UnexpectedType(mod.pos, c.toString, "Memory or Module Type", env(mod)) } - (env, sub) - case CIf(cond, cons, alt) => val (condS, condT, env1) = infer(env, cond) + (c, env, sub) + case i@CIf(cond, cons, alt) => + val (condS, condT, env1, fixed_cond) = infer(env, cond) val tempSub = compose_subst(sub, condS) val condTyp = apply_subst_typ(tempSub, condT) - val newSub = compose_subst(tempSub, unify(condTyp, TBool())) + val newSub = compose_subst(tempSub, unify(condTyp, TBool())._1) val newEnv = env1.apply_subst_typeenv(newSub) - val (consEnv, consSub) = checkCommand(cons, newEnv, newSub) + val (fixed_cons, consEnv, consSub) = checkCommand(cons, newEnv, newSub) val newEnv2 = newEnv.apply_subst_typeenv(consSub) - val (altEnv, altSub) = checkCommand(alt, newEnv2, consSub) //TODO: Intersection of both envs? - (consEnv.apply_subst_typeenv(altSub).intersect(altEnv).asInstanceOf[TypeEnv], altSub) + val (fixed_alt, altEnv, altSub) = checkCommand(alt, newEnv2, consSub) //TODO: Intersection of both envs? + (i.copy(cond = fixed_cond, cons = fixed_cons, alt = fixed_alt).copyMeta(i), + consEnv.apply_subst_typeenv(altSub).intersect(altEnv).asInstanceOf[TypeEnv], altSub) case CLockEnd(mod) => if (!(env(mod).isInstanceOf[TMemType] || env(mod).isInstanceOf[TModType] || env(mod).isInstanceOf[TLockedMemType])) { throw UnexpectedType(mod.pos, c.toString, "Memory or Module Type", env(mod)) } - (env, sub) - case CSplit(cases, default) => //TODO - var (runningEnv, runningSub) = checkCommand(default, env, sub) + (c, env, sub) + case cs@CSplit(cases, default) => //TODO + var (fixed_def, runningEnv, runningSub) = checkCommand(default, env, sub) + var fixed_cases : List[CaseObj] = List() for (c <- cases) { - val (condS, condT, env1) = infer(env, c.cond) + val (condS, condT, env1, fixed_cond) = infer(env, c.cond) val tempSub = compose_subst(runningSub, condS) val condTyp = apply_subst_typ(tempSub, condT) - val newSub = compose_subst(tempSub, unify(condTyp, TBool())) + val newSub = compose_subst(tempSub, unify(condTyp, TBool())._1) /*apply substitution to original environmnet, which you will use to check the body*/ val newEnv = env1.apply_subst_typeenv(newSub) - val (caseEnv, caseSub) = checkCommand(c.body, newEnv, newSub) + val (fixed_bod, caseEnv, caseSub) = checkCommand(c.body, newEnv, newSub) + fixed_cases = fixed_cases :+ c.copy(cond = fixed_cond, body = fixed_bod).setPos(c.pos) runningSub = caseSub runningEnv = runningEnv.apply_subst_typeenv(runningSub).intersect(caseEnv).asInstanceOf[TypeEnv] } - (runningEnv, runningSub) - case CExpr(exp) => val (s, t, e) = infer(env, exp) + (cs.copy(cases = fixed_cases, default = fixed_def).copyMeta(cs), runningEnv, runningSub) + case ce@CExpr(exp) => val (s, t, e, fixed) = infer(env, exp) val retS = compose_subst(sub, s) - (e.apply_subst_typeenv(retS), retS) //TODO - /*TODO is this right? I don't know. Maybe someone else does :)*/ case CCheckSpec(isBlocking) => (env, sub) - case CVerify(handle, args, preds) => (env, sub) - case CInvalidate(handle) => (env, sub) /*ODOT*/ case CTBar(c1, c2) => val (e, s) = checkCommand(c1, env, sub) - val (e2, s2) = checkCommand(c2, e, s) - (e2, s2) - case CPrint(evar) => (env, sub) - case CSpecCall(handle, pipe, args) => (env, sub) - case COutput(exp) => val (s, t, e) = infer(env, exp) + (ce.copy(exp = fixed).copyMeta(ce), e.apply_subst_typeenv(retS), retS) //TODO + /*TODO is this right? I don't know. Maybe someone else does :)*/ + case CCheckSpec(isBlocking) => (c, env, sub) + case CVerify(handle, args, preds) => (c, env, sub) + case CInvalidate(handle) => (c, env, sub) /*ODOT*/ + case ct@CTBar(c1, c2) => val (fixed1, e, s) = checkCommand(c1, env, sub) + val (fixed2, e2, s2) = checkCommand(c2, e, s) + (ct.copy(c1 = fixed1, c2 = fixed2).copyMeta(ct), e2, s2) + case CPrint(evar) => (c, env, sub) + case CSpecCall(handle, pipe, args) => (c, env, sub) + case co@COutput(exp) => + val (s, t, e, fixed) = infer(env, exp) val tempSub = compose_subst(sub, s) val tNew = apply_subst_typ(tempSub, t) val modT = env(currentDef) @@ -322,24 +360,35 @@ object TypeInferenceWrapper { case TModType(inputs, refs, retType, name) => retType match { - case Some(value) => val retSub = compose_subst(tempSub, unify(tNew, value)) - (e.apply_subst_typeenv(retSub), retSub) - case None => (e.apply_subst_typeenv(tempSub), tempSub) + case Some(value) => + val (subst, cast) = unify(tNew, value) + /*TODO insert cast*/ + val retSub = compose_subst(tempSub, subst) + (co.copy(exp = fixed).copyMeta(co), e.apply_subst_typeenv(retSub), retSub) + case None => (co.copy(exp = fixed).copyMeta(co), e.apply_subst_typeenv(tempSub), tempSub) } case b => throw UnexpectedType(c.pos, c.toString, modT.toString, b) } //How to check wellformedness with the module body - case CRecv(lhs, rhs, typ) => val (slhs, tlhs, lhsEnv) = lhs match - { - case EVar(id) => (List(), typ.getOrElse(generateTypeVar()), env) - case _ => infer(env, lhs) - } - val (srhs, trhs, rhsEnv) = infer(lhsEnv, rhs) + case cr@CRecv(lhs, rhs, typ) => + val (slhs, tlhs, lhsEnv, lhsFixed) = lhs match + { + case EVar(id) => (List(), typ.getOrElse(generateTypeVar()), env, lhs) + case _ => infer(env, lhs) + } + val (srhs, trhs, rhsEnv, rhsFixed) = infer(lhsEnv, rhs) val tempSub = compose_many_subst(sub, slhs, srhs) val lhstyp = apply_subst_typ(tempSub, tlhs) val rhstyp = apply_subst_typ(tempSub, trhs) - val s1 = unify(rhstyp, lhstyp) + lhs.typ = Some(lhstyp) + rhs.typ = Some(rhstyp) + val (s1, cast) = unify(rhstyp, lhstyp) + /*TODO insert cast*/ val sret = compose_many_subst(tempSub, s1, typ match - { case Some(value) => compose_subst(unify(lhstyp, value), unify(rhstyp, value)) + { case Some(value) => + val (s2, c2) = unify(lhstyp, value) + val (s3, c3) = unify(rhstyp, value) + /*TODO insert cast*/ + compose_subst(s2, s3) case None => List() }) val newEnv = lhs match @@ -347,16 +396,21 @@ object TypeInferenceWrapper case EVar(id) => rhsEnv.add(id, tlhs) case _ => rhsEnv } - (newEnv.asInstanceOf[TypeEnv].apply_subst_typeenv(sret), sret) - case CAssign(lhs, rhs, typ) => + (cr.copy(lhs = lhsFixed, rhs = rhsFixed).copyMeta(cr), newEnv.asInstanceOf[TypeEnv].apply_subst_typeenv(sret), sret) + case ca@CAssign(lhs, rhs, typ) => val (slhs, tlhs, lhsEnv) = (List(), typ.getOrElse(generateTypeVar()), env) - val (srhs, trhs, rhsEnv) = infer(lhsEnv, rhs) + val (srhs, trhs, rhsEnv, rhsFixed) = infer(lhsEnv, rhs) val tempSub = compose_many_subst(sub, slhs, srhs) val lhstyp = apply_subst_typ(tempSub, tlhs) val rhstyp = apply_subst_typ(tempSub, trhs) - val s1 = unify(rhstyp, lhstyp) + val (s1, cast) = unify(rhstyp, lhstyp) + /*TODO insert cast*/ val sret = compose_many_subst(tempSub, s1, typ match - { case Some(value) => compose_subst(unify(lhstyp, value), unify(rhstyp, value)) + { case Some(value) => + val (s2, c2) = unify(lhstyp, value) + val (s3, c3) = unify(rhstyp, value) + /*TODO insert cast*/ + compose_subst(s2, s3) case None => List() }) val newEnv = lhs match @@ -366,11 +420,12 @@ object TypeInferenceWrapper } lhs.typ = Some(lhstyp) rhs.typ = Some(rhstyp) - (newEnv.asInstanceOf[TypeEnv].apply_subst_typeenv(sret), sret) - case CSeq(c1, c2) => val (e1, s) = checkCommand(c1, env, sub) - val (e2, s2) = checkCommand(c2, e1, s) - (e2, s2) - case _:InternalCommand => (env, sub) + (ca.copy(rhs = rhsFixed).copyMeta(ca), newEnv.asInstanceOf[TypeEnv].apply_subst_typeenv(sret), sret) + case cs@CSeq(c1, c2) => + val (fixed1, e1, s) = checkCommand(c1, env, sub) + val (fixed2, e2, s2) = checkCommand(c2, e1, s) + (cs.copy(c1 = fixed1, c2 = fixed2).copyMeta(cs), e2, s2) + case _:InternalCommand => (c, env, sub) } } @@ -392,13 +447,13 @@ object TypeInferenceWrapper TSignVar(Id("__SIGN__" + counter)) } - private def occursIn(name: Id, b: Type): Boolean = b match + private def occursIn(name: Id, b: Type): bool = b match { case TSizedInt(len, unsigned) => occursIn(name, len) case TString() => false case TVoid() => false case TBool() => false - case TFun(args, ret) => args.foldLeft[Boolean](false)((b, t) => b || occursIn(name, t)) || occursIn(name, ret) + case TFun(args, ret) => args.foldLeft[bool](false)((b, t) => b || occursIn(name, t)) || occursIn(name, ret) case TRecType(name, fields) => false case TMemType(elem, addrSize, readLatency, writeLatency, readPorts, writePorts) => false case TModType(inputs, refs, retType, name) => false @@ -419,157 +474,208 @@ object TypeInferenceWrapper private def compose_many_subst(subs: Subst*): Subst = subs.foldRight[Subst](List())((s1, s2) => compose_subst(s1, s2)) /*for subtyping bit widths, t1 is the subtype, t2 is the supertype. so t2 is the expected private*/ - def unify(a: Type, b: Type): Subst = (a, b) match - { - case (t1: TNamedType, t2) => if (!occursIn(t1.name, t2)) List((t1.name, t2)) else List() - case (t1, t2: TNamedType) => if (!occursIn(t2.name, t1)) List((t2.name, t1)) else List() - case (t1 :TSignVar, t2 :TSignedNess) => if (!occursIn(t1.id, t2)) List((t1.id, t2)) else List() - case (t1 :TSignedNess, t2 :TSignVar) => if (!occursIn(t2.id, t1)) List((t2.id, t1)) else List() - case (_: TString, _: TString) => List() - case (_: TBool, _: TBool) => List() - case (_: TVoid, _: TVoid) => List() - case (_ :TSigned, _ :TSigned) => List() - case (_ :TUnsigned, _ :TUnsigned) => List() - case (TBool(), TSizedInt(len, u)) if len.asInstanceOf[TBitWidthLen].len == 1 && u.unsigned() => List() - case (TSizedInt(len, u), TBool()) if len.asInstanceOf[TBitWidthLen].len == 1 && u.unsigned() => List() - case (TSizedInt(len1, signed1), TSizedInt(len2, signed2)) => compose_subst(unify(len1, len2), unify(signed1, signed2)) //TODO: TSIZEDINT - case (TFun(args1, ret1), TFun(args2, ret2)) if args1.length == args2.length => - val s1 = args1.zip(args2).foldLeft[Subst](List())((s, t) => compose_subst(s, unify(apply_subst_typ(s, t._1), apply_subst_typ(s, t._2)))) - compose_subst(s1, unify(apply_subst_typ(s1, ret1), apply_subst_typ(s1, ret2))) - case (TModType(input1, refs1, retType1, name1), TModType(input2, refs2, retType2, name2)) => //TODO: Name?\ if (name1 != name2) throw UnificationError(a, b) - val s1 = input1.zip(input2).foldLeft[Subst](List())((s, t) => compose_subst(s, unify(apply_subst_typ(s, t._1), apply_subst_typ(s, t._2)))) - val s2 = refs1.zip(refs2).foldLeft[Subst](s1)((s, t) => compose_subst(s, unify(apply_subst_typ(s, t._1), apply_subst_typ(s, t._2)))) - compose_subst(s2, ((retType1, retType2) match - { - case (Some(t1: Type), Some(t2: Type)) => unify(apply_subst_typ(s2, t1), apply_subst_typ(s2, t2)) - case (None, None) => List() - case _ => throw UnificationError(a, b) - })) - case (TMemType(elem1, addr1, rl1, wl1, rp1, wp1), TMemType(elem2, addr2, rl2, wl2, rp2, wp2)) => if (addr1 != addr2 || rl1 != rl2 || wl1 != wl2 || rp1 < rp2 || wp1 < wp2) throw UnificationError(a, b) - unify(elem1, elem2) - case (t1: TBitWidthVar, t2: TBitWidth) => if (!occursIn(t1.name, t2)) List((t1.name, t2)) else List() - case (t1: TBitWidth, t2: TBitWidthVar) => if (!occursIn(t2.name, t1)) List((t2.name, t1)) else List() - - case (TBitWidthAdd(a1 :TBitWidthLen, a2), TBitWidthLen(len)) => println("UNIFY"); unify(a2, TBitWidthLen(len - a1.len)) - case (TBitWidthAdd(a2, a1 :TBitWidthLen), TBitWidthLen(len)) => println("UNIFY"); unify(a2, TBitWidthLen(len - a1.len)) - case (TBitWidthLen(len), TBitWidthAdd(a1 :TBitWidthLen, a2)) => println("UNIFY"); unify(a2, TBitWidthLen(len - a1.len)) - case (TBitWidthLen(len), TBitWidthAdd(a2, a1 :TBitWidthLen)) => println("UNIFY"); unify(a2, TBitWidthLen(len - a1.len)) - case (t1: TBitWidthLen, t2: TBitWidthLen) => if (t2.len < t1.len) throw UnificationError(t1, t2) else List() //TODO: need to figure this out: we want this subtyping rule to throw error when its being used, but not when its a binop!!! - case _ => throw UnificationError(a, b) + def unify(a: Type, b: Type): (Subst, bool) = { + println(s"unifying $a and $b") + (a, b) match + { + case (t1: TNamedType, t2) => if (!occursIn(t1.name, t2)) (List((t1.name, t2)), false) else (List(), false) + case (t1, t2: TNamedType) => if (!occursIn(t2.name, t1)) (List((t2.name, t1)), false) else (List(), false) + case (t1 :TSignVar, t2 :TSignedNess) => if (!occursIn(t1.id, t2)) (List((t1.id, t2)), false) else (List(), false) + case (t1 :TSignedNess, t2 :TSignVar) => if (!occursIn(t2.id, t1)) (List((t2.id, t1)), false) else (List(), false) + case (_: TString, _: TString) => (List(), false) + case (_: TBool, _: TBool) => (List(), false) + case (_: TVoid, _: TVoid) => (List(), false) + case (_ :TSigned, _ :TSigned) => (List(), false) + case (_ :TUnsigned, _ :TUnsigned) => (List(), false) + case (TBool(), TSizedInt(len, u)) if len.asInstanceOf[TBitWidthLen].len == 1 && u.unsigned() => (List(), false) + case (TSizedInt(len, u), TBool()) if len.asInstanceOf[TBitWidthLen].len == 1 && u.unsigned() => (List(), false) + case (TSizedInt(len1, signed1), TSizedInt(len2, signed2)) => + val (s1, c1) = unify(len1, len2); val (s2, c2) = unify(signed1, signed2) + (compose_subst(s1, s2), c1 || c2) + case (TFun(args1, ret1), TFun(args2, ret2)) if args1.length == args2.length => + val (s1, c1) = args1.zip(args2).foldLeft[(Subst, bool)]((List(), false))((sc, t) => + { + val (unif_s, unif_c) = unify(apply_subst_typ(sc._1, t._1), apply_subst_typ(sc._1, t._2)) + (compose_subst(sc._1, unif_s), unif_c || sc._2) + }) + val (s2, c2) = unify(apply_subst_typ(s1, ret1), apply_subst_typ(s1, ret2)) + (compose_subst(s1, s2), c1 || c2) + case (TModType(input1, refs1, retType1, name1), TModType(input2, refs2, retType2, name2)) => //TODO: Name?\ if (name1 != name2) throw UnificationError(a, b) + val (s1, c1) = input1.zip(input2).foldLeft[(Subst, bool)]((List(), false))((sc, t) => + { + val (unif_s, unif_c) = unify(apply_subst_typ(sc._1, t._1), apply_subst_typ(sc._1, t._2)) + (compose_subst(sc._1, unif_s), unif_c || sc._2) + }) + val (s2, c2) = refs1.zip(refs2).foldLeft[(Subst, bool)](s1, c1)((sc, t) => + { + val (unif_s, unif_c) = unify(apply_subst_typ(sc._1, t._1), apply_subst_typ(sc._1, t._2)) + (compose_subst(sc._1, unif_s), sc._2 || unif_c) + }) + val (s3, c3) = (retType1, retType2) match + { + case (Some(t1: Type), Some(t2: Type)) => unify(apply_subst_typ(s2, t1), apply_subst_typ(s2, t2)) + case (None, None) => (List(), false) + case _ => throw UnificationError(a, b) + } + (compose_subst(s2, s3), c2 || c3) + case (TMemType(elem1, addr1, rl1, wl1, rp1, wp1), TMemType(elem2, addr2, rl2, wl2, rp2, wp2)) => if (addr1 != addr2 || rl1 != rl2 || wl1 != wl2 || rp1 < rp2 || wp1 < wp2) throw UnificationError(a, b) + unify(elem1, elem2) + case (t1: TBitWidthVar, t2: TBitWidth) => if (!occursIn(t1.name, t2)) (List((t1.name, t2)), false) else (List(), false) + case (t1: TBitWidth, t2: TBitWidthVar) => if (!occursIn(t2.name, t1)) (List((t2.name, t1)), false) else (List(), false) + + case (TBitWidthAdd(a1 :TBitWidthLen, a2), TBitWidthLen(len)) => unify(a2, TBitWidthLen(len - a1.len)) + case (TBitWidthAdd(a2, a1 :TBitWidthLen), TBitWidthLen(len)) => unify(a2, TBitWidthLen(len - a1.len)) + case (TBitWidthLen(len), TBitWidthAdd(a1 :TBitWidthLen, a2)) => unify(a2, TBitWidthLen(len - a1.len)) + case (TBitWidthLen(len), TBitWidthAdd(a2, a1 :TBitWidthLen)) => unify(a2, TBitWidthLen(len - a1.len)) + case (TBitWidthAdd(a1 :TBitWidthVar, a2 :TBitWidthVar), TBitWidthLen(len)) => + if(len % 2 != 0) throw new RuntimeException(s"result of bitwidthadd should be even. Consider multiply. Found $len") + val (s1, c1) = unify(a1, TBitWidthLen(len / 2)) + val (s2, c2) = unify(a2, TBitWidthLen(len / 2)) + (compose_subst(s1, s2), c1 || c2) + case (TBitWidthLen(len), TBitWidthAdd(a1 :TBitWidthVar, a2 :TBitWidthVar)) => + if(len % 2 != 0) throw new RuntimeException(s"result of bitwidthadd should be even. Consider multiply. Found $len") + val (s1, c1) = unify(a1, TBitWidthLen(len / 2)) + val (s2, c2) = unify(a2, TBitWidthLen(len / 2)) + (compose_subst(s1, s2), c1 || c2) + case (t1: TBitWidthLen, t2: TBitWidthLen) => + if(autocast) + {if (t2.len < t1.len) throw UnificationError(t1, t2) else (List(), t1.len != t2.len)} //TODO: need to figure this out: we want this subtyping rule to throw error when its being used, but not when its a binop!!! + else + {if (t2.len != t1.len) throw UnificationError(t1, t2) else (List(), false)} + case _ => throw UnificationError(a, b) + } } //Updating the type environment with the new substitution whenever you generate one allows errors to be found :D //The environment returned is guaratneed to already have been substituted into with the returned substitution private - def infer(env: TypeEnv, e: Expr): (Subst, Type, TypeEnv) = e match - { - case EInt(v, base, bits) => - val sign = if (e.typ.isDefined) e.typ.get.asInstanceOf[TSizedInt].sign else generateSignTypeVar() - (List(), if(e.typ.isDefined) TSizedInt(TBitWidthLen(bits), sign) else generateTypeVar(), env) - case EString(v) => (List(), TString(), env) - case EBool(v) => (List(), TBool(), env) - case EUop(op, ex) => val (s, t, env1) = infer(env, ex) - val retType = generateTypeVar() - val tNew = apply_subst_typ(s, t) - val subst = unify(TFun(List(tNew), retType), uOpExpectedType(op)) - val retSubst = compose_subst(s, subst) - val retTyp = apply_subst_typ(retSubst, retType) - (retSubst, retTyp, env1.apply_subst_typeenv(retSubst)) - case EBinop(op, e1, e2) => - println(s"op: $op") - val (s1, t1, env1) = infer(env, e1) - val (s2, t2, env2) = infer(env1, e2) - println(s"inferred left: $t1;\tright: $t2") - val retType = generateTypeVar() - val subTemp = compose_subst(s1, s2) - val t1New = apply_subst_typ(subTemp, t1) - val t2New = apply_subst_typ(subTemp, t2) - val subst = unify(TFun(List(t1New, t2New), retType), binOpExpectedType(op)) - val retSubst = compose_many_subst(subTemp, subst) - val retTyp = apply_subst_typ(retSubst, retType) - val t1VNew = apply_subst_typ(retSubst, t1New) - val t2VNew = apply_subst_typ(retSubst, t2New) - e1.typ = Some(t1VNew) - e2.typ = Some(t2VNew) - println(s"decided left: $t1VNew;\tright: $t2VNew") - (retSubst, retTyp, env2.apply_subst_typeenv(retSubst)) - case EMemAccess(mem, index, wmask) => if (!(env(mem).isInstanceOf[TMemType] || env(mem).isInstanceOf[TLockedMemType])) throw UnexpectedType(e.pos, "Memory Access", "TMemtype", env(mem)) - - val retType = generateTypeVar() - val (s, t, env1) = infer(env, index) - val tTemp = apply_subst_typ(s, t) - val memt = env1(mem) match - { - case t@TMemType(_, _, _, _, _, _) => t - case TLockedMemType(t, _, _) => t - case _ => throw UnexpectedType(e.pos, "Memory Access", "TMemtype", env1(mem)) - } - val subst = unify(TFun(List(tTemp), retType), getMemAccessType(memt)) - val retSubst = compose_subst(s, subst) - val retTyp = apply_subst_typ(retSubst, retType) - (retSubst, retTyp, env1.apply_subst_typeenv(retSubst)) - case EBitExtract(num, start, end) => - val (s, t, e) = infer(env, num) - t match - { - case TSizedInt(TBitWidthLen(len), signedness) if len >= (math.abs(end - start) + 1) => - (s, TSizedInt(TBitWidthLen(math.abs(end - start) + 1), signedness), e) - case b => throw UnificationError(b, TSizedInt(TBitWidthLen(32), TUnsigned()/*true*/)) //TODO Add better error message - } //TODO - case ETernary(cond, tval, fval) => val (sc, tc, env1) = infer(env, cond) - val (st, tt, env2) = infer(env1, tval) - val (sf, tf, env3) = infer(env2, fval) - val substSoFar = compose_many_subst(sc, st, sf) - val tcNew = apply_subst_typ(substSoFar, tc) - val ttNew = apply_subst_typ(substSoFar, tt) - val tfNew = apply_subst_typ(substSoFar, tf) - val substc = unify(tcNew, TBool()) - val subst = unify(ttNew, tfNew) //TODO this will fail with bad subtyping stuff going on currently bc for sized ints, we don't care which one is bigger right - val retSubst = compose_many_subst(sc, st, sf, substc, subst) - val retType = apply_subst_typ(retSubst, ttNew) - (retSubst, retType, env3.apply_subst_typeenv(retSubst)) - case EApp(func, args) => val expectedType = env(func) - val retType = generateTypeVar() - var runningEnv: TypeEnv = env - var runningSubst: Subst = List() - var typeList: List[Type] = List() - for (a <- args) + def infer(env: TypeEnv, e: Expr): (Subst, Type, TypeEnv, Expr) = { + //println(e) + e match + { + case EInt(v, base, bits) => + val sign = if (e.typ.isDefined) e.typ.get.asInstanceOf[TSizedInt].sign else generateSignTypeVar() + (List(), if(e.typ.isDefined) TSizedInt(TBitWidthLen(bits), sign) else generateTypeVar(), env, e) + case EString(v) => (List(), TString(), env, e) + case EBool(v) => (List(), TBool(), env, e) + case u@EUop(op, ex) => + val (s, t, env1, fixed) = infer(env, ex) + val retType = generateTypeVar() + val tNew = apply_subst_typ(s, t) + val (subst, cast) = unify(TFun(List(tNew), retType), uOpExpectedType(op)) + /*TODO insert cast*/ + val retSubst = compose_subst(s, subst) + val retTyp = apply_subst_typ(retSubst, retType) + (retSubst, retTyp, env1.apply_subst_typeenv(retSubst), u.copy(ex = fixed).copyMeta(u)) + case b@EBinop(op, e1, e2) => + println(s"op: $op") + val (s1, t1, env1, fixed1) = infer(env, e1) + val (s2, t2, env2, fixed2) = infer(env1, e2) + println(s"inferred left: $t1;\tright: $t2") + val retType = generateTypeVar() + val subTemp = compose_subst(s1, s2) + val t1New = apply_subst_typ(subTemp, t1) + val t2New = apply_subst_typ(subTemp, t2) + val (subst, cast) = unify(TFun(List(t1New, t2New), retType), binOpExpectedType(op)) + + /*TODO insert cast*/ + val retSubst = compose_many_subst(subTemp, subst) + val retTyp = apply_subst_typ(retSubst, retType) + val t1VNew = apply_subst_typ(retSubst, t1New) + val t2VNew = apply_subst_typ(retSubst, t2New) + println(s"decided left: $t1VNew;\tright: $t2VNew") + println(s"needs cast: $cast") + fixed1.typ = Some(t1VNew) + fixed2.typ = Some(t2VNew) + // println(s"decided left: $t1VNew;\tright: $t2VNew") + (retSubst, retTyp, env2.apply_subst_typeenv(retSubst), b.copy(e1 = fixed1, e2 = fixed2).copyMeta(b)) + case m@EMemAccess(mem, index, wmask) => if (!(env(mem).isInstanceOf[TMemType] || env(mem).isInstanceOf[TLockedMemType])) throw UnexpectedType(e.pos, "Memory Access", "TMemtype", env(mem)) + + val retType = generateTypeVar() + val (s, t, env1, fixed_idx) = infer(env, index) + val tTemp = apply_subst_typ(s, t) + val memt = env1(mem) match { - val (sub, typ, env1) = infer(runningEnv, a) - runningSubst = compose_subst(runningSubst, sub) - typeList = typeList :+ typ - runningEnv = env1 + case t@TMemType(_, _, _, _, _, _) => t + case TLockedMemType(t, _, _) => t + case _ => throw UnexpectedType(e.pos, "Memory Access", "TMemtype", env1(mem)) } - typeList = typeList.map(t => apply_subst_typ(runningSubst, t)) - val subst = unify(TFun(typeList, retType), expectedType) - val retSubst = compose_subst(runningSubst, subst) - val retEnv = runningEnv.apply_subst_typeenv(retSubst) - val retTyp = apply_subst_typ(retSubst, retType) - (retSubst, retTyp, retEnv) - case ECall(mod, args) => if (!env(mod).isInstanceOf[TModType]) throw UnexpectedType(e.pos, "Module Call", "TModType", env(mod)) - val expectedType = getArrowModType(env(mod).asInstanceOf[TModType]) - val retType = generateTypeVar() - var runningEnv: TypeEnv = env - var runningSubst: Subst = List() - var typeList: List[Type] = List() - for (a <- args) + val (subst, cast) = unify(TFun(List(tTemp), retType), getMemAccessType(memt)) + /*TODO insert cast*/ + val retSubst = compose_subst(s, subst) + val retTyp = apply_subst_typ(retSubst, retType) + (retSubst, retTyp, env1.apply_subst_typeenv(retSubst), m.copy(index = fixed_idx).copyMeta(m)) + case b@EBitExtract(num, start, end) => + val (s, t, e, fixed_num) = infer(env, num) + t match { - val (sub, typ, env1) = infer(runningEnv, a) - runningSubst = compose_subst(runningSubst, sub) - typeList = typeList :+ typ - runningEnv = env1 - } - typeList = typeList.map(t => apply_subst_typ(runningSubst, t)) - val subst = unify(TFun(typeList, retType), expectedType) - val retSubst = compose_subst(runningSubst, subst) - val retEnv = runningEnv.apply_subst_typeenv(retSubst) - val retTyp = apply_subst_typ(retSubst, retType) - (retSubst, retTyp, retEnv) - case EVar(id) => (List(), env(id), env) - case ECast(ctyp, exp) => /*TODO this is wrong probably*/ - val (s, t, env1) = infer(env, exp) - val newT = apply_subst_typ(s, t) - if (!canCast(ctyp, newT)) throw Errors.IllegalCast(e.pos, ctyp, newT) - (s, ctyp, env1) + case TSizedInt(TBitWidthLen(len), signedness) if len >= (math.abs(end - start) + 1) => + (s, TSizedInt(TBitWidthLen(math.abs(end - start) + 1), signedness), e, b.copy(num = fixed_num).copyMeta(b)) + case b => throw UnificationError(b, TSizedInt(TBitWidthLen(32), TUnsigned())) //TODO Add better error message + } //TODO + case trn@ETernary(cond, tval, fval) => + val (sc, tc, env1, fixed_cond) = infer(env, cond) + val (st, tt, env2, fixed_tval) = infer(env1, tval) + val (sf, tf, env3, fixed_fval) = infer(env2, fval) + val substSoFar = compose_many_subst(sc, st, sf) + val tcNew = apply_subst_typ(substSoFar, tc) + val ttNew = apply_subst_typ(substSoFar, tt) + val tfNew = apply_subst_typ(substSoFar, tf) + val (substc, _) = unify(tcNew, TBool()) + val (subst, cast) = unify(ttNew, tfNew) //TODO this will fail with bad subtyping stuff going on currently bc for sized ints, we don't care which one is bigger right + /*TODO insert cast*/ + val retSubst = compose_many_subst(sc, st, sf, substc, subst) + val retType = apply_subst_typ(retSubst, ttNew) + (retSubst, retType, env3.apply_subst_typeenv(retSubst), trn.copy(cond = fixed_cond, tval = fixed_tval, fval = fixed_fval).copyMeta(trn)) + case ap@EApp(func, args) => val expectedType = env(func) + val retType = generateTypeVar() + var runningEnv: TypeEnv = env + var runningSubst: Subst = List() + var typeList: List[Type] = List() + var argList: List[Expr] = List() + for (a <- args) + { + val (sub, typ, env1, fixed_a) = infer(runningEnv, a) + runningSubst = compose_subst(runningSubst, sub) + typeList = typeList :+ typ + argList = argList :+ fixed_a + runningEnv = env1 + } + typeList = typeList.map(t => apply_subst_typ(runningSubst, t)) + val (subst, cast) = unify(TFun(typeList, retType), expectedType) + /*TODO insert cast*/ + val retSubst = compose_subst(runningSubst, subst) + val retEnv = runningEnv.apply_subst_typeenv(retSubst) + val retTyp = apply_subst_typ(retSubst, retType) + (retSubst, retTyp, retEnv, ap.copy(args = argList).copyMeta(ap)) + case ca@ECall(mod, args) => if (!env(mod).isInstanceOf[TModType]) throw UnexpectedType(e.pos, "Module Call", "TModType", env(mod)) + val expectedType = getArrowModType(env(mod).asInstanceOf[TModType]) + val retType = generateTypeVar() + var runningEnv: TypeEnv = env + var runningSubst: Subst = List() + var typeList: List[Type] = List() + var argList: List[Expr] = List() + for (a <- args) + { + val (sub, typ, env1, fixed_a) = infer(runningEnv, a) + runningSubst = compose_subst(runningSubst, sub) + typeList = typeList :+ typ + argList = argList :+ fixed_a + runningEnv = env1 + } + typeList = typeList.map(t => apply_subst_typ(runningSubst, t)) + val (subst, cast) = unify(TFun(typeList, retType), expectedType) + /*TODO insert cast*/ + val retSubst = compose_subst(runningSubst, subst) + val retEnv = runningEnv.apply_subst_typeenv(retSubst) + val retTyp = apply_subst_typ(retSubst, retType) + (retSubst, retTyp, retEnv, ca.copy(args = argList).copyMeta(ca)) + case EVar(id) => (List(), env(id), env, e) + case ECast(ctyp, exp) => /*TODO this is wrong probably*/ + val (s, t, env1, _) = infer(env, exp) + val newT = apply_subst_typ(s, t) + if (!canCast(ctyp, newT)) throw Errors.IllegalCast(e.pos, ctyp, newT) + (s, ctyp, env1, e) + } } diff --git a/src/test/scala/pipedsl/TypeAutoCastSuite.scala b/src/test/scala/pipedsl/TypeAutoCastSuite.scala new file mode 100644 index 00000000..7049a449 --- /dev/null +++ b/src/test/scala/pipedsl/TypeAutoCastSuite.scala @@ -0,0 +1,17 @@ +package pipedsl + +import org.scalatest.funsuite.AnyFunSuite + +import java.io.File + +class TypeAutoCastSuite extends AnyFunSuite + { + private val folder = "src/test/tests/autocastTests" + private val testFiles = getListOfTests(folder) + private val testFolder = new File(folder) + + testFiles.foreach(t => + {val testBaseName = getTestName(t) + test(testBaseName + " Typecheck") + {testTypecheck(testFolder, t, autocast = true)}}) + } diff --git a/src/test/scala/pipedsl/package.scala b/src/test/scala/pipedsl/package.scala index c250f98c..a59b38ef 100644 --- a/src/test/scala/pipedsl/package.scala +++ b/src/test/scala/pipedsl/package.scala @@ -43,10 +43,10 @@ package object pipedsl { assert(success) } - def testTypecheck(testDir: File, inputFile: File): Boolean = { + def testTypecheck(testDir: File, inputFile: File, autocast :Boolean = false): Boolean = { var doesTypecheck: Boolean = false try { - Main.runPasses(printOutput = true, inputFile, testDir, port_warn = false) + Main.runPasses(printOutput = true, inputFile, testDir, port_warn = false, autocast) doesTypecheck = true } catch { case _: Throwable => () @@ -59,7 +59,7 @@ package object pipedsl { def testBlueSpecCompile(testDir: File, inputFile: File, addrLockMod: Option[String] = None, memInit: Map[String, String]): Unit = { val _ = (pathToBluespecScript + " c " + testDir.getAbsolutePath).!! - Main.gen(testDir, inputFile, printStgInfo = false, debug = false, addrLockMod, memInit, port_warn = false) + Main.gen(testDir, inputFile, printStgInfo = false, debug = false, addrLockMod, memInit, port_warn = false, autocast = false) val exit = (pathToBluespecScript + " v " + testDir.getAbsolutePath).! deleteGeneratedFiles(testDir) deleteBSVFiles(testDir, memInit) @@ -68,7 +68,7 @@ package object pipedsl { def testBlueSpecSim(testDir: File, inputFile: File, addrLockMod: Option[String] = None, memInit: Map[String, String], simFile: Option[String] = None): Unit = { val _ = (pathToBluespecScript + " c " + testDir.getAbsolutePath).!! - Main.gen(testDir, inputFile, printStgInfo = false, debug = false, addrLockMod, memInit, port_warn = false) + Main.gen(testDir, inputFile, printStgInfo = false, debug = false, addrLockMod, memInit, port_warn = false, autocast = false) val exit = (pathToBluespecScript + " s " + testDir.getAbsolutePath + " " + FilenameUtils.getBaseName(inputFile.getName) + ".sim").! val success = exit == 0 && compareFiles(testDir, inputFile, "sim", simFile) deleteGeneratedFiles(testDir) diff --git a/src/test/tests/autocastTests/autocast-basic-pass.pdl b/src/test/tests/autocastTests/autocast-basic-pass.pdl new file mode 100644 index 00000000..4af4ea65 --- /dev/null +++ b/src/test/tests/autocastTests/autocast-basic-pass.pdl @@ -0,0 +1,159 @@ + +def helper1(a: int<32>, b:bool, c: String): int<32> { + d = a + 1<16>; + e = b && false; + if (e) { + f = c; + } + return d; +} + +def helper2(a:bool, b: bool): bool { + c = a && b; + return c; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } + call test1(input); +} + +pipe test2(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } else { + d = b; + } + call test2(input); +} + +pipe test3()[] { + a = true; + b = a; + c = a || b; + d = c || b; + if (c) { + e = 1<32>; + } + if (d) { + f = 1<32>; + } + call test3(); +} + +pipe test4()[] { + a = true; + b = false; + c = a == b; + d = 5<32>; + e = 6<32>; + f = e==d; + if (c) { + + } + if (f) { + + } + call test4(); +} + +pipe test5()[] { + a = 5<32>; + b = 6<32>; + c = a + b; + d = cast(c * b, int<32>); + e = c / d; + f = e % d; + g = e - f; + h = g > f; + i = g <= f; + j = h && i; + if (j) { + + } + call test5(); +} + + +pipe test6(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } else { + d = b; + } + call test6(input); +} + +pipe test7()[rf: uint<32>[32]] { + a = 1; + b = a; + start(rf); + acquire(rf[a], R); + c <- rf[a]; + release(rf[a]); + end(rf); + --- + d = c == a; + e = d && d; + call test7(); +} + +pipe test8()[rf: int<32>[32]] { + a = 5<32>; + b = true; + c = false; + if (helper2(helper2(b, c),b)) { + d = a; + } + f = a; + s = "yES"; + e = helper1(f, helper2(b, c), s); + if (e==f) { + + } + call test8(); +} + +pipe test9()[rf: int<32>[32]] { + a = true || false; + b = a; + c = b ; + d = b && c; + e = (b) ? d : c; + if (!e) { + + } + call test9(); +} + +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g <- call test10(f, c); + --- + h = g == b; + call test11(); +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/autocast-basic-pass.typechecksol b/src/test/tests/autocastTests/solutions/autocast-basic-pass.typechecksol new file mode 100644 index 00000000..9fb4ec93 --- /dev/null +++ b/src/test/tests/autocastTests/solutions/autocast-basic-pass.typechecksol @@ -0,0 +1 @@ +Passed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-basic-pass.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-basic-pass.typechecksol new file mode 100644 index 00000000..9fb4ec93 --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-basic-pass.typechecksol @@ -0,0 +1 @@ +Passed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-bit-width-tests.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-bit-width-tests.typechecksol new file mode 100644 index 00000000..9fb4ec93 --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-bit-width-tests.typechecksol @@ -0,0 +1 @@ +Passed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-base-type.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-base-type.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-base-type.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-memAccessToosmall.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-memAccessToosmall.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-memAccessToosmall.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-minus.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-minus.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-minus.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-mult.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-mult.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-mult.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-plus.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-plus.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-bit-too-small-plus.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-boolBinOp.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-boolBinOp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-boolBinOp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-call-args.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-call-args.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-call-args.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-call.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-call.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-call.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-eqBinOp.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-eqBinOp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-eqBinOp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-func-app-arg.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-func-app-arg.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-func-app-arg.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-funcApp.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-funcApp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-funcApp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-numBinOp.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-numBinOp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-numBinOp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/solutions/type-inference-fail-ternary.typechecksol b/src/test/tests/autocastTests/solutions/type-inference-fail-ternary.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/autocastTests/solutions/type-inference-fail-ternary.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-basic-pass.pdl b/src/test/tests/autocastTests/type-inference-basic-pass.pdl new file mode 100644 index 00000000..a30854a2 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-basic-pass.pdl @@ -0,0 +1,159 @@ + +def helper1(a: int<32>, b:bool, c: String): int<32> { + d = a + 1<32>; + e = b && false; + if (e) { + f = c; + } + return d; +} + +def helper2(a:bool, b: bool): bool { + c = a && b; + return c; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } + call test1(input); +} + +pipe test2(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } else { + d = b; + } + call test2(input); +} + +pipe test3()[] { + a = true; + b = a; + c = a || b; + d = c || b; + if (c) { + e = 1<32>; + } + if (d) { + f = 1<32>; + } + call test3(); +} + +pipe test4()[] { + a = true; + b = false; + c = a == b; + d = 5<32>; + e = 6<32>; + f = e==d; + if (c) { + + } + if (f) { + + } + call test4(); +} + +pipe test5()[] { + a = 5<32>; + b = 6<32>; + c = a + b; + d = cast(c * b, int<32>); + e = c / d; + f = e % d; + g = e - f; + h = g > f; + i = g <= f; + j = h && i; + if (j) { + + } + call test5(); +} + + +pipe test6(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } else { + d = b; + } + call test6(input); +} + +pipe test7()[rf: uint<32>[32]] { + a = 1; + b = a; + start(rf); + acquire(rf[a], R); + c <- rf[a]; + release(rf[a]); + end(rf); + --- + d = c == a; + e = d && d; + call test7(); +} + +pipe test8()[rf: int<32>[32]] { + a = 5<32>; + b = true; + c = false; + if (helper2(helper2(b, c),b)) { + d = a; + } + f = a; + s = "yES"; + e = helper1(f, helper2(b, c), s); + if (e==f) { + + } + call test8(); +} + +pipe test9()[rf: int<32>[32]] { + a = true || false; + b = a; + c = b ; + d = b && c; + e = (b) ? d : c; + if (!e) { + + } + call test9(); +} + +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g <- call test10(f, c); + --- + h = g == b; + call test11(); +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-bit-width-tests.pdl b/src/test/tests/autocastTests/type-inference-bit-width-tests.pdl new file mode 100644 index 00000000..b2a31e6e --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-bit-width-tests.pdl @@ -0,0 +1,61 @@ + +def helper1(a: int<32>, b:bool, c: String): int<32> { + d = a + 1; + f = d + 4; + if (f == d) { + return f; + } else {return d;} +} + +def helper2(a:bool, b: bool): bool { + c = a && b; + return c; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = 6 * 6; + int<32> b = a; + int<32> c = a + b; + call test1(c); +} + +pipe test2(input: int<32>)[rf: int<32>[32]] { + a = 1; + start(rf); + acquire(rf[a], R); + b <- rf[a]; + release(rf[a]); + end(rf); + --- + call test2(b); +} + +pipe test3(input: int<32>)[rf: int<32>[32]] { + a = 1; + int<32> b = a << 4; + c = a << 4; + call test3(c); +} + +pipe test4(input: int<32>)[rf: int<32>[32]] { + a = 15<32>; + int<32> b = cast(a{0:8}, int<32>); + call test4(a); +} + +pipe test5()[] { + a = 6 * 6; + int<6> b = a; + int<32> c = helper1(cast(a, int<32>), true, "hi"); + call test5(); +} + +pipe test6()[] { + a = 6 - 6; + int<3> b = a; + call test6(); +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-base-type.pdl b/src/test/tests/autocastTests/type-inference-fail-base-type.pdl new file mode 100644 index 00000000..72889371 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-base-type.pdl @@ -0,0 +1,10 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input + 2<32>; + if (a) { + + } +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-bit-too-small-memAccessToosmall.pdl b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-memAccessToosmall.pdl new file mode 100644 index 00000000..dd313404 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-memAccessToosmall.pdl @@ -0,0 +1,9 @@ + +pipe test6()[rf: int<32>[32]] { + int<64> a = 6 * 6; + c = rf[a]; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-bit-too-small-minus.pdl b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-minus.pdl new file mode 100644 index 00000000..1149577f --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-minus.pdl @@ -0,0 +1,9 @@ + +pipe test6()[] { + a = 6 - 6; + int<2> b = a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-bit-too-small-mult.pdl b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-mult.pdl new file mode 100644 index 00000000..737be003 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-mult.pdl @@ -0,0 +1,9 @@ + +pipe test6()[] { + a = 6 * 6; + int<5> b = a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-bit-too-small-plus.pdl b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-plus.pdl new file mode 100644 index 00000000..deabf477 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-bit-too-small-plus.pdl @@ -0,0 +1,9 @@ + +pipe test6()[] { + a = 6 + 6; + int<2> b = a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-boolBinOp.pdl b/src/test/tests/autocastTests/type-inference-fail-boolBinOp.pdl new file mode 100644 index 00000000..3a302da6 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-boolBinOp.pdl @@ -0,0 +1,9 @@ + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input; + b = a || a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-call-args.pdl b/src/test/tests/autocastTests/type-inference-fail-call-args.pdl new file mode 100644 index 00000000..379def08 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-call-args.pdl @@ -0,0 +1,18 @@ +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g = call test10(c, c); + h = g == b; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-call.pdl b/src/test/tests/autocastTests/type-inference-fail-call.pdl new file mode 100644 index 00000000..6bc02fad --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-call.pdl @@ -0,0 +1,18 @@ +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g = call test10(f, c); + h = g == d; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-eqBinOp.pdl b/src/test/tests/autocastTests/type-inference-fail-eqBinOp.pdl new file mode 100644 index 00000000..0d4bae05 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-eqBinOp.pdl @@ -0,0 +1,8 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = a == input; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-func-app-arg.pdl b/src/test/tests/autocastTests/type-inference-fail-func-app-arg.pdl new file mode 100644 index 00000000..c2bb8609 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-func-app-arg.pdl @@ -0,0 +1,12 @@ +def func(a: bool, b: int<32>): bool { + return b; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = func(a, a); +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-funcApp.pdl b/src/test/tests/autocastTests/type-inference-fail-funcApp.pdl new file mode 100644 index 00000000..f69d3e87 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-funcApp.pdl @@ -0,0 +1,12 @@ +def func(a: bool, b: int<32>): bool { + return b; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = func(a, input) + 5<32>; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-numBinOp.pdl b/src/test/tests/autocastTests/type-inference-fail-numBinOp.pdl new file mode 100644 index 00000000..3096b3d3 --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-numBinOp.pdl @@ -0,0 +1,8 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = a + a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/autocastTests/type-inference-fail-ternary.pdl b/src/test/tests/autocastTests/type-inference-fail-ternary.pdl new file mode 100644 index 00000000..e635be6e --- /dev/null +++ b/src/test/tests/autocastTests/type-inference-fail-ternary.pdl @@ -0,0 +1,9 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = input; + c = (b) ? a : b; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-basic-pass.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-basic-pass.typechecksol new file mode 100644 index 00000000..9fb4ec93 --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-basic-pass.typechecksol @@ -0,0 +1 @@ +Passed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-base-type.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-base-type.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-base-type.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-memAccessToosmall.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-memAccessToosmall.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-memAccessToosmall.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-minus.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-minus.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-minus.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-mult.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-mult.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-mult.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-plus.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-plus.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-bit-too-small-plus.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-boolBinOp.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-boolBinOp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-boolBinOp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-call-args.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-call-args.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-call-args.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-call.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-call.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-call.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-eqBinOp.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-eqBinOp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-eqBinOp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-func-app-arg.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-func-app-arg.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-func-app-arg.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-funcApp.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-funcApp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-funcApp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-numBinOp.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-numBinOp.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-numBinOp.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/solutions/type-inference-fail-ternary.typechecksol b/src/test/tests/typecheckTests/solutions/type-inference-fail-ternary.typechecksol new file mode 100644 index 00000000..e4d7046a --- /dev/null +++ b/src/test/tests/typecheckTests/solutions/type-inference-fail-ternary.typechecksol @@ -0,0 +1 @@ +Failed \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-basic-pass.pdl b/src/test/tests/typecheckTests/type-inference-basic-pass.pdl new file mode 100644 index 00000000..a30854a2 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-basic-pass.pdl @@ -0,0 +1,159 @@ + +def helper1(a: int<32>, b:bool, c: String): int<32> { + d = a + 1<32>; + e = b && false; + if (e) { + f = c; + } + return d; +} + +def helper2(a:bool, b: bool): bool { + c = a && b; + return c; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } + call test1(input); +} + +pipe test2(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } else { + d = b; + } + call test2(input); +} + +pipe test3()[] { + a = true; + b = a; + c = a || b; + d = c || b; + if (c) { + e = 1<32>; + } + if (d) { + f = 1<32>; + } + call test3(); +} + +pipe test4()[] { + a = true; + b = false; + c = a == b; + d = 5<32>; + e = 6<32>; + f = e==d; + if (c) { + + } + if (f) { + + } + call test4(); +} + +pipe test5()[] { + a = 5<32>; + b = 6<32>; + c = a + b; + d = cast(c * b, int<32>); + e = c / d; + f = e % d; + g = e - f; + h = g > f; + i = g <= f; + j = h && i; + if (j) { + + } + call test5(); +} + + +pipe test6(input: int<32>)[rf: int<32>[32]] { + a = input; + b = true; + c = b; + if (c) { + d = a + 5<32>; + } else { + d = b; + } + call test6(input); +} + +pipe test7()[rf: uint<32>[32]] { + a = 1; + b = a; + start(rf); + acquire(rf[a], R); + c <- rf[a]; + release(rf[a]); + end(rf); + --- + d = c == a; + e = d && d; + call test7(); +} + +pipe test8()[rf: int<32>[32]] { + a = 5<32>; + b = true; + c = false; + if (helper2(helper2(b, c),b)) { + d = a; + } + f = a; + s = "yES"; + e = helper1(f, helper2(b, c), s); + if (e==f) { + + } + call test8(); +} + +pipe test9()[rf: int<32>[32]] { + a = true || false; + b = a; + c = b ; + d = b && c; + e = (b) ? d : c; + if (!e) { + + } + call test9(); +} + +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g <- call test10(f, c); + --- + h = g == b; + call test11(); +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-bit-width-tests.pdl b/src/test/tests/typecheckTests/type-inference-bit-width-tests.pdl index 49580d16..b2a31e6e 100644 --- a/src/test/tests/typecheckTests/type-inference-bit-width-tests.pdl +++ b/src/test/tests/typecheckTests/type-inference-bit-width-tests.pdl @@ -4,7 +4,7 @@ def helper1(a: int<32>, b:bool, c: String): int<32> { f = d + 4; if (f == d) { return f; - } else { return d; } + } else {return d;} } def helper2(a:bool, b: bool): bool { @@ -16,33 +16,44 @@ pipe test1(input: int<32>)[rf: int<32>[32]] { a = 6 * 6; int<32> b = a; int<32> c = a + b; + call test1(c); } pipe test2(input: int<32>)[rf: int<32>[32]] { a = 1; - b = rf[a]; + start(rf); + acquire(rf[a], R); + b <- rf[a]; + release(rf[a]); + end(rf); + --- + call test2(b); } pipe test3(input: int<32>)[rf: int<32>[32]] { a = 1; int<32> b = a << 4; - int<5> c = a << 4; + c = a << 4; + call test3(c); } pipe test4(input: int<32>)[rf: int<32>[32]] { a = 15<32>; - int<32> b = a{0:8}; + int<32> b = cast(a{0:8}, int<32>); + call test4(a); } pipe test5()[] { a = 6 * 6; int<6> b = a; - int<64> c = helper1(a, true, "hi"); + int<32> c = helper1(cast(a, int<32>), true, "hi"); + call test5(); } pipe test6()[] { a = 6 - 6; int<3> b = a; + call test6(); } circuit { diff --git a/src/test/tests/typecheckTests/type-inference-fail-base-type.pdl b/src/test/tests/typecheckTests/type-inference-fail-base-type.pdl new file mode 100644 index 00000000..72889371 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-base-type.pdl @@ -0,0 +1,10 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input + 2<32>; + if (a) { + + } +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-memAccessToosmall.pdl b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-memAccessToosmall.pdl new file mode 100644 index 00000000..dd313404 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-memAccessToosmall.pdl @@ -0,0 +1,9 @@ + +pipe test6()[rf: int<32>[32]] { + int<64> a = 6 * 6; + c = rf[a]; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-minus.pdl b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-minus.pdl new file mode 100644 index 00000000..1149577f --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-minus.pdl @@ -0,0 +1,9 @@ + +pipe test6()[] { + a = 6 - 6; + int<2> b = a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-mult.pdl b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-mult.pdl new file mode 100644 index 00000000..737be003 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-mult.pdl @@ -0,0 +1,9 @@ + +pipe test6()[] { + a = 6 * 6; + int<5> b = a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-plus.pdl b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-plus.pdl new file mode 100644 index 00000000..deabf477 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-bit-too-small-plus.pdl @@ -0,0 +1,9 @@ + +pipe test6()[] { + a = 6 + 6; + int<2> b = a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-boolBinOp.pdl b/src/test/tests/typecheckTests/type-inference-fail-boolBinOp.pdl new file mode 100644 index 00000000..3a302da6 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-boolBinOp.pdl @@ -0,0 +1,9 @@ + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = input; + b = a || a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-call-args.pdl b/src/test/tests/typecheckTests/type-inference-fail-call-args.pdl new file mode 100644 index 00000000..379def08 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-call-args.pdl @@ -0,0 +1,18 @@ +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g = call test10(c, c); + h = g == b; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-call.pdl b/src/test/tests/typecheckTests/type-inference-fail-call.pdl new file mode 100644 index 00000000..6bc02fad --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-call.pdl @@ -0,0 +1,18 @@ +pipe test10(a: bool, b: int<32>)[rf: int<32>[32]]: int<32> { + output(5<32>); +} + +pipe test11()[rf: int<32>[32]] { + a = 5<32>; + b = 10<32>; + c = a + b; + d = false; + e = true; + f = e || d; + g = call test10(f, c); + h = g == d; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-eqBinOp.pdl b/src/test/tests/typecheckTests/type-inference-fail-eqBinOp.pdl new file mode 100644 index 00000000..0d4bae05 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-eqBinOp.pdl @@ -0,0 +1,8 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = a == input; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-func-app-arg.pdl b/src/test/tests/typecheckTests/type-inference-fail-func-app-arg.pdl new file mode 100644 index 00000000..c2bb8609 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-func-app-arg.pdl @@ -0,0 +1,12 @@ +def func(a: bool, b: int<32>): bool { + return b; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = func(a, a); +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-funcApp.pdl b/src/test/tests/typecheckTests/type-inference-fail-funcApp.pdl new file mode 100644 index 00000000..f69d3e87 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-funcApp.pdl @@ -0,0 +1,12 @@ +def func(a: bool, b: int<32>): bool { + return b; +} + +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = func(a, input) + 5<32>; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-numBinOp.pdl b/src/test/tests/typecheckTests/type-inference-fail-numBinOp.pdl new file mode 100644 index 00000000..3096b3d3 --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-numBinOp.pdl @@ -0,0 +1,8 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = a + a; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file diff --git a/src/test/tests/typecheckTests/type-inference-fail-ternary.pdl b/src/test/tests/typecheckTests/type-inference-fail-ternary.pdl new file mode 100644 index 00000000..e635be6e --- /dev/null +++ b/src/test/tests/typecheckTests/type-inference-fail-ternary.pdl @@ -0,0 +1,9 @@ +pipe test1(input: int<32>)[rf: int<32>[32]] { + a = true; + b = input; + c = (b) ? a : b; +} + +circuit { + r = memory(int<32>, 32); +} \ No newline at end of file