From cfdd9ddef365ad52b84cabce420af50d08281f3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B8ller?= Date: Mon, 9 Nov 2020 13:01:07 +0100 Subject: [PATCH] Cumulative updates --- README.md | 2 +- examples/cfa.tip | 4 +- src/tip/Tip.scala | 40 +++-- src/tip/analysis/AndersenAnalysis.scala | 17 +-- src/tip/analysis/AvailableExpAnalysis.scala | 14 +- .../ConstantPropagationAnalysis.scala | 4 +- src/tip/analysis/ControlFlowAnalysis.scala | 11 +- .../CopyConstantPropagationAnalysis.scala | 8 +- src/tip/analysis/DeclarationAnalysis.scala | 57 +++---- src/tip/analysis/LiveVarsAnalysis.scala | 10 +- src/tip/analysis/SignAnalysis.scala | 4 +- src/tip/analysis/SimpleSignAnalysis.scala | 8 +- src/tip/analysis/SteensgaardAnalysis.scala | 28 ++-- src/tip/analysis/TypeAnalysis.scala | 94 ++++++++---- src/tip/analysis/ValueAnalysis.scala | 16 +- src/tip/ast/Ast.scala | 52 +++---- src/tip/ast/AstNodeData.scala | 10 +- src/tip/ast/AstOps.scala | 77 ++++++---- src/tip/ast/AstPrinters.scala | 36 +++-- src/tip/ast/DepthFirstAstVisitor.scala | 31 ++-- src/tip/ast/TipNormalizers.scala | 52 ++++--- src/tip/ast/TipSublanguages.scala | 78 ++++++---- src/tip/cfg/CfgOps.scala | 6 +- src/tip/cfg/InterproceduralProgramCfg.scala | 40 +++-- src/tip/concolic/ConcolicEngine.scala | 14 +- src/tip/concolic/ExecutionTree.scala | 3 - src/tip/concolic/SMTSolver.scala | 13 +- src/tip/interpreter/ConcreteValues.scala | 5 + src/tip/interpreter/Interpreter.scala | 143 +++++++++++------- src/tip/interpreter/ValueSpecification.scala | 1 - src/tip/lattices/GenericLattices.scala | 4 +- src/tip/parser/TipParser.scala | 32 +++- src/tip/solvers/CubicSolver.scala | 8 +- src/tip/solvers/FixpointSolvers.scala | 7 +- src/tip/solvers/UnificationTerms.scala | 81 +++++----- src/tip/solvers/UnionFindSolver.scala | 4 +- src/tip/types/Types.scala | 93 ++++++++---- src/tip/util/Log.scala | 4 +- src/tip/util/TipProgramException.scala | 6 + 39 files changed, 669 insertions(+), 448 deletions(-) create mode 100644 src/tip/util/TipProgramException.scala diff --git a/README.md b/README.md index 6962b6e..b5c4f3c 100644 --- a/README.md +++ b/README.md @@ -143,8 +143,8 @@ To automatically format when the file is saved, go to File -> Settings..., under ## Authors -- [Gianluca Mezzetti](http://gmezzetti.name/) - [Anders Møller](http://cs.au.dk/~amoeller/) +- [Gianluca Mezzetti](http://gmezzetti.name/) with contributions from diff --git a/examples/cfa.tip b/examples/cfa.tip index d23f2c0..2ec464e 100644 --- a/examples/cfa.tip +++ b/examples/cfa.tip @@ -5,13 +5,13 @@ ide(k) { return k; } foo(n,f) { var r; if (n==0) { f=ide; } - r = (f)(n); + r = f(n); return r; } main() { var x,y; - x = 1;//input; + x = input; if (x>0) { y = foo(x,inc); } else { y = foo(x,dec); } return y; } \ No newline at end of file diff --git a/src/tip/Tip.scala b/src/tip/Tip.scala index 1c84ad4..97d9259 100644 --- a/src/tip/Tip.scala +++ b/src/tip/Tip.scala @@ -6,7 +6,7 @@ import org.parboiled2.ParseError import tip.analysis.FlowSensitiveAnalysis.{Analysis => dfa, AnalysisOption => dfo} import tip.analysis._ import tip.ast.AstNodeData._ -import tip.ast.AProgram +import tip.ast.{AProgram, NoNormalizer} import tip.concolic.ConcolicEngine import tip.cfg._ import tip.interpreter.ConcreteInterpreter @@ -20,7 +20,6 @@ import scala.util.{Failure, Success} * Options for running the TIP system. */ class RunOption { - val log = Log.logger[this.type]() /** * If set, construct the (intraprocedural) control-flow graph after parsing. @@ -82,7 +81,7 @@ class RunOption { */ def check(): Boolean = if (source == null) { - log.error(s"Source file/directory missing") + Tip.log.error(s"Source file/directory missing") false } else true @@ -158,9 +157,17 @@ object Tip extends App { */ def processFile(file: File, options: RunOption) = { try { - val program = Source.fromFile(file).mkString + val program = { + val bs = Source.fromFile(file) + try { + bs.mkString + } finally { + bs.close() + } + } // parse the program + log.verb("Parsing") val tipParser = new TipParser(program) val res = tipParser.InputLine.run() @@ -173,17 +180,21 @@ object Tip extends App { sys.exit(1) case Success(parsedNode: AProgram) => // run normalizer + log.verb("Normalizing") val programNode = options.normalizer.normalizeProgram(parsedNode) - Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out) + if (options.normalizer != NoNormalizer) + Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out) // run declaration analysis // (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]]) + log.verb("Declaration analysis") implicit val declData: DeclarationData = new DeclarationAnalysis(programNode).analyze() // run selected intraprocedural flow-sensitive analyses if (options.cfg | options.dfAnalysis.exists(p => p._2 != dfo.Disabled && !dfo.interprocedural(p._2))) { // generate control-flow graph + log.verb("Building intraprocedural control flow graphs") val wcfg = IntraproceduralProgramCfg.generateFromProgram(programNode) if (options.cfg) Output.output(file, OtherOutput(OutputKindE.cfg), wcfg.toDot({ x => @@ -195,6 +206,7 @@ object Tip extends App { if (!dfo.interprocedural(v)) { FlowSensitiveAnalysis.select(s, v, wcfg).foreach { an => // run the analysis + log.verb(s"Performing ${an.getClass.getSimpleName}") val res = an.analyze().asInstanceOf[Map[CfgNode, _]] Output.output(file, DataFlowOutput(s), wcfg.toDot(Output.labeler(res), Output.dotIder), options.out) } @@ -207,8 +219,10 @@ object Tip extends App { // generate control-flow graph val wcfg = if (options.cfa) { + log.verb("Building interprocedural control flow graph using control flow analysis") InterproceduralProgramCfg.generateFromProgramWithCfa(programNode) } else { + log.verb("Building interprocedural control flow graph") InterproceduralProgramCfg.generateFromProgram(programNode) } @@ -223,6 +237,7 @@ object Tip extends App { if (dfo.interprocedural(v)) { FlowSensitiveAnalysis.select(s, v, wcfg).foreach { an => // run the analysis + log.verb(s"Starting ${an.getClass.getSimpleName}") val res = an.analyze() val res2 = if (dfo.contextsensitive(v)) @@ -238,12 +253,14 @@ object Tip extends App { // run type analysis, if selected if (options.types) { // (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]]) + log.verb("Starting TypeAnalysis") implicit val typeData: TypeData = new TypeAnalysis(programNode).analyze() Output.output(file, OtherOutput(OutputKindE.types), programNode.toTypedString, options.out) } // run Andersen analysis, if selected if (options.andersen) { + log.verb("Starting AndersenAnalysis") val s = new AndersenAnalysis(programNode) s.analyze() s.pointsTo() @@ -251,6 +268,7 @@ object Tip extends App { // run Steensgaard analysis, if selected if (options.steensgaard) { + log.verb("Starting SteensgaardAnalysis") val s = new SteensgaardAnalysis(programNode) s.analyze() s.pointsTo() @@ -259,31 +277,34 @@ object Tip extends App { // run control-flow analysis, if selected if (options.cfa) { // TODO: skip if InterproceduralProgramCfg.generateFromProgramWithCfa has been executed above val s = new ControlFlowAnalysis(programNode) + log.verb("Starting ControlFlowAnalysis") s.analyze() } // execute the program, if selected if (options.run) { + log.verb("Starting ConcreteInterpreter") val intp = new ConcreteInterpreter(programNode) intp.semp() } // concolically execute the program, if selected if (options.concolic) { + log.verb("Starting ConcolicEngine") new ConcolicEngine(programNode).test() } - - log.info("Success") } } catch { + case e: TipProgramException => + log.error(e.getMessage) + sys.exit(1) case e: Exception => - log.error(s"Error: ${e.getMessage}", e) + log.error(s"Internal error: ${e.getMessage}", e) sys.exit(1) } } // parse options - Log.defaultLevel = Log.Level.Info val options = new RunOption() var i = 0 while (i < args.length) { @@ -322,6 +343,7 @@ object Tip extends App { options.concolic = true case "-verbose" => Log.defaultLevel = Log.Level.Verbose + log.level = Log.Level.Verbose case _ => log.error(s"Unrecognized option $s") printUsage() diff --git a/src/tip/analysis/AndersenAnalysis.scala b/src/tip/analysis/AndersenAnalysis.scala index ce3ffb0..944e433 100644 --- a/src/tip/analysis/AndersenAnalysis.scala +++ b/src/tip/analysis/AndersenAnalysis.scala @@ -6,7 +6,7 @@ import tip.util.Log import tip.ast.AstNodeData.DeclarationData import scala.language.implicitConversions -class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Null] with PointsToAnalysis { +class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Unit] with PointsToAnalysis { val log = Log.logger[this.type]() @@ -21,7 +21,7 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex val solver = new CubicSolver[Cell, Cell] import AstOps._ - val allTargets: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc) + val cells: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc) NormalizedForPointsToAnalysis.assertContainsProgram(program) NoRecords.assertContainsProgram(program) @@ -30,30 +30,27 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex * @inheritdoc */ def analyze(): Unit = - visit(program, null) + visit(program, ()) /** * Generates the constraints for the given sub-AST. * @param node the node for which it generates the constraints * @param arg unused for this visitor */ - def visit(node: AstNode, arg: Null): Unit = { + def visit(node: AstNode, arg: Unit): Unit = { implicit def identifierToTarget(id: AIdentifier): Var = Var(id) implicit def allocToTarget(alloc: AAlloc): Alloc = Alloc(alloc) node match { case AAssignStmt(id: AIdentifier, alloc: AAlloc, _) => ??? //<--- Complete here - case AAssignStmt(id1: AIdentifier, AUnaryOp(RefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here + case AAssignStmt(id1: AIdentifier, AVarRef(id2: AIdentifier, _), _) => ??? //<--- Complete here case AAssignStmt(id1: AIdentifier, id2: AIdentifier, _) => ??? //<--- Complete here case AAssignStmt(id1: AIdentifier, AUnaryOp(DerefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here - case AAssignStmt(AUnaryOp(_, id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here - case AAssignStmt(_: AIdentifier, ANull(_), _) => - case AAssignStmt(_: AIdentifier, _: AAtomicExpr, _) => - case ass: AAssignStmt => NormalizedForPointsToAnalysis.LanguageRestrictionViolation(s"Assignment $ass not expected") + case AAssignStmt(ADerefWrite(id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here case _ => } - visitChildren(node, null) + visitChildren(node, ()) } /** diff --git a/src/tip/analysis/AvailableExpAnalysis.scala b/src/tip/analysis/AvailableExpAnalysis.scala index 25fb146..33a18ec 100644 --- a/src/tip/analysis/AvailableExpAnalysis.scala +++ b/src/tip/analysis/AvailableExpAnalysis.scala @@ -14,7 +14,7 @@ abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit dec import tip.cfg.CfgOps._ import tip.ast.AstOps._ - val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingExpressions.map(UnlabelledNode[AExpr])) + val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingNonInputExpressions.map(UnlabelledNode[AExpr])) NoPointers.assertContainsProgram(cfg.prog) NoRecords.assertContainsProgram(cfg.prog) @@ -26,20 +26,20 @@ abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit dec case _: CfgFunEntryNode => Set() case r: CfgStmtNode => r.data match { - case ass: AAssignStmt => - ass.left match { + case as: AAssignStmt => + as.left match { case id: AIdentifier => - (s union ass.right.appearingExpressions.map(UnlabelledNode[AExpr])).filter { e => + (s union as.right.appearingNonInputExpressions.map(UnlabelledNode[AExpr])).filter { e => !(id.appearingIds subsetOf e.n.appearingIds) } case _ => ??? } case exp: AExpr => - s union exp.appearingExpressions.map(UnlabelledNode[AExpr]) + s union exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr]) case out: AOutputStmt => - s union out.value.appearingExpressions.map(UnlabelledNode[AExpr]) + s union out.exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr]) case ret: AReturnStmt => - s union ret.value.appearingExpressions.map(UnlabelledNode[AExpr]) + s union ret.exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr]) case _ => s } case _ => s diff --git a/src/tip/analysis/ConstantPropagationAnalysis.scala b/src/tip/analysis/ConstantPropagationAnalysis.scala index d1c6b38..3e1870e 100644 --- a/src/tip/analysis/ConstantPropagationAnalysis.scala +++ b/src/tip/analysis/ConstantPropagationAnalysis.scala @@ -49,13 +49,13 @@ object ConstantPropagationAnalysis { /** * Interprocedural analysis that uses the worklist solver with reachability and propagation-style. - * with call-string context sensivity. + * with call-string context sensitivity. */ class CallString(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends CallStringValueAnalysis(cfg, ConstantPropagationLattice) /** * Interprocedural analysis that uses the worklist solver with reachability and propagation-style. - * with functional-approach context sensivity. + * with functional-approach context sensitivity. */ class Functional(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends FunctionalValueAnalysis(cfg, ConstantPropagationLattice) } diff --git a/src/tip/analysis/ControlFlowAnalysis.scala b/src/tip/analysis/ControlFlowAnalysis.scala index 78de8b3..d0b1da5 100644 --- a/src/tip/analysis/ControlFlowAnalysis.scala +++ b/src/tip/analysis/ControlFlowAnalysis.scala @@ -8,7 +8,7 @@ import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData} import scala.language.implicitConversions class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData) - extends DepthFirstAstVisitor[Null] + extends DepthFirstAstVisitor[Unit] with Analysis[Map[AstNode, Set[AFunDeclaration]]] { val log = Log.logger[this.type]() @@ -35,9 +35,9 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData) * @inheritdoc */ def analyze(): Map[AstNode, Set[AFunDeclaration]] = { - visit(program, null) + visit(program, ()) val sol = solver.getSolution - log.info(s"Solution is:\n${sol.map { case (k, v) => s" [[$k]] = {${v.mkString(",")}}" }.mkString("\n")}") + log.info(s"Solution is:\n${sol.map { case (k, v) => s" \u27E6$k\u27E7 = {${v.mkString(",")}}" }.mkString("\n")}") sol.map(vardecl => vardecl._1.n -> vardecl._2.map(_.fun)) } @@ -46,7 +46,7 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData) * @param node the node for which it generates the constraints * @param arg unused for this visitor */ - def visit(node: AstNode, arg: Null) = { + def visit(node: AstNode, arg: Unit) = { /** * Get the declaration if the supplied AstNode is an identifier, @@ -63,9 +63,10 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData) node match { case fun: AFunDeclaration => ??? //<--- Complete here case AAssignStmt(id: AIdentifier, e, _) => ??? //<--- Complete here + case ACallFuncExpr(targetFun: AIdentifier, args, _) if decl(targetFun).isInstanceOf[AFunDeclaration] => ??? //<--- Complete here (or remove this case) case ACallFuncExpr(targetFun, args, _) => ??? //<--- Complete here case _ => } - visitChildren(node, null) + visitChildren(node, ()) } } diff --git a/src/tip/analysis/CopyConstantPropagationAnalysis.scala b/src/tip/analysis/CopyConstantPropagationAnalysis.scala index 75537bf..9c06520 100644 --- a/src/tip/analysis/CopyConstantPropagationAnalysis.scala +++ b/src/tip/analysis/CopyConstantPropagationAnalysis.scala @@ -58,8 +58,8 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration, } // assignments - case ass: AAssignStmt => - ass match { + case as: AAssignStmt => + as match { case AAssignStmt(id: AIdentifier, right, _) => val edges = assign(d, id.declaration, right) d match { @@ -68,11 +68,11 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration, case _ => edges } - case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$ass not allowed") + case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$as not allowed", as.loc) } // return statement - case ret: AReturnStmt => assign(d, AstOps.returnId, ret.value) + case ret: AReturnStmt => assign(d, AstOps.returnId, ret.exp) // all other kinds of statements: like no-ops case _ => List((d, IdEdge())) diff --git a/src/tip/analysis/DeclarationAnalysis.scala b/src/tip/analysis/DeclarationAnalysis.scala index 69f7ca1..28d4e4c 100644 --- a/src/tip/analysis/DeclarationAnalysis.scala +++ b/src/tip/analysis/DeclarationAnalysis.scala @@ -2,6 +2,7 @@ package tip.analysis import tip.ast.DepthFirstAstVisitor import tip.ast._ +import tip.util.TipProgramException /** * Declaration analysis, binds identifiers to their declarations. @@ -45,7 +46,7 @@ class DeclarationAnalysis(prog: AProgram) extends DepthFirstAstVisitor[Map[Strin case funDec: AFunDeclaration => // Associate to each parameter itself as definition val argsMap = funDec.params.foldLeft(Map[String, ADeclaration]()) { (acc, cur: AIdentifierDeclaration) => - extendEnv(acc, cur.value -> cur) + extendEnv(acc, cur.name -> cur) } // Visit the function body in the extended environment val extendedEnv = extendEnv(env, argsMap) @@ -58,30 +59,33 @@ class DeclarationAnalysis(prog: AProgram) extends DepthFirstAstVisitor[Map[Strin p.funs.foreach { fd => visit(fd, extended) } - case ident: AIdentifier => + case ident @ AIdentifier(name, loc) => // Associate with each identifier the definition in the environment try { - declResult += ident -> env(ident.value) + declResult += ident -> env(name) } catch { - case e: Exception => - throw new RuntimeException(s"Identifier $ident not declared", e) + case _: Exception => + throw new DeclarationError(s"Identifier ${ident.name} not declared ${loc.toStringLong}") } case AAssignStmt(id: AIdentifier, _, loc) => - if (env.contains(id.value)) { - env(id.value) match { + if (env.contains(id.name)) { + env(id.name) match { case f: AFunDeclaration => - throw new RuntimeException(s"Function identifier for function $f can not appears on the left-hand side of an assignment at $loc") + throw new DeclarationError(s"Function $f cannot appear on the left-hand side of an assignment ${loc.toStringLong}") case _ => } } visitChildren(node, env) - case AUnaryOp(RefOp, id, loc) => - id match { - case id: AIdentifier if env.contains(id.value) && env(id.value).isInstanceOf[AFunDeclaration] => - throw new RuntimeException(s"Cannot take address of function ${env(id.value)} at $loc") - case _: AIdentifier => // no problem - case _ => ??? // unexpected, only identifiers are allowed here by the parser - } + case AVarRef(id, loc) => + if (env.contains(id.name) && env(id.name).isInstanceOf[AFunDeclaration]) + throw new DeclarationError(s"Cannot take address of function ${env(id.name)} ${loc.toStringLong}") + visitChildren(node, env) + case ARecord(fields, _) => + fields.foldLeft(Set[String]())((s, f) => { + if (s.contains(f.field)) + throw new DeclarationError(s"Duplicate field name ${f.field} ${f.loc.toStringLong}") + s + f.field + }) visitChildren(node, env) case _ => // There is no alteration of the environment, just visit the children in the current environment @@ -92,38 +96,35 @@ class DeclarationAnalysis(prog: AProgram) extends DepthFirstAstVisitor[Map[Strin * Extend the environment `env` with the bindings in `ext`, checking that no re-definitions occur. * @param env the environment to extend * @param ext the bindings to add - * @return the extended environment if no conflict occurs, throws a RuntimeException otherwise + * @return the extended environment if no conflict occurs, throws a DeclarationError otherwise */ - def extendEnv(env: Map[String, ADeclaration], ext: Map[String, ADeclaration]): Map[String, ADeclaration] = { - // Check for conflicts - val conflicts = env.keys.toSet.intersect(ext.keys.toSet) - if (conflicts.nonEmpty) redefinition(conflicts.map(env(_))) - env ++ ext - } + def extendEnv(env: Map[String, ADeclaration], ext: Map[String, ADeclaration]): Map[String, ADeclaration] = + ext.foldLeft(env)((e, p) => extendEnv(e, p)) /** * Extend the environment `env` with the binding `pair`, checking that no re-definition occurs. * @param env the environment to extend * @param pair the binding to add - * @return the extended environment if no conflict occurs, throws a RuntimeException otherwise + * @return the extended environment if no conflict occurs, throws a DeclarationError otherwise */ def extendEnv(env: Map[String, ADeclaration], pair: (String, ADeclaration)): Map[String, ADeclaration] = { - if (env.contains(pair._1)) redefinition(Set(env(pair._1))) + if (env.contains(pair._1)) + throw new DeclarationError(s"Redefinition of identifier ${pair._1} ${pair._2.loc.toStringLong}") env + pair } /** * Returns a map containing the new declarations contained in the given sequence of variable declaration statements. - * If a variable is re-defined, a RuntimeException is thrown. + * If a variable is re-defined, a DeclarationError is thrown. * @param decls the sequence of variable declaration statements * @return a map associating with each name the node that declares it */ private def peekDecl(decls: Seq[AVarStmt]): Map[String, ADeclaration] = { - val allDecls = decls.flatMap(v => v.declIds.map(id => id.value -> id)) + val allDecls = decls.flatMap(v => v.declIds.map(id => id.name -> id)) allDecls.foldLeft(Map[String, ADeclaration]()) { (map, pair) => extendEnv(map, pair) } } - - def redefinition(conflicting: Set[ADeclaration]) = throw new RuntimeException(s"Redefinition of identifiers $conflicting") } + +class DeclarationError(message: String) extends TipProgramException(s"Symbol error: $message") diff --git a/src/tip/analysis/LiveVarsAnalysis.scala b/src/tip/analysis/LiveVarsAnalysis.scala index 182fd85..acdfad4 100644 --- a/src/tip/analysis/LiveVarsAnalysis.scala +++ b/src/tip/analysis/LiveVarsAnalysis.scala @@ -2,7 +2,6 @@ package tip.analysis import tip.ast._ import tip.cfg.CfgOps._ -import tip.ast.AstOps._ import tip.lattices._ import tip.ast.AstNodeData.DeclarationData @@ -14,20 +13,21 @@ import tip.cfg._ */ abstract class LiveVarsAnalysis(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis[CfgNode](cfg) { - import AstNodeData._ - val allVars: Set[ADeclaration] = cfg.nodes.flatMap(_.appearingIds) val lattice = new MapLattice(cfg.nodes, new PowersetLattice(allVars)) + NoPointers.assertContainsProgram(cfg.prog) + NoRecords.assertContainsProgram(cfg.prog) + def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = n match { case _: CfgFunExitNode => lattice.sublattice.bottom case r: CfgStmtNode => r.data match { case cond: AExpr => ??? //<--- Complete here - case ass: AAssignStmt => - ass.left match { + case as: AAssignStmt => + as.left match { case id: AIdentifier => ??? //<--- Complete here case _ => ??? } diff --git a/src/tip/analysis/SignAnalysis.scala b/src/tip/analysis/SignAnalysis.scala index 3858fd5..8e44ca5 100644 --- a/src/tip/analysis/SignAnalysis.scala +++ b/src/tip/analysis/SignAnalysis.scala @@ -47,13 +47,13 @@ object SignAnalysis { /** * Interprocedural analysis that uses the worklist solver with reachability and propagation-style. - * with call-string context sensivity. + * with call-string context sensitivity. */ class CallString(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends CallStringValueAnalysis(cfg, SignLattice) /** * Interprocedural analysis that uses the worklist solver with reachability and propagation-style. - * with functional-approach context sensivity. + * with functional-approach context sensitivity. */ class Functional(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends FunctionalValueAnalysis(cfg, SignLattice) } diff --git a/src/tip/analysis/SimpleSignAnalysis.scala b/src/tip/analysis/SimpleSignAnalysis.scala index 60ab0d7..f2bff50 100644 --- a/src/tip/analysis/SimpleSignAnalysis.scala +++ b/src/tip/analysis/SimpleSignAnalysis.scala @@ -3,7 +3,7 @@ package tip.analysis import tip.cfg.CfgOps._ import tip.cfg.{CfgNode, CfgStmtNode, ProgramCfg} import tip.lattices.{MapLattice, SignLattice} -import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData} +import tip.ast.AstNodeData.DeclarationData import tip.ast._ import tip.solvers.FixpointSolvers @@ -43,7 +43,7 @@ class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) ex def eval(exp: AExpr, env: statelattice.Element)(implicit declData: DeclarationData): valuelattice.Element = { import valuelattice._ exp match { - case id: AIdentifier => env(id.declaration) + case id: AIdentifier => env(id) case n: ANumber => num(n.value) case bin: ABinaryOp => val left = eval(bin.left, env) @@ -58,9 +58,6 @@ class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) ex case _ => ??? } case _: AInput => valuelattice.top - case AUnaryOp(RefOp, _, _) | AUnaryOp(DerefOp, _, _) | ANull(_) | AAlloc(_, _) | AAccess(_, _, _) => - NoPointers.LanguageRestrictionViolation(s"No pointers allowed in eval $exp") - case _: ACallFuncExpr => NoCalls.LanguageRestrictionViolation(s"No calls allowed in eval $exp") case _ => ??? } } @@ -87,7 +84,6 @@ class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) ex // assignments case AAssignStmt(id: AIdentifier, right, _) => ??? //<--- Complete here - case AAssignStmt(_: AUnaryOp, _, _) => NoPointers.LanguageRestrictionViolation(s"${r.data} not allowed") // all others: like no-ops case _ => s diff --git a/src/tip/analysis/SteensgaardAnalysis.scala b/src/tip/analysis/SteensgaardAnalysis.scala index ae19b38..d030902 100644 --- a/src/tip/analysis/SteensgaardAnalysis.scala +++ b/src/tip/analysis/SteensgaardAnalysis.scala @@ -11,7 +11,7 @@ import scala.language.implicitConversions * The analysis associates an [[StTerm]] with each variable declaration and expression node in the AST. * It is implemented using [[tip.solvers.UnionFindSolver]]. */ -class SteensgaardAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Null] with PointsToAnalysis { +class SteensgaardAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Unit] with PointsToAnalysis { val log = Log.logger[this.type]() @@ -25,14 +25,14 @@ class SteensgaardAnalysis(program: AProgram)(implicit declData: DeclarationData) */ def analyze(): Unit = // generate the constraints by traversing the AST and solve them on-the-fly - visit(program, null) + visit(program, ()) /** * Generates the constraints for the given sub-AST. * @param node the node for which it generates the constraints * @param arg unused for this visitor */ - def visit(node: AstNode, arg: Null): Unit = { + def visit(node: AstNode, arg: Unit): Unit = { implicit def identifierToTerm(id: AIdentifier): Term[StTerm] = IdentifierVariable(id) implicit def allocToTerm(alloc: AAlloc): Term[StTerm] = AllocVariable(alloc) @@ -40,15 +40,13 @@ class SteensgaardAnalysis(program: AProgram)(implicit declData: DeclarationData) log.verb(s"Visiting ${node.getClass.getSimpleName} at ${node.loc}") node match { case AAssignStmt(id1: AIdentifier, alloc: AAlloc, _) => ??? //<--- Complete here - case AAssignStmt(id1: AIdentifier, AUnaryOp(RefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here + case AAssignStmt(id1: AIdentifier, AVarRef(id2: AIdentifier, _), _) => ??? //<--- Complete here case AAssignStmt(id1: AIdentifier, id2: AIdentifier, _) => ??? //<--- Complete here case AAssignStmt(id1: AIdentifier, AUnaryOp(DerefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here - case AAssignStmt(AUnaryOp(_, id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here - case AAssignStmt(_: AIdentifier, _, _) => // ignore other assignments where left-hand-side is an identifier - case ass: AAssignStmt => NormalizedForPointsToAnalysis.LanguageRestrictionViolation(s"Not expecting other kinds of assignment: $ass") + case AAssignStmt(ADerefWrite(id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here case _ => // ignore other kinds of nodes } - visitChildren(node, null) + visitChildren(node, ()) } private def unify(t1: Term[StTerm], t2: Term[StTerm]): Unit = { @@ -98,7 +96,7 @@ object Fresh { var n = 0 - def next: Int = { + def next(): Int = { n += 1 n } @@ -114,7 +112,7 @@ sealed trait StTerm */ case class AllocVariable(alloc: AAlloc) extends StTerm with Var[StTerm] { - override def toString: String = s"[[alloc:${alloc.loc}]]" + override def toString: String = s"\u27E6alloc{${alloc.loc}}]]" } /** @@ -122,7 +120,7 @@ case class AllocVariable(alloc: AAlloc) extends StTerm with Var[StTerm] { */ case class IdentifierVariable(id: ADeclaration) extends StTerm with Var[StTerm] { - override def toString: String = s"[[$id]]" + override def toString: String = s"\u27E6$id\u27E7" } /** @@ -130,9 +128,9 @@ case class IdentifierVariable(id: ADeclaration) extends StTerm with Var[StTerm] */ case class FreshVariable(var id: Int = 0) extends StTerm with Var[StTerm] { - id = Fresh.next + id = Fresh.next() - override def toString: String = s"\u03B1$id" + override def toString: String = s"x$id" } /** @@ -142,7 +140,7 @@ case class PointerRef(of: Term[StTerm]) extends StTerm with Cons[StTerm] { val args: List[Term[StTerm]] = List(of) - def subst(v: Var[StTerm], t: Term[StTerm]): Term[StTerm] = PointerRef(of.subst(v, t)) // currently not used + def subst(v: Var[StTerm], t: Term[StTerm]): Term[StTerm] = PointerRef(of.subst(v, t)) - override def toString: String = s"&$of" + override def toString: String = s"\u2B61$of" } diff --git a/src/tip/analysis/TypeAnalysis.scala b/src/tip/analysis/TypeAnalysis.scala index efbd28f..f7f0fe6 100644 --- a/src/tip/analysis/TypeAnalysis.scala +++ b/src/tip/analysis/TypeAnalysis.scala @@ -2,14 +2,16 @@ package tip.analysis import tip.ast._ import tip.solvers._ -import tip.types._ +import tip.types.{AbsentFieldType, _} import tip.ast.AstNodeData._ -import tip.util.Log +import tip.util.{Log, TipProgramException} import AstOps._ +import scala.collection.mutable + /** * Unification-based type analysis. - * The analysis associates a [[tip.types.TipType]] with each variable declaration and expression node in the AST. + * The analysis associates a [[tip.types.Type]] with each variable declaration and expression node in the AST. * It is implemented using [[tip.solvers.UnionFindSolver]]. * * To novice Scala programmers: @@ -20,11 +22,11 @@ import AstOps._ * by `DeclarationAnalysis` and the type information produced by `TypeAnalysis`. * For more information about implicit parameters in Scala, see [[https://docs.scala-lang.org/tour/implicit-parameters.html]]. */ -class TypeAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Null] with Analysis[TypeData] { +class TypeAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Unit] with Analysis[TypeData] { val log = Log.logger[this.type]() - val solver = new UnionFindSolver[TipType] + val solver = new UnionFindSolver[Type] implicit val allFieldNames: List[String] = program.appearingFields.toList.sorted @@ -34,28 +36,60 @@ class TypeAnalysis(program: AProgram)(implicit declData: DeclarationData) extend def analyze(): TypeData = { // generate the constraints by traversing the AST and solve them on-the-fly - visit(program, null) + try { + visit(program, ()) + } catch { + case e: UnificationFailure => + throw new TipProgramException(s"Type error: ${e.getMessage}") + } + + // check for accesses to absent record fields + new DepthFirstAstVisitor[Unit] { + visit(program, ()) + + override def visit(node: AstNode, arg: Unit): Unit = { + node match { + case ac: AFieldAccess => + if (solver.find(node).isInstanceOf[AbsentFieldType.type]) + throw new TipProgramException(s"Type error: Reading from absent field ${ac.field} ${ac.loc.toStringLong}") + case as: AAssignStmt => + as.left match { + case dfw: ADirectFieldWrite => + if (solver.find(as.right).isInstanceOf[AbsentFieldType.type]) + throw new TipProgramException(s"Type error: Writing to absent field ${dfw.field} ${dfw.loc.toStringLong}") + case ifw: AIndirectFieldWrite => + if (solver.find(as.right).isInstanceOf[AbsentFieldType.type]) + throw new TipProgramException(s"Type error: Writing to absent field ${ifw.field} ${ifw.loc.toStringLong}") + case _ => + } + case _ => + } + visitChildren(node, ()) + } + } var ret: TypeData = Map() // close the terms and create the TypeData - new DepthFirstAstVisitor[Null] { - val sol: Map[Var[TipType], Term[TipType]] = solver.solution() - visit(program, null) + new DepthFirstAstVisitor[Unit] { + val sol: Map[Var[Type], Term[Type]] = solver.solution() + log.info(s"Solution (not yet closed):\n${sol.map { case (k, v) => s" \u27E6$k\u27E7 = $v" }.mkString("\n")}") + val freshvars: mutable.Map[Var[Type], Var[Type]] = mutable.Map() + visit(program, ()) // extract the type for each identifier declaration and each non-identifier expression - override def visit(node: AstNode, arg: Null): Unit = { + override def visit(node: AstNode, arg: Unit): Unit = { node match { case _: AIdentifier => case _: ADeclaration | _: AExpr => - ret += node -> Some(TipTypeOps.close(TipVar(node), sol).asInstanceOf[TipType]) + ret += node -> Some(TipTypeOps.close(VarType(node), sol, freshvars).asInstanceOf[Type]) case _ => } - visitChildren(node, null) + visitChildren(node, ()) } } - log.info(s"Inferred types are:\n${ret.map { case (k, v) => s" [[$k]] = ${v.get}" }.mkString("\n")}") + log.info(s"Inferred types:\n${ret.map { case (k, v) => s" \u27E6$k\u27E7 = ${v.get}" }.mkString("\n")}") ret } @@ -64,16 +98,22 @@ class TypeAnalysis(program: AProgram)(implicit declData: DeclarationData) extend * @param node the node for which it generates the constraints * @param arg unused for this visitor */ - def visit(node: AstNode, arg: Null): Unit = { + def visit(node: AstNode, arg: Unit): Unit = { log.verb(s"Visiting ${node.getClass.getSimpleName} at ${node.loc}") node match { case program: AProgram => ??? // <--- Complete here case _: ANumber => ??? // <--- Complete here case _: AInput => ??? // <--- Complete here - case iff: AIfStmt => ??? // <--- Complete here - case out: AOutputStmt => ??? // <--- Complete here - case whl: AWhileStmt => ??? // <--- Complete here - case ass: AAssignStmt => ??? // <--- Complete here + case is: AIfStmt => ??? // <--- Complete here + case os: AOutputStmt => ??? // <--- Complete here + case ws: AWhileStmt => ??? // <--- Complete here + case as: AAssignStmt => + as.left match { + case id: AIdentifier => ??? // <--- Complete here + case dw: ADerefWrite => ??? // <--- Complete here + case dfw: ADirectFieldWrite => ??? // <--- Complete here + case ifw: AIndirectFieldWrite => ??? // <--- Complete here + } case bin: ABinaryOp => bin.operator match { case Eqq => ??? // <--- Complete here @@ -81,31 +121,31 @@ class TypeAnalysis(program: AProgram)(implicit declData: DeclarationData) extend } case un: AUnaryOp => un.operator match { - case RefOp => ??? // <--- Complete here case DerefOp => ??? // <--- Complete here } case alloc: AAlloc => ??? // <--- Complete here + case ref: AVarRef => ??? // <--- Complete here case _: ANull => ??? // <--- Complete here case fun: AFunDeclaration => ??? // <--- Complete here case call: ACallFuncExpr => ??? // <--- Complete here case _: AReturnStmt => case rec: ARecord => - val fieldmap = rec.fields.foldLeft(Map[String, Term[TipType]]()) { (a, b) => + val fieldmap = rec.fields.foldLeft(Map[String, Term[Type]]()) { (a, b) => a + (b.field -> b.exp) } - unify(rec, TipRecord(allFieldNames.map { f => - fieldmap.getOrElse(f, TipAlpha(rec, f)) + unify(rec, RecordType(allFieldNames.map { f => + fieldmap.getOrElse(f, AbsentFieldType) })) - case ac: AAccess => - unify(ac.record, TipRecord(allFieldNames.map { f => - if (f == ac.field) TipVar(ac) else TipAlpha(ac, f) + case ac: AFieldAccess => + unify(ac.record, RecordType(allFieldNames.map { f => + if (f == ac.field) VarType(ac) else FreshVarType() })) case _ => } - visitChildren(node, null) + visitChildren(node, ()) } - private def unify(t1: Term[TipType], t2: Term[TipType]): Unit = { + private def unify(t1: Term[Type], t2: Term[Type]): Unit = { log.verb(s"Generating constraint $t1 = $t2") solver.unify(t1, t2) } diff --git a/src/tip/analysis/ValueAnalysis.scala b/src/tip/analysis/ValueAnalysis.scala index 11326c8..f48c76a 100644 --- a/src/tip/analysis/ValueAnalysis.scala +++ b/src/tip/analysis/ValueAnalysis.scala @@ -37,7 +37,7 @@ trait ValueAnalysisMisc { def eval(exp: AExpr, env: statelattice.Element)(implicit declData: DeclarationData): valuelattice.Element = { import valuelattice._ exp match { - case id: AIdentifier => env(id.declaration) + case id: AIdentifier => env(id) case n: ANumber => num(n.value) case bin: ABinaryOp => val left = eval(bin.left, env) @@ -52,9 +52,6 @@ trait ValueAnalysisMisc { case _ => ??? } case _: AInput => valuelattice.top - case AUnaryOp(RefOp, _, _) | AUnaryOp(DerefOp, _, _) | ANull(_) | AAlloc(_, _) | AAccess(_, _, _) => - NoPointers.LanguageRestrictionViolation(s"No pointers allowed in eval $exp") - case _: ACallFuncExpr => NoCalls.LanguageRestrictionViolation(s"No calls allowed in eval $exp") case _ => ??? } } @@ -74,7 +71,6 @@ trait ValueAnalysisMisc { // assignments case AAssignStmt(id: AIdentifier, right, _) => ??? //<--- Complete here - case AAssignStmt(_: AUnaryOp, _, _) => NoPointers.LanguageRestrictionViolation(s"${r.data} not allowed") // all others: like no-ops case _ => s @@ -123,7 +119,7 @@ trait InterprocValueAnalysisFunctions[L <: LatticeWithOps] extends MapLiftLattic * Overrides `funsub` from [[tip.solvers.MapLatticeSolver]] adding support for function calls and returns. */ override def funsub(n: CfgNode, x: lattice.Element): liftedstatelattice.Element = { - import cfg._ // gives easy access to the functionality in InterproceduralProgramCfg + //import cfg._ // gives easy access to the functionality in InterproceduralProgramCfg import liftedstatelattice._ new NormalizedCalls().assertContainsNode(n.data) @@ -138,7 +134,7 @@ trait InterprocValueAnalysisFunctions[L <: LatticeWithOps] extends MapLiftLattic // return node case CfgStmtNode(_, _, _, ret: AReturnStmt) => val j = join(n, x) - j + (AstOps.returnId -> eval(ret.value, j)) + j + (AstOps.returnId -> eval(ret.exp, j)) // call nodes (like no-ops here) case _: CfgCallNode => join(n, x) @@ -196,7 +192,7 @@ trait InterprocValueAnalysisFunctionsWithPropagation // return statement case CfgStmtNode(_, _, _, ret: AReturnStmt) => - s + (AstOps.returnId -> eval(ret.value, s)) + s + (AstOps.returnId -> eval(ret.exp, s)) // function entry nodes (like no-op here) case _: CfgFunEntryNode => s @@ -259,7 +255,7 @@ abstract class LiftedValueAnalysis[P <: ProgramCfg](val cfg: P)(implicit val dec import liftedstatelattice._ n match { // function entry nodes are always reachable (if intra-procedural analysis) - case funentry: CfgFunEntryNode => lift(statelattice.bottom) + case _: CfgFunEntryNode => lift(statelattice.bottom) // all other nodes are processed with join+transfer case _ => super.funsub(n, x) } @@ -360,7 +356,7 @@ abstract class ContextSensitiveValueAnalysis[C <: CallContext, L <: LatticeWithO // return statement case CfgStmtNode(_, _, _, ret: AReturnStmt) => - s + (AstOps.returnId -> eval(ret.value, s)) + s + (AstOps.returnId -> eval(ret.exp, s)) // function entry nodes (like no-op here) case _: CfgFunEntryNode => s diff --git a/src/tip/ast/Ast.scala b/src/tip/ast/Ast.scala index c7e4264..2527010 100644 --- a/src/tip/ast/Ast.scala +++ b/src/tip/ast/Ast.scala @@ -1,16 +1,14 @@ package tip.ast import tip.ast.AstPrinters._ - -object AstNode { - - var lastUid: Int = 0 -} +import tip.util.TipProgramException /** * Source code location. */ case class Loc(line: Int, col: Int) { override def toString: String = s"$line:$col" + + def toStringLong: String = s"(line $line, column $col)" } sealed trait Operator @@ -41,10 +39,6 @@ case object GreatThan extends Operator with BinaryOperator { override def toString: String = ">" } -case object RefOp extends Operator with UnaryOperator { - override def toString: String = "&" -} - case object DerefOp extends Operator with UnaryOperator { override def toString: String = "*" } @@ -56,19 +50,13 @@ case object DerefOp extends Operator with UnaryOperator { */ sealed abstract class AstNode extends Product { - /** - * Unique ID of the node. - * Every new node object gets a fresh ID (but the ID is ignored in equals tests). - */ - val uid: Int = { AstNode.lastUid += 1; AstNode.lastUid } - /** * Source code location. */ val loc: Loc override def toString: String = - s"${this.print(PartialFunction.empty)}:$loc" + s"${this.print(PartialFunction.empty)}[$loc]" } //////////////// Expressions ////////////////////////// @@ -77,21 +65,19 @@ sealed trait AExprOrIdentifierDeclaration extends AstNode sealed trait AExpr extends AExprOrIdentifierDeclaration -sealed trait Assignable extends AExpr - sealed trait AAtomicExpr extends AExpr sealed trait ADeclaration extends AstNode case class ACallFuncExpr(targetFun: AExpr, args: List[AExpr], loc: Loc) extends AExpr -case class AIdentifierDeclaration(value: String, loc: Loc) extends ADeclaration with AExprOrIdentifierDeclaration +case class AIdentifierDeclaration(name: String, loc: Loc) extends ADeclaration with AExprOrIdentifierDeclaration -case class AIdentifier(value: String, loc: Loc) extends AExpr with AAtomicExpr with Assignable +case class AIdentifier(name: String, loc: Loc) extends AExpr with AAtomicExpr with ReferenceAssignable case class ABinaryOp(operator: BinaryOperator, left: AExpr, right: AExpr, loc: Loc) extends AExpr -case class AUnaryOp(operator: UnaryOperator, target: AExpr, loc: Loc) extends AExpr with Assignable +case class AUnaryOp(operator: UnaryOperator, subexp: AExpr, loc: Loc) extends AExpr case class ANumber(value: Int, loc: Loc) extends AExpr with AAtomicExpr @@ -99,13 +85,15 @@ case class AInput(loc: Loc) extends AExpr with AAtomicExpr case class AAlloc(exp: AExpr, loc: Loc) extends AExpr with AAtomicExpr +case class AVarRef(id: AIdentifier, loc: Loc) extends AExpr with AAtomicExpr + case class ANull(loc: Loc) extends AExpr with AAtomicExpr case class ARecord(fields: List[ARecordField], loc: Loc) extends AExpr case class ARecordField(field: String, exp: AExpr, loc: Loc) -case class AAccess(record: AExpr, field: String, loc: Loc) extends AExpr with AAtomicExpr +case class AFieldAccess(record: AExpr, field: String, loc: Loc) extends AExpr with AAtomicExpr //////////////// Statements ////////////////////////// @@ -118,6 +106,18 @@ sealed trait AStmtInNestedBlock extends AStmt case class AAssignStmt(left: Assignable, right: AExpr, loc: Loc) extends AStmtInNestedBlock +sealed trait Assignable + +sealed trait ReferenceAssignable extends Assignable + +case class ADerefWrite(exp: AExpr, loc: Loc) extends ReferenceAssignable + +sealed trait FieldAssignable extends Assignable + +case class ADirectFieldWrite(id: AIdentifier, field: String, loc: Loc) extends FieldAssignable + +case class AIndirectFieldWrite(exp: AExpr, field: String, loc: Loc) extends FieldAssignable + sealed trait ABlock extends AStmt { /** @@ -139,11 +139,11 @@ case class AFunBlockStmt(declarations: List[AVarStmt], others: List[AStmtInNeste case class AIfStmt(guard: AExpr, ifBranch: AStmtInNestedBlock, elseBranch: Option[AStmtInNestedBlock], loc: Loc) extends AStmtInNestedBlock -case class AOutputStmt(value: AExpr, loc: Loc) extends AStmtInNestedBlock +case class AOutputStmt(exp: AExpr, loc: Loc) extends AStmtInNestedBlock -case class AReturnStmt(value: AExpr, loc: Loc) extends AStmt +case class AReturnStmt(exp: AExpr, loc: Loc) extends AStmt -case class AErrorStmt(value: AExpr, loc: Loc) extends AStmtInNestedBlock +case class AErrorStmt(exp: AExpr, loc: Loc) extends AStmtInNestedBlock case class AVarStmt(declIds: List[AIdentifierDeclaration], loc: Loc) extends AStmt @@ -156,7 +156,7 @@ case class AProgram(funs: List[AFunDeclaration], loc: Loc) extends AstNode { def mainFunction: AFunDeclaration = { val main = findMainFunction() if (main.isDefined) main.get - else throw new RuntimeException(s"Missing main function, declared functions are $funs") + else throw new TipProgramException(s"Missing main function, declared functions are $funs") } def hasMainFunction: Boolean = diff --git a/src/tip/ast/AstNodeData.scala b/src/tip/ast/AstNodeData.scala index e4439d8..2d447b8 100644 --- a/src/tip/ast/AstNodeData.scala +++ b/src/tip/ast/AstNodeData.scala @@ -1,7 +1,7 @@ package tip.ast import tip.ast.AstPrinters._ -import tip.types.TipType +import tip.types.Type object AstNodeData { @@ -15,7 +15,7 @@ object AstNodeData { * Map from AST node to type, if available. * @see [[tip.analysis.TypeAnalysis]] */ - type TypeData = Map[AstNode, Option[TipType]] + type TypeData = Map[AstNode, Option[Type]] /** * Implicitly make declaration data available on identifier AST nodes. @@ -36,12 +36,12 @@ object AstNodeData { * (For information about Scala's implicit classes, see [[tip.ast.AstNodeData.AstNodeWithDeclaration]].) */ implicit class AstNodeWithType(n: AstNode)(implicit val data: TypeData) { - def theType: Option[TipType] = data.getOrElse(n, None) + def theType: Option[Type] = data.getOrElse(n, None) private def printer: PartialFunction[AstNode, String] = { - case id: AIdentifierDeclaration => s"${id.value}: ${id.theType.getOrElse("??")}" + case id: AIdentifierDeclaration => s"${id.name}: ${id.theType.getOrElse("??")}" case f: AFunDeclaration => - s"${f.name}(${f.params.map(_.value).mkString(",")}): ${f.theType.getOrElse("??")}\n${f.stmts.print(printer)}" + s"${f.name}(${f.params.map(_.name).mkString(",")}): ${f.theType.getOrElse("??")}\n${f.stmts.print(printer)}" } def toTypedString: String = n.print(printer) diff --git a/src/tip/ast/AstOps.scala b/src/tip/ast/AstOps.scala index 154053a..fc79f78 100644 --- a/src/tip/ast/AstOps.scala +++ b/src/tip/ast/AstOps.scala @@ -26,15 +26,15 @@ object AstOps { */ def containsInvocation: Boolean = { var found = false - val invocationFinder = new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = + val invocationFinder = new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = node match { case _: ACallFuncExpr => found = true - case _ => visitChildren(node, null) + case _ => visitChildren(node, ()) } } - invocationFinder.visit(n, null) + invocationFinder.visit(n, ()) found } @@ -52,8 +52,8 @@ object AstOps { */ def appearingIds(implicit declData: DeclarationData): Set[ADeclaration] = { val ids = mutable.Set[ADeclaration]() - val idFinder = new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = { + val idFinder = new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = { node match { case id: AIdentifier => id.declaration match { @@ -64,10 +64,10 @@ object AstOps { case fun: AFunDeclaration => ids += fun case _ => } - visitChildren(node, null) + visitChildren(node, ()) } } - idFinder.visit(n, null) + idFinder.visit(n, ()) ids.toSet } @@ -76,14 +76,14 @@ object AstOps { */ def appearingAllocs: Set[AAlloc] = { val allocs = mutable.Set[AAlloc]() - val allocsFinder = new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = + val allocsFinder = new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = node match { case alloc: AAlloc => allocs += alloc - case _ => visitChildren(node, null) + case _ => visitChildren(node, ()) } } - allocsFinder.visit(n, null) + allocsFinder.visit(n, ()) allocs.toSet } @@ -92,14 +92,14 @@ object AstOps { */ def appearingConstants: Set[ANumber] = { val numbers = mutable.Set[ANumber]() - val numFinder = new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = + val numFinder = new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = node match { case num: ANumber => numbers += num - case _ => visitChildren(node, null) + case _ => visitChildren(node, ()) } } - numFinder.visit(n, null) + numFinder.visit(n, ()) numbers.toSet } @@ -108,37 +108,58 @@ object AstOps { */ def appearingExpressions: Set[AExpr] = { val exps = mutable.Set[AExpr]() - val expFinder = new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = + val expFinder = new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = node match { case exp: ABinaryOp => exps += exp - visitChildren(exp, null) - case _ => visitChildren(node, null) + visitChildren(exp, ()) + case _ => visitChildren(node, ()) } } - expFinder.visit(n, null) + expFinder.visit(n, ()) exps.toSet } + /** + * Returns the set of non-'input' expressions appearing in the subtree of the node. + */ + def appearingNonInputExpressions: Set[AExpr] = + appearingExpressions.filterNot(e => e.containsInput) + + /** + * Checks whether the subtree of the node contains an 'input' expression. + */ + def containsInput: Boolean = { + var res = false; + new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = + node match { + case _: AInput => res = true; + case _ => visitChildren(node, ()) + } + }.visit(n, ()) + res + } + /** * Returns the set of record field names appearing in the subtree of the node. */ def appearingFields: Set[String] = { val fields = mutable.Set[String]() - val expFinder = new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = + val expFinder = new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = node match { - case exp: AAccess => + case exp: AFieldAccess => fields += exp.field - visitChildren(exp, null) + visitChildren(exp, ()) case rec: ARecord => fields ++= rec.fields.map { _.field } - visitChildren(rec, null) - case _ => visitChildren(node, null) + visitChildren(rec, ()) + case _ => visitChildren(node, ()) } } - expFinder.visit(n, null) + expFinder.visit(n, ()) fields.toSet } } diff --git a/src/tip/ast/AstPrinters.scala b/src/tip/ast/AstPrinters.scala index 0364d46..1dd2eb2 100644 --- a/src/tip/ast/AstPrinters.scala +++ b/src/tip/ast/AstPrinters.scala @@ -27,8 +27,8 @@ object AstPrinters { n match { case ACallFuncExpr(targetFun, args, _) => s"${targetFun.print(printer)}(${args.map(_.print(printer)).mkString(",")})" - case AIdentifier(value, _) => - value + case AIdentifier(name, _) => + name case ABinaryOp(operator, left, right, _) => s"(${left.print(printer)} $operator ${right.print(printer)})" case AUnaryOp(operator, target, _) => @@ -39,33 +39,45 @@ object AstPrinters { "input" case AAlloc(e, _) => s"alloc ${e.print(printer)}" + case AVarRef(id, _) => + s"&${id.print(printer)}" case ARecord(fields, _) => fields.map { f => s"${f.field}:${f.exp.print(printer)}" }.mkString("{", ",", "}") - case AAccess(record, field, _) => + case AFieldAccess(record, field, _) => s"${record.print(printer)}.$field" case ANull(_) => "null" - case AIdentifierDeclaration(value, _) => - value + case AIdentifierDeclaration(name, _) => + name case AFunDeclaration(name, args, stmts, _) => s"$name(${args.map(_.print(printer)).mkString(",")})\n${stmts.print(printer)}" case AAssignStmt(left, right, _) => - s"${left.print(printer)} = ${right.print(printer)};" + val ls = left match { + case AIdentifier(name, _) => + name + case ADerefWrite(exp, _) => + s"*${exp.print(printer)}" + case ADirectFieldWrite(id, field, _) => + s"${id.print(printer)}.$field" + case AIndirectFieldWrite(exp, field, _) => + s"(*${exp.print(printer)}).$field" + } + s"$ls = ${right.print(printer)};" case AIfStmt(guard, ifBranch, elseBranch, _) => val elseb = elseBranch.map(x => "else " + x.print(printer)).getOrElse("") s"if (${guard.print(printer)}) ${ifBranch.print(printer)} $elseb" - case AOutputStmt(value, _) => - s"output ${value.print(printer)};" - case AErrorStmt(value, _) => - s"error ${value.print(printer)};" + case AOutputStmt(exp, _) => + s"output ${exp.print(printer)};" + case AErrorStmt(exp, _) => + s"error ${exp.print(printer)};" case AWhileStmt(guard, innerBlock, _) => s"while (${guard.print(printer)}) ${innerBlock.print(printer)}" case block: ABlock => s"{\n${block.body.map(_.print(printer)).mkString("\n")}\n}" - case AReturnStmt(value, _) => - s"return ${value.print(printer)};" + case AReturnStmt(exp, _) => + s"return ${exp.print(printer)};" case AVarStmt(declIds, _) => s"var ${declIds.map(_.print(printer)).mkString(",")};" case AProgram(funs, _) => diff --git a/src/tip/ast/DepthFirstAstVisitor.scala b/src/tip/ast/DepthFirstAstVisitor.scala index a3f034f..2a2e60a 100644 --- a/src/tip/ast/DepthFirstAstVisitor.scala +++ b/src/tip/ast/DepthFirstAstVisitor.scala @@ -23,10 +23,19 @@ trait DepthFirstAstVisitor[A] { visit(bin.left, arg) visit(bin.right, arg) case un: AUnaryOp => - visit(un.target, arg) - case ass: AAssignStmt => - visit(ass.right, arg) - visit(ass.left, arg) + visit(un.subexp, arg) + case as: AAssignStmt => + as.left match { + case id: AIdentifier => + visit(id, arg) + case dw: ADerefWrite => + visit(dw.exp, arg) + case dfw: ADirectFieldWrite => + visit(dfw.id, arg) + case ifw: AIndirectFieldWrite => + visit(ifw.exp, arg) + } + visit(as.right, arg) case block: ABlock => block.body.foreach(visit(_, arg)) case iff: AIfStmt => @@ -34,11 +43,11 @@ trait DepthFirstAstVisitor[A] { visit(iff.ifBranch, arg) iff.elseBranch.foreach(visit(_, arg)) case out: AOutputStmt => - visit(out.value, arg) + visit(out.exp, arg) case ret: AReturnStmt => - visit(ret.value, arg) + visit(ret.exp, arg) case err: AErrorStmt => - visit(err.value, arg) + visit(err.exp, arg) case varr: AVarStmt => varr.declIds.foreach(visit(_, arg)) case whl: AWhileStmt => @@ -49,14 +58,14 @@ trait DepthFirstAstVisitor[A] { visit(funDec.stmts, arg) case p: AProgram => p.funs.foreach(visit(_, arg)) - case acc: AAccess => + case acc: AFieldAccess => visit(acc.record, arg) case rec: ARecord => - rec.fields.foreach { f => - visit(f.exp, arg) - } + rec.fields.foreach(f => visit(f.exp, arg)) case alloc: AAlloc => visit(alloc.exp, arg) + case ref: AVarRef => + visit(ref.id, arg) case _: AAtomicExpr | _: AIdentifierDeclaration => } } diff --git a/src/tip/ast/TipNormalizers.scala b/src/tip/ast/TipNormalizers.scala index f68fd7d..a03e671 100644 --- a/src/tip/ast/TipNormalizers.scala +++ b/src/tip/ast/TipNormalizers.scala @@ -32,10 +32,11 @@ class Normalizer { */ def normalizeExpr(e: AExpr): AExpr = e match { - case a: Assignable => normalizeAssignable(a) + case _: AIdentifier => e + case uop: AUnaryOp => uop.copy(subexp = normalizeExpr(uop.subexp)) + case bop: ABinaryOp => bop.copy(left = normalizeExpr(bop.left), right = normalizeExpr(bop.right)) case r: ARecord => r.copy(fields = r.fields.map(normalizeRecordField)) case call: ACallFuncExpr => call.copy(targetFun = normalizeExpr(call.targetFun), args = call.args.map(normalizeExpr)) - case op: ABinaryOp => op.copy(left = normalizeExpr(op.left), right = normalizeExpr(op.right)) case _ => e } @@ -64,8 +65,9 @@ class Normalizer { */ def normalizeAssignable(e: Assignable): Assignable = e match { - case _: AIdentifier => e - case uop: AUnaryOp => uop.copy(target = normalizeExpr(uop.target)) + case _: AIdentifier | _: ADirectFieldWrite => e + case dw: ADerefWrite => dw.copy(exp = normalizeExpr(dw.exp)) + case ifw: AIndirectFieldWrite => ifw.copy(exp = normalizeExpr(ifw.exp)) } /** @@ -93,9 +95,9 @@ class Normalizer { val elseBranch2 = stmt.elseBranch.map(normalizeStmtInNestedBlock) nestedBlock(stmt.copy(guard = normalizeExpr(stmt.guard), ifBranch = ifBranch2, elseBranch = elseBranch2)) case stmt: AOutputStmt => - nestedBlock(stmt.copy(value = normalizeExpr(stmt.value))) + nestedBlock(stmt.copy(exp = normalizeExpr(stmt.exp))) case stmt: AErrorStmt => - nestedBlock(stmt.copy(value = normalizeExpr(stmt.value))) + nestedBlock(stmt.copy(exp = normalizeExpr(stmt.exp))) case stmt: AWhileStmt => val innerBlock2 = normalizeStmtInNestedBlock(stmt.innerBlock) nestedBlock(stmt.copy(guard = normalizeExpr(stmt.guard), innerBlock = innerBlock2)) @@ -105,7 +107,7 @@ class Normalizer { * Normalizes an AReturnStmt. */ def normalizeReturnStmt(ret: AReturnStmt): AReturnStmt = - ret.copy(value = normalizeExpr(ret.value)) + ret.copy(exp = normalizeExpr(ret.exp)) /** * Normalizes an AFunBlockStmt. @@ -167,7 +169,7 @@ object NoNormalizer extends Normalizer { object ReturnsNormalizer extends Normalizer { override def normalizeReturnStmt(ret: AReturnStmt): AReturnStmt = // [[return e]] becomes [[return id]] - ret.copy(value = normalizeToIdentifier(ret.value)) + ret.copy(exp = normalizeToIdentifier(ret.exp)) } /** @@ -211,18 +213,32 @@ object CallsNormalizer extends Normalizer { object PointersNormalizer extends Normalizer { /** - * Normalizes the left-hand side of an assignment so that it has the form id or *id. + * Normalizes the left-hand side of an assignment so that it has the form id, *id, id.id, or (*id).id. */ def normalizeLeft(left: Assignable): Assignable = left match { - case _: AIdentifier => left - case AUnaryOp(_, _: AIdentifier, _) => left - case AUnaryOp(op, target, loc) => - val tmpVar = newVariable() - val id = AIdentifier(tmpVar, left.loc) - addDeclaration(AIdentifierDeclaration(tmpVar, left.loc)) - addStatement(normalizeStmtInNestedBlock(AAssignStmt(id, target, left.loc))) - AUnaryOp(op, id, left.loc) + case AIdentifier(_, _) => left + case ADerefWrite(exp, loc) => + exp match { + case AIdentifier(_, _) => left + case _ => + val tmpVar = newVariable() + val id = AIdentifier(tmpVar, loc) + addDeclaration(AIdentifierDeclaration(tmpVar, loc)) + addStatement(normalizeStmtInNestedBlock(AAssignStmt(id, exp, loc))) + ADerefWrite(id, loc) + } + case ADirectFieldWrite(_, _, _) => left + case AIndirectFieldWrite(exp, field, loc) => + exp match { + case AIdentifier(_, _) => left + case _ => + val tmpVar = newVariable() + val id = AIdentifier(tmpVar, loc) + addDeclaration(AIdentifierDeclaration(tmpVar, loc)) + addStatement(normalizeStmtInNestedBlock(AAssignStmt(id, exp, loc))) + AIndirectFieldWrite(id, field, loc) + } } /** @@ -231,7 +247,7 @@ object PointersNormalizer extends Normalizer { def normalizeRight(right: AExpr): AExpr = right match { case op: AUnaryOp => - op.copy(target = normalizeToIdentifier(op.target)) + op.copy(subexp = normalizeToIdentifier(op.subexp)) case _: AIdentifier => right case _: ANull => right case _: AAlloc => right diff --git a/src/tip/ast/TipSublanguages.scala b/src/tip/ast/TipSublanguages.scala index 0bb6408..dd255b5 100644 --- a/src/tip/ast/TipSublanguages.scala +++ b/src/tip/ast/TipSublanguages.scala @@ -2,26 +2,27 @@ package tip.ast import tip.ast.AstNodeData.DeclarationData import AstNodeData._ +import tip.util.TipProgramException /** * Defines restrictions of TIP for the different analyses. */ -trait TipSublanguages extends DepthFirstAstVisitor[Any] { +trait TipSublanguages extends DepthFirstAstVisitor[Unit] { /** * Throws an exception if `prog` is not in the sub-language. */ def assertContainsProgram(prog: AProgram): Unit = - visit(prog, null) + visit(prog, ()) /** * Throws an exception if the AST node `n` is not in the sub-language. */ def assertContainsNode(n: AstNode): Unit = - visit(n, null) + visit(n, ()) - def LanguageRestrictionViolation(message: String): Nothing = - throw new IllegalArgumentException(s"The TIP program is required to be in the ${this.getClass} sub-language\n $message") + def LanguageRestrictionViolation(message: String, loc: Loc): Nothing = + throw new TipProgramException(s"The analysis requires the program to be in the ${this.getClass} sub-language\n $message ${loc.toStringLong}") } /** @@ -29,21 +30,21 @@ trait TipSublanguages extends DepthFirstAstVisitor[Any] { */ class NoFunctionPointers(implicit declData: DeclarationData) extends TipSublanguages { - def visit(ast: AstNode, x: Any): Unit = + def visit(ast: AstNode, x: Unit): Unit = ast match { case ACallFuncExpr(targetFun: AIdentifier, args, _) => targetFun.declaration match { case _: AFunDeclaration => case _ => - LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function") + LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function", ast.loc) } args.foreach(visit(_, x)) case ACallFuncExpr(targetFun, args, _) => - LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function") + LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function", ast.loc) case id: AIdentifier => id.declaration match { case _: AFunDeclaration => - LanguageRestrictionViolation(s"Identifier $id is a function identifier not appearing in a direct call expression") + LanguageRestrictionViolation(s"Identifier $id is a function identifier not appearing in a direct call expression", ast.loc) case _ => } case _ => visitChildren(ast, x) @@ -62,21 +63,21 @@ class NoFunctionPointers(implicit declData: DeclarationData) extends TipSublangu */ object NormalizedForPointsToAnalysis extends TipSublanguages { - def visit(ast: AstNode, x: Any): Unit = { + def visit(ast: AstNode, x: Unit): Unit = { ast match { case AAssignStmt(_: AIdentifier, AAlloc(ANull(_) | ANumber(_, _), _), _) => - case AAssignStmt(_: AIdentifier, AUnaryOp(RefOp, _: AIdentifier, _), _) => + case AAssignStmt(_: AIdentifier, AVarRef(_, _), _) => case AAssignStmt(_: AIdentifier, _: AIdentifier, _) => case AAssignStmt(_: AIdentifier, AUnaryOp(DerefOp, _: AIdentifier, _), _) => - case AAssignStmt(AUnaryOp(_, _: AIdentifier, _), _: AIdentifier, _) => + case AAssignStmt(ADerefWrite(_: AIdentifier, _), _: AIdentifier, _) => case AAssignStmt(_: AIdentifier, _: ANull, _) => case AAssignStmt(_: AIdentifier, _: AAtomicExpr, _) => case _: ABlock => case _: AVarStmt => case _: AReturnStmt => case _: AIfStmt => - case x: AStmt => - LanguageRestrictionViolation(s"Statement $x is not allowed") + case stmt: AStmt => + LanguageRestrictionViolation(s"Statement $stmt is not allowed", ast.loc) case _ => } visitChildren(ast, x) @@ -88,12 +89,20 @@ object NormalizedForPointsToAnalysis extends TipSublanguages { */ object NoPointers extends TipSublanguages { - def visit(ast: AstNode, x: Any): Unit = { + def visit(ast: AstNode, x: Unit): Unit = { ast match { - case AUnaryOp(deref: DerefOp.type, _, _) => - LanguageRestrictionViolation(s"Pointer operation $deref is not allowed") - case AUnaryOp(ref: RefOp.type, _, _) => - LanguageRestrictionViolation(s"Pointer operation $ref is not allowed") + case AUnaryOp(_: DerefOp.type, _, _) => + LanguageRestrictionViolation(s"Pointer load operation is not allowed", ast.loc) + case AVarRef(_, _) => + LanguageRestrictionViolation(s"Pointer reference operation is not allowed", ast.loc) + case as: AAssignStmt => + as.left match { + case _: ADerefWrite => + LanguageRestrictionViolation(s"Pointer store operation is not allowed", ast.loc) + case _: AIndirectFieldWrite => + LanguageRestrictionViolation(s"Pointer field store operation is not allowed", ast.loc) + case _ => + } case _ => } visitChildren(ast, x) @@ -105,10 +114,10 @@ object NoPointers extends TipSublanguages { */ object NoCalls extends TipSublanguages { - def visit(ast: AstNode, x: Any): Unit = { + def visit(ast: AstNode, x: Unit): Unit = { ast match { case call: ACallFuncExpr => - LanguageRestrictionViolation(s"Call $call is not allowed") + LanguageRestrictionViolation(s"Call $call is not allowed", ast.loc) case _ => } visitChildren(ast, x) @@ -125,19 +134,19 @@ object NoCalls extends TipSublanguages { */ class NormalizedCalls(implicit declData: DeclarationData) extends TipSublanguages { - def visit(ast: AstNode, x: Any): Unit = + def visit(ast: AstNode, x: Unit): Unit = ast match { case AAssignStmt(_: AIdentifier, ACallFuncExpr(targetFun: AIdentifier, args, _), _) => targetFun.declaration match { case _: AFunDeclaration => case _ => - LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function") + LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function", ast.loc) } if (args.exists(!_.isInstanceOf[AAtomicExpr])) - LanguageRestrictionViolation(s"One of the arguments $args is not atomic") + LanguageRestrictionViolation(s"One of the arguments $args is not atomic", ast.loc) case AAssignStmt(_: AIdentifier, ACallFuncExpr(targetFun, args, _), _) => - LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function") - case call: ACallFuncExpr => LanguageRestrictionViolation(s"Call $call outside an assignment is not allowed") + LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function", ast.loc) + case call: ACallFuncExpr => LanguageRestrictionViolation(s"Call $call outside an assignment is not allowed", ast.loc) case _ => visitChildren(ast, x) } } @@ -146,12 +155,21 @@ class NormalizedCalls(implicit declData: DeclarationData) extends TipSublanguage * This sub-language has no records and record accesses. */ object NoRecords extends TipSublanguages { - def visit(ast: AstNode, x: Any): Unit = { + + def visit(ast: AstNode, x: Unit): Unit = { ast match { case _: ARecord => - LanguageRestrictionViolation(s"Using records at: ${ast.loc}") - case _: AAccess => - LanguageRestrictionViolation(s"Record access at: ${ast.loc}") + LanguageRestrictionViolation(s"Record is not allowed", ast.loc) + case _: AFieldAccess => + LanguageRestrictionViolation(s"Field read is not allowed", ast.loc) + case as: AAssignStmt => + as.left match { + case _: ADirectFieldWrite => + LanguageRestrictionViolation(s"Field write operation is not allowed", ast.loc) + case _: AIndirectFieldWrite => + LanguageRestrictionViolation(s"Pointer field store operation is not allowed", ast.loc) + case _ => + } case _ => } visitChildren(ast, x) diff --git a/src/tip/cfg/CfgOps.scala b/src/tip/cfg/CfgOps.scala index 429371a..8056232 100644 --- a/src/tip/cfg/CfgOps.scala +++ b/src/tip/cfg/CfgOps.scala @@ -48,10 +48,10 @@ object CfgOps { /** * Returns the set of expressions that appear in the node. */ - def appearingExpressions: Set[AExpr] = + def appearingNonInputExpressions: Set[AExpr] = n match { case r: CfgStmtNode => - r.data.appearingExpressions + r.data.appearingNonInputExpressions case _ => Set() } @@ -62,7 +62,7 @@ object CfgOps { n match { case r: CfgStmtNode => r.data match { - case ass: AAssignStmt => Some(ass) + case as: AAssignStmt => Some(as) case _ => None } case _ => None diff --git a/src/tip/cfg/InterproceduralProgramCfg.scala b/src/tip/cfg/InterproceduralProgramCfg.scala index 84257ef..1be637f 100644 --- a/src/tip/cfg/InterproceduralProgramCfg.scala +++ b/src/tip/cfg/InterproceduralProgramCfg.scala @@ -4,6 +4,7 @@ import tip.analysis.ControlFlowAnalysis import tip.ast.AstNodeData._ import tip.ast._ import tip.util.MapUtils._ +import tip.util.TipProgramException object InterproceduralProgramCfg { @@ -26,19 +27,19 @@ object InterproceduralProgramCfg { case i: AIfStmt => assert(!i.guard.containsInvocation) FragmentCfg.nodeToGraph(CfgStmtNode(data = i.guard)) - case ass: AAssignStmt => - ass.right match { + case as: AAssignStmt => + as.right match { case call: ACallFuncExpr => assert( !call.targetFun.containsInvocation && call.args.forall(!_.containsInvocation) ) - val cnode = CfgCallNode(data = ass) - val retnode = CfgAfterCallNode(data = ass) + val cnode = CfgCallNode(data = as) + val retnode = CfgAfterCallNode(data = as) FragmentCfg.nodeToGraph(cnode) ~ FragmentCfg.nodeToGraph(retnode) case _ => - assert(!ass.containsInvocation) - FragmentCfg.nodeToGraph(CfgStmtNode(data = ass)) + assert(!as.containsInvocation) + FragmentCfg.nodeToGraph(CfgStmtNode(data = as)) } case _ => assert(!normal.data.containsInvocation) @@ -52,9 +53,9 @@ object InterproceduralProgramCfg { case ACallFuncExpr(target: AIdentifier, _, loc) => declData(target) match { case d: AFunDeclaration => Set(d) - case _ => new NoFunctionPointers().LanguageRestrictionViolation(s"$target is not a function identifier at $loc") + case _ => new NoFunctionPointers().LanguageRestrictionViolation(s"$target is not a function identifier", loc) } - case ACallFuncExpr(target, _, loc) => new NoFunctionPointers().LanguageRestrictionViolation(s"Indirect call to $target not supported at $loc") + case ACallFuncExpr(target, _, loc) => new NoFunctionPointers().LanguageRestrictionViolation(s"Indirect call to $target not supported", loc) case _ => Set[AFunDeclaration]() } } @@ -84,21 +85,18 @@ object InterproceduralProgramCfg { val allEntries = funGraphs.mapValues(cfg => { assert(cfg.graphEntries.size == 1); cfg.graphEntries.head.asInstanceOf[CfgFunEntryNode] }) val allExits = funGraphs.mapValues(cfg => { assert(cfg.graphExits.size == 1); cfg.graphExits.head.asInstanceOf[CfgFunExitNode] }) - // ensure that there are no function pointers - new NormalizedCalls().assertContainsProgram(prog) - val cfaSolution = new ControlFlowAnalysis(prog).analyze() var callInfo: Map[AAssignStmt, Set[AFunDeclaration]] = Map() // Using result of CFA to build callInfo - new DepthFirstAstVisitor[Null] { - override def visit(node: AstNode, arg: Null): Unit = + new DepthFirstAstVisitor[Unit] { + override def visit(node: AstNode, arg: Unit): Unit = node match { - case a @ AAssignStmt(_, c @ ACallFuncExpr(id: AIdentifier, _, _), _) => + case a @ AAssignStmt(_, ACallFuncExpr(id: AIdentifier, _, _), _) => callInfo += a -> cfaSolution(id.declaration) case _ => visitChildren(node, arg) } - }.visit(prog, null) + }.visit(prog, ()) new InterproceduralProgramCfg(allEntries, allExits, prog, callInfo) } @@ -258,18 +256,18 @@ class InterproceduralProgramCfg( def targetIdentifier: AIdentifier = nd.data match { case AAssignStmt(id: AIdentifier, _, _) => id - case _ => throw new IllegalArgumentException("Expected left-hand-side of call assignment to be an identifier") + case _ => throw new TipProgramException("Expected left-hand-side of call assignment to be an identifier") } def assignment: AAssignStmt = nd.data match { - case ass: AAssignStmt => ass + case as: AAssignStmt => as } def invocation: ACallFuncExpr = this.assignment.right match { case call: ACallFuncExpr => call - case _ => throw new IllegalArgumentException("Expected right-hand-side of call assignment to be a call") + case _ => throw new TipProgramException("Expected right-hand-side of call assignment to be a call") } } @@ -278,18 +276,18 @@ class InterproceduralProgramCfg( def targetIdentifier: AIdentifier = nd.data match { case AAssignStmt(id: AIdentifier, _, _) => id - case _ => throw new IllegalArgumentException("Expected left-hand-side of call assignment to be an identifier") + case _ => throw new TipProgramException("Expected left-hand-side of call assignment to be an identifier") } def assignment: AAssignStmt = nd.data match { - case ass: AAssignStmt => ass + case as: AAssignStmt => as } def invocation: ACallFuncExpr = this.assignment.right match { case call: ACallFuncExpr => call - case _ => throw new IllegalArgumentException("Expected right-hand-side of call assignment to be a call") + case _ => throw new TipProgramException("Expected right-hand-side of call assignment to be a call") } } } diff --git a/src/tip/concolic/ConcolicEngine.scala b/src/tip/concolic/ConcolicEngine.scala index c376fc3..7c63f05 100644 --- a/src/tip/concolic/ConcolicEngine.scala +++ b/src/tip/concolic/ConcolicEngine.scala @@ -35,12 +35,12 @@ class ConcolicEngine(val program: AProgram)(implicit declData: DeclarationData) log.info(s"SMT script for next run: \n$smt") SMTSolver.solve(smt) match { case None => - log.info(s"Path condition is unsatisfiable.") + log.info(s"Path condition is unsatisfiable") targetNode.unsat(value) newInputs(symbols, lastNode, root) case Some(mapping) => log.info(s"Model: $mapping") - Some(symbols.map(v => mapping.get(v.value).map(_.toInt).getOrElse(scala.util.Random.nextInt))) + Some(symbols.map(v => mapping.get(v.name).map(_.toInt).getOrElse(scala.util.Random.nextInt))) } case _ => None } @@ -70,7 +70,7 @@ class ConcolicEngine(val program: AProgram)(implicit declData: DeclarationData) } catch { case err: ExecutionError => log.info(s"Error found: $err") - ExFailure(err.store.extra, err.message) + ExFailure(err.store.extra, err.getMessage) } results = result :: results @@ -79,22 +79,22 @@ class ConcolicEngine(val program: AProgram)(implicit declData: DeclarationData) log.info(s"New input for ${result.symbolicVars}: $values") inputs = values case None => - log.info(s"Finished exhaustive exploration in $runs runs.\n") + log.info(s"Finished exhaustive exploration in $runs runs") reportExplorationStatistics(results) return } } - log.info(s"Exhausted search budget after $runs runs.\n") + log.info(s"Exhausted search budget after $runs runs") reportExplorationStatistics(results) } private def reportExplorationStatistics(results: List[ExecutionResult]): Unit = { val successes = results.collect { case s: ExSuccess => s } - log.info(s"Found ${successes.length} successful input sequences.") + log.info(s"Found ${successes.length} successful input sequences") successes.foreach(s => log.info(s"Input sequence ${s.usedInputs} produces: \n${s.value}")) val failures = results.collect { case f: ExFailure => f } log.info(s"Found ${failures.length} failure-inducing input sequences.") - failures.foreach(f => log.info(s"Input sequence ${f.usedInputs} fails with: \n${f.message}.")) + failures.foreach(f => log.info(s"Input sequence ${f.usedInputs} fails: \n${f.message}.")) } abstract class ExecutionResult(val concolicState: ConcolicState) { diff --git a/src/tip/concolic/ExecutionTree.scala b/src/tip/concolic/ExecutionTree.scala index 5a3714c..832bb44 100644 --- a/src/tip/concolic/ExecutionTree.scala +++ b/src/tip/concolic/ExecutionTree.scala @@ -52,7 +52,6 @@ class ExecutionTreeRoot() extends ExecutionTree { log.info(s"Exploring ${if (node.count(value) == 0) "unseen " else ""}$value branch") node.count(value) += 1 node.branches(value) - } } @@ -120,7 +119,6 @@ class Branch( case _ => ??? // Impossible: previously satisfiable branch becomes unsatisfiable } - } object ExecutionTreePrinter { @@ -171,5 +169,4 @@ object ExecutionTreePrinter { printTree(treeNode.children.last, sb, root = true) sb.toString } - } diff --git a/src/tip/concolic/SMTSolver.scala b/src/tip/concolic/SMTSolver.scala index 8988243..adaec95 100644 --- a/src/tip/concolic/SMTSolver.scala +++ b/src/tip/concolic/SMTSolver.scala @@ -2,6 +2,7 @@ package tip.concolic import tip.ast._ import smtlib.Interpreter +import smtlib.interpreters.Z3Interpreter import smtlib.parser.Parser import smtlib.parser.Commands._ import smtlib.parser.CommandsResponses._ @@ -13,7 +14,7 @@ object SMTSolver { val log = Log.logger[this.type]() /** - * Expressions extended with symbols + * Expressions extended with symbols. */ class Symbol(location: Loc, counter: Int) extends AIdentifier(s"s$counter", location) { override def toString: String = s"s$counter" @@ -31,12 +32,12 @@ object SMTSolver { case ABinaryOp(op, left, right, _) => s"(${opToSexp(op)} ${expToSexp(left)} ${expToSexp(right)})" case n: ANumber => n.value.toString - case n: Symbol => n.value.toString + case n: Symbol => n.name.toString case _ => exp.toString } def symbolsToSMT(vars: List[Symbol]): String = - vars.map(sv => s"(declare-const ${sv.value} Int)").mkString("\n") + vars.map(sv => s"(declare-const ${sv.name} Int)").mkString("\n") path.foldLeft(symbolsToSMT(vars))((script: String, cond: (AExpr, Boolean)) => { val branchrecord = @@ -95,7 +96,7 @@ object SMTSolver { } } - implicit lazy val z3 = smtlib.interpreters.Z3Interpreter.buildDefault + implicit lazy val z3: Z3Interpreter = smtlib.interpreters.Z3Interpreter.buildDefault /** Solves a SMTLib script */ def solve(script: Script): Option[Map[String, BigInt]] = { @@ -112,9 +113,7 @@ object SMTSolver { solve(Parser.fromString(s).parseScript) /** - * Reset the status of the solver. If not called, previous constraints still - * hold. + * Reset the status of the solver. If not called, previous constraints still hold. */ def reset(): Unit = z3.eval(Reset()) - } diff --git a/src/tip/interpreter/ConcreteValues.scala b/src/tip/interpreter/ConcreteValues.scala index 71301d9..98c9caf 100644 --- a/src/tip/interpreter/ConcreteValues.scala +++ b/src/tip/interpreter/ConcreteValues.scala @@ -25,6 +25,11 @@ object ConcreteValues extends ValueSpecification { */ case class ConcreteReferenceValue(i: Int) extends ReferenceValue + /** + * Reference to field. + */ + case class ConcreteReferenceFieldValue(i: Int, field: String) extends ReferenceValue + /** * Function value. */ diff --git a/src/tip/interpreter/Interpreter.scala b/src/tip/interpreter/Interpreter.scala index 8539102..1e798a6 100644 --- a/src/tip/interpreter/Interpreter.scala +++ b/src/tip/interpreter/Interpreter.scala @@ -2,7 +2,7 @@ package tip.interpreter import tip.ast.AstNodeData._ import tip.ast._ -import tip.util.Log +import tip.util.{Log, TipProgramException} import scala.util.{Failure, Success, Try} @@ -60,7 +60,7 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData } // Store the input in the associated argument locations val storeWithInputArgs = program.mainFunction.params.foldLeft(boundStore) { (s: Store, id: AIdentifierDeclaration) => - val (v, s2) = input(AIdentifier(id.value, id.loc), boundEnv, s) + val (v, s2) = input(AIdentifier(id.name, id.loc), boundEnv, s) s2 + (envWithInputArgs(id) -> v) } // Execute the main function @@ -71,7 +71,7 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData output(x) (x, cs) case _ => - errorReturnNotInt(program.mainFunction, cs) + errorReturnNotInt(program.mainFunction.stmts.ret.exp.loc, program.mainFunction, cs) } } @@ -123,7 +123,17 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData */ protected def semc(stm: AStmt, env: Env, store: Store): (Env, Store) = stm match { - case AAssignStmt(left, right: AExpr, _) => + case AAssignStmt(left: FieldAssignable, right: AExpr, _) => + val (lv, field, s1) = semeref(left, env, store) + store.getOrElse(lv, errorUninitializedLocation(stm.loc, s1)) match { + case rec: RecordValue => + val (rv, s2) = semeright(right, env, s1) + if (rv.isInstanceOf[RecordValue]) errorWriteFieldRecord(stm.loc, rv, s2) + (env, s2 + (lv -> mkRecord(rec.fields + (field -> rv)))) + case _ => + errorAccessNonRecord(stm.loc, lv, s1) + } + case AAssignStmt(left: ReferenceAssignable, right: AExpr, _) => val (lv, s1) = semeref(left, env, store) val (rv, s2) = semeright(right, env, s1) (env, s2 + (lv -> rv)) @@ -141,13 +151,13 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData case _ => errorConditionNotInt(loc, s1) } case ret: AReturnStmt => - val (v, s1) = semeright(ret.value, env, store) + val (v, s1) = semeright(ret.exp, env, store) (env, s1 + (returnLoc -> v)) case err: AErrorStmt => - val (ev, s1) = semeright(err.value, env, store) + val (ev, s1) = semeright(err.exp, env, store) ev match { - case i: IntValue => throw ExecutionError(s"Execution error, code: ${i.i}", s1) - case _ => errorErrorNonInt(ev, store) + case i: IntValue => throw new ExecutionError(s"Execution error, code: ${i.i}", s1) + case _ => errorErrorNonInt(stm.loc, ev, store) } case w: AWhileStmt => val (gv, s1) = semeright(w.guard, env, store) @@ -161,8 +171,8 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData semc(w, env1, s3) case _ => errorConditionNotInt(w.loc, s1) } - case AOutputStmt(value, _) => - val (ov, s1) = semeright(value, env, store) + case AOutputStmt(exp, _) => + val (ov, s1) = semeright(exp, env, store) ov match { case y: IntValue => output(y) @@ -170,7 +180,7 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData case y: ReferenceValue => output(y) (env, s1) - case _ => errorOutputNotInt(s1) + case _ => errorOutputNotInt(exp.loc, s1) } case AVarStmt(ids, _) => (ids.foldLeft(env) { (accenv, id) => @@ -179,27 +189,47 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData } /** - * Semantics for left-hand-side expressions. + * Semantics for ordinary lvalue expressions. * - * @param exp the expression to execute + * @param exp the lvalue expression to execute * @param env the environment * @param store the initial store * @return the resulting location and store */ - protected def semeref(exp: AExpr, env: Env, store: Store): (ReferenceValue, Store) = + protected def semeref(exp: ReferenceAssignable, env: Env, store: Store): (ReferenceValue, Store) = exp match { case id: AIdentifier => (env(id.declaration), store) - case AUnaryOp(_: DerefOp.type, target, loc) => - semeright(target, env, store) match { + case ADerefWrite(subexp, loc) => + semeright(subexp, env, store) match { case (pref: ReferenceValue, s1) => (pref, s1) case (_: NullValue, s1) => errorNullDereference(loc, s1) - case (x, s1) => errorDerefNotPointer(loc, target, x, s1) + case (x, s1) => errorDerefNotPointer(loc, x, s1) } case _ => ??? } + /** + * Semantics for field lvalue expressions. + * + * @param exp the lvalue expression to execute + * @param env the environment + * @param store the initial store + * @return the resulting location, field, and store + */ + protected def semeref(exp: FieldAssignable, env: Env, store: Store): (ReferenceValue, String, Store) = + exp match { + case ADirectFieldWrite(id, field, _) => (env(id.declaration), field, store) + case AIndirectFieldWrite(fexp, field, loc) => + semeright(fexp, env, store) match { + case (pref: ReferenceValue, s1) => (pref, field, s1) + case (_: NullValue, s1) => errorNullDereference(loc, s1) + case (x, s1) => errorDerefNotPointer(loc, x, s1) + } + } + /** * Semantics for right-hand-side expressions. + * * @param exp the expression to execute * @param env the environment * @param store the initial store @@ -207,7 +237,7 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData */ protected def semeright(exp: AExpr, env: Env, store: Store): (EValue, Store) = exp match { - case access: AAccess => + case access: AFieldAccess => val (tv, s1) = semeright(access.record, env, store) tv match { case rec: RecordValue => @@ -235,17 +265,28 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData (left, right) match { case (lv: IntValue, rv: IntValue) => op match { + case Eqq => spec.eqq(lv, rv) case Divide => spec.divideInt(lv, rv) case GreatThan => spec.greatThanInt(lv, rv) case Minus => spec.minusInt(lv, rv) case Plus => spec.plusInt(lv, rv) case Times => spec.timesInt(lv, rv) - case _ => ??? } - case _ => errorArithmeticOnNonInt(op, s2) + case _ => errorArithmeticOnNonInt(exp.loc, op, s2) } } (cval, s2) + case e: AUnaryOp => + val (sub, s1) = semeright(e.subexp, env, store) + val cval = e.operator match { + case DerefOp => + sub match { + case crv: ReferenceValue => + s1.getOrElse(crv, errorUninitializedLocation(exp.loc, s1)) + case _ => errorDerefNotPointer(exp.loc, sub, s1) + } + } + (cval, s1) case AInput(_) => input(exp, env, store) case AAlloc(content, _) => @@ -254,11 +295,8 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData (l, s1 + (l -> cv)) case ANull(_) => (spec.nullValue, store) case ANumber(value, _) => (spec.constInt(value), store) - case AUnaryOp(_: RefOp.type, e: AExpr, _) => - semeref(e, env, store) - case op @ AUnaryOp(_: DerefOp.type, _, _) => - val (l, s1) = semeref(op, env, store) - (s1.getOrElse(l, errorDerefNotPointer(exp.loc, op, l, s1)), s1) + case AVarRef(e: AIdentifier, _) => + (env(e.declaration), store) case ACallFuncExpr(target, actualParams, _) => val (funValue, s1) = semeright(target, env, store) funValue match { @@ -271,11 +309,11 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData } val finStore = semf(f.fun, actualParamsValues, env, computedStore) (finStore(returnLoc), finStore) - case _ => errorCallNotFunction(funValue, s1) + case _ => errorCallNotFunction(target.loc, funValue, s1) } case id: AIdentifier => - val (l, s1) = semeref(id, env, store) - (s1.getOrElse(l, errorDerefNotPointer(exp.loc, id, l, s1)), s1) + val l = env(id.declaration) + (store.getOrElse(l, errorUninitializedLocation(exp.loc, store)), store) } /** @@ -301,48 +339,51 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData } else { Try(line.toInt) match { case Success(i) => (spec.constInt(i), store) - case Failure(_) => errorInputNotInt(store) + case Failure(_) => errorInputNotInt(exp.loc, store) } } } - case class ExecutionError(message: String, store: Store) extends RuntimeException(message) - - def errorCallNotFunction(funValue: EValue, store: Store) = - throw ExecutionError(s"Call to a non-function $funValue", store) + class ExecutionError(message: String, val store: Store) extends TipProgramException(s"Runtime error: $message") - def errorOutputNotInt(store: Store) = - throw ExecutionError(s"Output not supported for non-integer values", store) + def errorCallNotFunction(loc: Loc, funValue: EValue, store: Store) = + throw new ExecutionError(s"Call to a non-function $funValue ${loc.toStringLong}", store) - def errorInputNotInt(store: Store) = - throw ExecutionError(s"Input not supported for non-integer values", store) + def errorOutputNotInt(loc: Loc, store: Store) = + throw new ExecutionError(s"Output not supported for non-integer values ${loc.toStringLong}", store) - def errorErrorNonInt(v: EValue, store: Store) = - throw ExecutionError(s"Error statement expects integer value as error code, given $v", store) + def errorInputNotInt(loc: Loc, store: Store) = + throw new ExecutionError(s"Input not supported for non-integer values ${loc.toStringLong}", store) - def errorNonRefable(exp: AExpr, store: Store) = - throw ExecutionError(s"Cannot take the address of an expression at $exp", store) + def errorErrorNonInt(loc: Loc, v: EValue, store: Store) = + throw new ExecutionError(s"Error statement non-integer value $v ${loc.toStringLong}", store) - def errorArithmeticOnNonInt(op: BinaryOperator, store: Store) = - throw ExecutionError(s"Unable to apply the operator $op to non-integer values", store) + def errorArithmeticOnNonInt(loc: Loc, op: BinaryOperator, store: Store) = + throw new ExecutionError(s"Unable to apply the operator $op to non-integer value ${loc.toStringLong}", store) - def errorReturnNotInt(fun: AFunDeclaration, store: Store) = - throw ExecutionError(s"Return statement returning non-integer in function ${fun.name}", store) + def errorReturnNotInt(loc: Loc, fun: AFunDeclaration, store: Store) = + throw new ExecutionError(s"Return statement returning non-integer in function ${fun.name} ${loc.toStringLong}", store) def errorNullDereference(loc: Loc, store: Store) = - throw ExecutionError(s"Null pointer error at $loc", store) + throw new ExecutionError(s"Null pointer dereference ${loc.toStringLong}", store) def errorConditionNotInt(loc: Loc, store: Store) = - throw ExecutionError(s"Branch condition at $loc not evaluating to an integer", store) + throw new ExecutionError(s"Branch condition not evaluating to an integer ${loc.toStringLong}", store) - def errorDerefNotPointer(loc: Loc, target: AExpr, x: EValue, store: Store) = - throw ExecutionError(s"Dereferencing non-pointer $target at $loc: $x", store) + def errorDerefNotPointer(loc: Loc, x: EValue, store: Store) = + throw new ExecutionError(s"Dereferencing non-pointer $x ${loc.toStringLong}", store) def errorAccessNonRecord(loc: Loc, x: EValue, store: Store) = - throw ExecutionError(s"Accessing field on a value that is not a record at $loc: $x", store) + throw new ExecutionError(s"Accessing field on non-record value $x ${loc.toStringLong}", store) + + def errorWriteFieldRecord(loc: Loc, x: EValue, store: Store) = + throw new ExecutionError(s"Writing record to field $x ${loc.toStringLong}", store) def errorAccessMissingField(loc: Loc, rec: RecordValue, field: String, store: Store) = - throw ExecutionError(s"Missing field $field in record $rec at $loc", store) + throw new ExecutionError(s"Accessing missing field $field in record $rec ${loc.toStringLong}", store) + + def errorUninitializedLocation(loc: Loc, store: Store) = + throw new ExecutionError(s"Accessing uninitialized memory location ${loc.toStringLong}", store) } /** diff --git a/src/tip/interpreter/ValueSpecification.scala b/src/tip/interpreter/ValueSpecification.scala index 1580b88..dba2697 100644 --- a/src/tip/interpreter/ValueSpecification.scala +++ b/src/tip/interpreter/ValueSpecification.scala @@ -40,7 +40,6 @@ trait ValueSpecification { trait IntValue extends EValue { val i: Int - } /** diff --git a/src/tip/lattices/GenericLattices.scala b/src/tip/lattices/GenericLattices.scala index 91ebd07..0cf662f 100644 --- a/src/tip/lattices/GenericLattices.scala +++ b/src/tip/lattices/GenericLattices.scala @@ -60,7 +60,7 @@ class UniformProductLattice[L <: Lattice](val sublattice: L, n: Int) extends Lat (x zip y).map { case (xc, yc) => sublattice.lub(xc, yc) } } - private def error() = throw new IllegalArgumentException("products not of same length") + private def error() = throw new IllegalArgumentException("Products not of same length") } /** @@ -98,7 +98,7 @@ class FlatLattice[X] extends Lattice { */ implicit def unwrap(a: Element): X = a match { case FlatEl(n) => n - case _ => throw new IllegalArgumentException(s"cannot unlift $a") + case _ => throw new IllegalArgumentException(s"Cannot unlift $a") } val bottom: Element = Bot diff --git a/src/tip/parser/TipParser.scala b/src/tip/parser/TipParser.scala index db6a23e..12b6c36 100644 --- a/src/tip/parser/TipParser.scala +++ b/src/tip/parser/TipParser.scala @@ -78,11 +78,29 @@ class TipParser(val input: ParserInput) extends Parser with Comments { } def AssignableExpression: Rule1[Assignable] = rule { - (Identifier | DeRef) ~> { x: Assignable => + (DirectFieldWrite | IndirectFieldWrite | Identifier | DerefWrite) ~> { x: Assignable => x } } + def DirectFieldWrite: Rule1[ADirectFieldWrite] = rule { + push(cursor) ~ Identifier ~ wspStr(".") ~ Identifier ~> ((cur: Int, id: AIdentifier, field: AIdentifier) => ADirectFieldWrite(id, field.name, cur)) + } + + def IndirectFieldWrite: Rule1[AIndirectFieldWrite] = rule { + push(cursor) ~ wspStr("(") ~ wspStr("*") ~ Expression ~ wspStr(")") ~ wspStr(".") ~ Identifier ~> ( + ( + cur: Int, + exp: AExpr, + field: AIdentifier + ) => AIndirectFieldWrite(exp, field.name, cur) + ) + } + + def DerefWrite: Rule1[ADerefWrite] = rule { + push(cursor) ~ wspStr("*") ~ Expression ~> ((cur: Int, exp: AExpr) => ADerefWrite(exp, cur)) + } + def Expression: Rule1[AExpr] = rule { Operation ~ optional( @@ -95,18 +113,18 @@ class TipParser(val input: ParserInput) extends Parser with Comments { push(cursor) ~ "{" ~ zeroOrMore(Field).separatedBy(wspStr(",")) ~ "}" ~> ((cur: Int, fields: Seq[ARecordField]) => ARecord(fields.toList, cur)) } - def Access: Rule1[AAccess] = + def Access: Rule1[AFieldAccess] = rule { (Identifier | DeRef | Parens) ~ oneOrMore("." ~ Identifier) ~> ( ( e1: AExpr, fs: Seq[AIdentifier] - ) => fs.foldLeft(e1)((e: AExpr, f: AIdentifier) => AAccess(e, f.value, f.loc)) + ) => fs.foldLeft(e1)((e: AExpr, f: AIdentifier) => AFieldAccess(e, f.name, f.loc)) ) - }.asInstanceOf[Rule1[AAccess]] + }.asInstanceOf[Rule1[AFieldAccess]] def Field: Rule1[ARecordField] = rule { - push(cursor) ~ Identifier ~ wspStr(":") ~ Expression ~> ((cur: Int, id: AIdentifier, expr: AExpr) => ARecordField(id.value, expr, id.loc)) + push(cursor) ~ Identifier ~ wspStr(":") ~ Expression ~> ((cur: Int, id: AIdentifier, expr: AExpr) => ARecordField(id.name, expr, id.loc)) } def Operation: Rule1[AExpr] = rule { @@ -170,7 +188,7 @@ class TipParser(val input: ParserInput) extends Parser with Comments { } def Ref = rule { - push(cursor) ~ "&" ~ Identifier ~> ((cur: Int, id: AIdentifier) => AUnaryOp(RefOp, id, cur)) + push(cursor) ~ "&" ~ Identifier ~> ((cur: Int, id: AIdentifier) => AVarRef(id, cur)) } def DeRef: Rule1[AUnaryOp] = rule { @@ -184,7 +202,7 @@ class TipParser(val input: ParserInput) extends Parser with Comments { def TipFunction: Rule1[AFunDeclaration] = rule { push(cursor) ~ Identifier ~ "(" ~ zeroOrMore(IdentifierDeclaration).separatedBy(",") ~ ")" ~ FunBlock ~> { (cur: Int, id: AIdentifier, args: Seq[AIdentifierDeclaration], b: AFunBlockStmt) => - AFunDeclaration(id.value, args.toList, b, cur) + AFunDeclaration(id.name, args.toList, b, cur) } } diff --git a/src/tip/solvers/CubicSolver.scala b/src/tip/solvers/CubicSolver.scala index abeb8ef..86e3f4b 100644 --- a/src/tip/solvers/CubicSolver.scala +++ b/src/tip/solvers/CubicSolver.scala @@ -150,7 +150,7 @@ class CubicSolver[V, T](cycleElimination: Boolean = true) { * Adds a constraint of type t ∈ x. */ def addConstantConstraint(t: T, x: V): Unit = { - log.verb(s"Adding constraint $t \u2208 [[$x]]") + log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7") val bs = new mutable.BitSet() bs.add(t) addAndPropagateBits(bs, x) @@ -160,7 +160,7 @@ class CubicSolver[V, T](cycleElimination: Boolean = true) { * Adds a constraint of type x ⊆ y. */ def addSubsetConstraint(x: V, y: V): Unit = { - log.verb(s"Adding constraint [[$x]] \u2286 [[$y]]") + log.verb(s"Adding constraint \u27E6$x\u27E7 \u2286 \u27E6$y\u27E7") val nx = getOrPutNode(x) val ny = getOrPutNode(y) @@ -182,14 +182,14 @@ class CubicSolver[V, T](cycleElimination: Boolean = true) { * Adds a constraint of type t ∈ x ⇒ y ⊆ z. */ def addConditionalConstraint(t: T, x: V, y: V, z: V): Unit = { - log.verb(s"Adding constraint $t \u2208 [[$x]] => [[$y]] \u2286 [[$z]]") + log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7 => \u27E6$y\u27E7 \u2286 \u27E6$z\u27E7") val xn = getOrPutNode(x) if (xn.tokenSol.contains(t)) { // Already enabled addSubsetConstraint(y, z) } else if (y != z) { // Not yet enabled, add to pending list - log.verb(s"Condition $t \u2208 [[$x]] not yet enabled, adding ([[$y]],[[$z]]) to pending") + log.verb(s"Condition $t \u2208 \u27E6$x\u27E7 not yet enabled, adding (\u27E6$y\u27E7,\u27E6$z\u27E7) to pending") xn.conditionals .getOrElseUpdate(t, mutable.Set[(V, V)]()) .add((y, z)) diff --git a/src/tip/solvers/FixpointSolvers.scala b/src/tip/solvers/FixpointSolvers.scala index 9622d31..d701f59 100644 --- a/src/tip/solvers/FixpointSolvers.scala +++ b/src/tip/solvers/FixpointSolvers.scala @@ -208,8 +208,9 @@ trait WorklistFixpointSolver[N] extends MapLatticeSolver[N] with ListSetWorklist def process(n: N) = { val xn = x(n) - FixpointSolvers.log.verb(s"Processing $n in state $xn") + FixpointSolvers.log.verb(s"Processing $n, current state: $xn") val y = funsub(n, x) + FixpointSolvers.log.verb(s"New state: $y") if (y != xn) { x += n -> y add(outdep(n)) @@ -327,6 +328,7 @@ trait WorklistFixpointPropagationSolver[N] extends WorklistFixpointSolverWithRea // apply the transfer function FixpointSolvers.log.verb(s"Processing $n in state $xn") val y = transfer(n, xn) + FixpointSolvers.log.verb(s"Resulting state: $y") // propagate to all nodes that depend on this one for (m <- outdep(n)) propagate(y, m) } @@ -360,8 +362,9 @@ trait WorklistFixpointSolverWithReachabilityAndWidening[N] extends WorklistFixpo override def process(n: N) = { val xn = x(n) - FixpointSolvers.log.verb(s"Processing $n in state $xn") + FixpointSolvers.log.verb(s"Processing $n, current state $xn") val y = funsub(n, x) + FixpointSolvers.log.verb(s"New state: $y") if (y != xn) { x += n -> (if (loophead(n)) widen(xn, y) else y) add(outdep(n)) diff --git a/src/tip/solvers/UnificationTerms.scala b/src/tip/solvers/UnificationTerms.scala index c29f1ce..79b9782 100644 --- a/src/tip/solvers/UnificationTerms.scala +++ b/src/tip/solvers/UnificationTerms.scala @@ -1,5 +1,7 @@ package tip.solvers +import scala.collection.mutable + /** * A generic term: a variable [[Var]], a constructor [[Cons]], or a recursive term [[Mu]]. * @@ -87,51 +89,50 @@ trait TermOps[A] { def makeMu(v: Var[A], t: Term[A]): Mu[A] /** - * Constructor for fresh variables. - * The identity of the variable is uniquely determined by `x`. + * Constructor for fresh term variables. */ - def makeAlpha(x: Var[A]): Var[A] + def makeFreshVar(): Var[A] /** * Closes the term by replacing each free variable with its value in the given environment. - * Whenever a recursive type is detected, a [[Mu]] term is generated. + * Whenever a recursive term is detected, a [[Mu]] term is generated. * Remaining free variables are replaced by fresh variables that are implicitly universally quantified. * - * @param t the term to close - * @param env environment, map from variables to terms - */ - def close(t: Term[A], env: Map[Var[A], Term[A]]): Term[A] = closeRec(t, env) - - /** - * Closes the term by replacing each variable that appears as a subterm of with its value in the given environment. - * Whenever a recursive type is detected, a [[Mu]] term is generated. - * - * @param t the term to close - * @param env environment, map from variables to terms - * @param visited the set of already visited variables (empty by default) + * @param t the term to close + * @param env environment, map from term variables to terms + * @param freshvars map from recursive and unconstrained term variables to fresh term variables */ - private def closeRec(t: Term[A], env: Map[Var[A], Term[A]], visited: Set[Var[A]] = Set()): Term[A] = - t match { - case v: Var[A] => - if (!visited.contains(v) && env(v) != v) { - // no cycle found, and the variable does not map to itself - val cterm = closeRec(env(v), env, visited + v) - val newV = makeAlpha(v) - if (cterm.fv.contains(newV)) { - // recursive term found, make a [[Mu]] - makeMu(newV, cterm.subst(v, newV)) - } else - cterm - } else { - // an unconstrained (i.e. universally quantified) variable - makeAlpha(v) - } - case c: Cons[A] => - // substitute each free variable with its closed term - c.fv.foldLeft(t: Term[A]) { (acc, v) => - acc.subst(v, closeRec(v, env, visited)) - } - case m: Mu[A] => - makeMu(m.v, closeRec(m.t, env, visited)) - } + def close(t: Term[A], env: Map[Var[A], Term[A]], freshvars: mutable.Map[Var[A], Var[A]]): Term[A] = { + + def closeRec(t: Term[A], visited: Set[Var[A]] = Set()): Term[A] = + t match { + case v: Var[A] => + if (!visited.contains(v) && env(v) != v) { + // no recursion found, and the variable does not map to itself + val cterm = closeRec(env(v), visited + v) + val f = freshvars.get(v) + if (f.isDefined && cterm.fv.contains(f.get)) { + // recursive term found, make a [[Mu]] + makeMu(f.get, cterm.subst(v, f.get)) + } else + cterm + } else { + // recursive or unconstrained term variables, make a fresh term variable + freshvars.getOrElse(v, { + val w = makeFreshVar() + freshvars += v -> w + w + }) + } + case c: Cons[A] => + // substitute each free variable with its closed term + c.fv.foldLeft(t) { (acc, v) => + acc.subst(v, closeRec(v, visited)) + } + case m: Mu[A] => + makeMu(m.v, closeRec(m.t, visited)) + } + + closeRec(t) + } } diff --git a/src/tip/solvers/UnionFindSolver.scala b/src/tip/solvers/UnionFindSolver.scala index c85dbe1..1b15047 100644 --- a/src/tip/solvers/UnionFindSolver.scala +++ b/src/tip/solvers/UnionFindSolver.scala @@ -48,7 +48,7 @@ class UnionFindSolver[A] { unify(a1, a2) } case (x, y) => - throw new UnificationFailure(s"Can't unify $t1 and $t2 (with representatives $x and $y)") + throw new UnificationFailure(s"Cannot unify $t1 and $t2 (with representatives $x and $y)") } } @@ -105,4 +105,4 @@ class UnionFindSolver[A] { /** * Exception thrown in case of unification failure. */ -class UnificationFailure(message: String = null, cause: Throwable = null) extends RuntimeException(message, cause) +class UnificationFailure(message: String = null) extends RuntimeException(message) diff --git a/src/tip/types/Types.scala b/src/tip/types/Types.scala index 018a43a..5056178 100644 --- a/src/tip/types/Types.scala +++ b/src/tip/types/Types.scala @@ -5,7 +5,7 @@ import tip.solvers._ import tip.ast.AstNodeData._ import scala.language.implicitConversions -object TipType { +object Type { /** * Implicitly converts any AstNode to its type variable. @@ -18,36 +18,49 @@ object TipType { * function will be invoked implicitly to make the conversion (provided that the function is imported). * For more information about implicit conversions in Scala, see [[https://docs.scala-lang.org/tour/implicit-conversions.html]]. */ - implicit def ast2typevar(node: AstNode)(implicit declData: DeclarationData): Var[TipType] = + implicit def ast2typevar(node: AstNode)(implicit declData: DeclarationData): Var[Type] = node match { - case id: AIdentifier => TipVar(declData(id)) - case _ => TipVar(node) + case id: AIdentifier => VarType(declData(id)) + case _ => VarType(node) } + + implicit def ast2typevar(nodes: List[AstNode])(implicit declData: DeclarationData): List[Var[Type]] = + nodes.map(ast2typevar) } /** - * A type for a TIP variable or expression. + * Counter for producing fresh IDs. */ -sealed trait TipType +object Fresh { -object TipTypeOps extends TermOps[TipType] { + var n = 0 - def makeAlpha(node: Var[TipType]): Var[TipType] = node match { - case v: TipVar => TipAlpha(v.node.uid) - case alpha: TipAlpha => alpha + def next(): Int = { + n += 1 + n } +} + +/** + * A type for a TIP variable or expression. + */ +sealed trait Type + +object TipTypeOps extends TermOps[Type] { - def makeMu(v: Var[TipType], t: Term[TipType]): Mu[TipType] = TipMu(v, t) + def makeFreshVar(): Var[Type] = FreshVarType() + + def makeMu(v: Var[Type], t: Term[Type]): Mu[Type] = RecursiveType(v, t) } /** * Int type. */ -case class TipInt() extends TipType with Cons[TipType] { +case class IntType() extends Type with Cons[Type] { - val args: List[Term[TipType]] = List() + val args: List[Term[Type]] = List() - def subst(v: Var[TipType], t: Term[TipType]): Term[TipType] = this + def subst(v: Var[Type], t: Term[Type]): Term[Type] = this override def toString: String = "int" } @@ -55,12 +68,12 @@ case class TipInt() extends TipType with Cons[TipType] { /** * Function type. */ -case class TipFunction(params: List[Term[TipType]], ret: Term[TipType]) extends TipType with Cons[TipType] { +case class FunctionType(params: List[Term[Type]], ret: Term[Type]) extends Type with Cons[Type] { - val args: List[Term[TipType]] = ret :: params + val args: List[Term[Type]] = ret :: params - def subst(v: Var[TipType], t: Term[TipType]): Term[TipType] = - TipFunction(params.map { p => + def subst(v: Var[Type], t: Term[Type]): Term[Type] = + FunctionType(params.map { p => p.subst(v, t) }, ret.subst(v, t)) @@ -70,24 +83,25 @@ case class TipFunction(params: List[Term[TipType]], ret: Term[TipType]) extends /** * Pointer type. */ -case class TipRef(of: Term[TipType]) extends TipType with Cons[TipType] { +case class PointerType(of: Term[Type]) extends Type with Cons[Type] { - val args: List[Term[TipType]] = List(of) + val args: List[Term[Type]] = List(of) - def subst(v: Var[TipType], t: Term[TipType]): Term[TipType] = TipRef(of.subst(v, t)) + def subst(v: Var[Type], t: Term[Type]): Term[Type] = PointerType(of.subst(v, t)) - override def toString: String = s"&$of" + override def toString: String = s"\u2B61$of" } /** * Record type. * * A record type is represented as a term with a sub-term for every field name in the entire program. + * (This could be represented more concisely by using AbsentFieldType as a default.) */ -case class TipRecord(args: List[Term[TipType]])(implicit allFieldNames: List[String]) extends TipType with Cons[TipType] { +case class RecordType(args: List[Term[Type]])(implicit allFieldNames: List[String]) extends Type with Cons[Type] { - def subst(v: Var[TipType], t: Term[TipType]): Term[TipType] = - TipRecord(args.map { p => + def subst(v: Var[Type], t: Term[Type]): Term[Type] = + RecordType(args.map { p => p.subst(v, t) }) @@ -100,27 +114,40 @@ case class TipRecord(args: List[Term[TipType]])(implicit allFieldNames: List[Str .mkString(",")}}" } +case object AbsentFieldType extends Type with Cons[Type] { + + val args: List[Term[Type]] = List() + + def subst(v: Var[Type], t: Term[Type]): Term[Type] = this + + override def toString: String = "\u25C7" +} + /** * Type variable for a program variable or expression. */ -case class TipVar(node: AstNode) extends TipType with Var[TipType] { +case class VarType(node: AstNode) extends Type with Var[Type] { - override def toString: String = s"[[$node]]" + require(!node.isInstanceOf[AIdentifier], "Trying to construct type variable for identifier expression"); + + override def toString: String = s"\u27E6$node\u27E7" } /** - * Fresh type variable, whose identity is uniquely determined by `x`. + * Fresh type variable. */ -case class TipAlpha(x: Any) extends TipType with Var[TipType] { +case class FreshVarType(var id: Int = 0) extends Type with Var[Type] { + + id = Fresh.next() - override def toString: String = s"\u03B1<$x>" + override def toString: String = s"x$id" } /** * Recursive type (only created when closing terms). */ -case class TipMu(v: Var[TipType], t: Term[TipType]) extends TipType with Mu[TipType] { +case class RecursiveType(v: Var[Type], t: Term[Type]) extends Type with Mu[Type] { - def subst(sv: Var[TipType], to: Term[TipType]): Term[TipType] = - if (sv == v) this else TipMu(v, t.subst(sv, to)) + def subst(sv: Var[Type], to: Term[Type]): Term[Type] = + if (sv == v) this else RecursiveType(v, t.subst(sv, to)) } diff --git a/src/tip/util/Log.scala b/src/tip/util/Log.scala index 07dca51..383ba53 100644 --- a/src/tip/util/Log.scala +++ b/src/tip/util/Log.scala @@ -16,7 +16,7 @@ object Log { val None, Error, Warn, Info, Debug, Verbose = Value } - var defaultLevel = Level.None + var defaultLevel = Level.Info /** * Constructs a new logger. @@ -30,7 +30,7 @@ object Log { /** * A logger. */ -final case class Logger(var tag: String, level: Log.Level.Level) { +final case class Logger(var tag: String, var level: Log.Level.Level) { // val TAG_MAX_LEN = 30 // diff --git a/src/tip/util/TipProgramException.scala b/src/tip/util/TipProgramException.scala new file mode 100644 index 0000000..c2d7422 --- /dev/null +++ b/src/tip/util/TipProgramException.scala @@ -0,0 +1,6 @@ +package tip.util + +/** + * Exception throw in case of an error in the given TIP program. + */ +class TipProgramException(message: String) extends RuntimeException(message)