Skip to content

Commit cfdd9dd

Browse files
committed
Cumulative updates
1 parent a8e9428 commit cfdd9dd

39 files changed

+669
-448
lines changed

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -143,8 +143,8 @@ To automatically format when the file is saved, go to File -> Settings..., under
143143

144144
## Authors
145145

146-
- [Gianluca Mezzetti](http://gmezzetti.name/)
147146
- [Anders Møller](http://cs.au.dk/~amoeller/)
147+
- [Gianluca Mezzetti](http://gmezzetti.name/)
148148

149149
with contributions from
150150

examples/cfa.tip

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ ide(k) { return k; }
55
foo(n,f) {
66
var r;
77
if (n==0) { f=ide; }
8-
r = (f)(n);
8+
r = f(n);
99
return r;
1010
}
1111

1212
main() {
1313
var x,y;
14-
x = 1;//input;
14+
x = input;
1515
if (x>0) { y = foo(x,inc); } else { y = foo(x,dec); }
1616
return y;
1717
}

src/tip/Tip.scala

Lines changed: 31 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ import org.parboiled2.ParseError
66
import tip.analysis.FlowSensitiveAnalysis.{Analysis => dfa, AnalysisOption => dfo}
77
import tip.analysis._
88
import tip.ast.AstNodeData._
9-
import tip.ast.AProgram
9+
import tip.ast.{AProgram, NoNormalizer}
1010
import tip.concolic.ConcolicEngine
1111
import tip.cfg._
1212
import tip.interpreter.ConcreteInterpreter
@@ -20,7 +20,6 @@ import scala.util.{Failure, Success}
2020
* Options for running the TIP system.
2121
*/
2222
class RunOption {
23-
val log = Log.logger[this.type]()
2423

2524
/**
2625
* If set, construct the (intraprocedural) control-flow graph after parsing.
@@ -82,7 +81,7 @@ class RunOption {
8281
*/
8382
def check(): Boolean =
8483
if (source == null) {
85-
log.error(s"Source file/directory missing")
84+
Tip.log.error(s"Source file/directory missing")
8685
false
8786
} else
8887
true
@@ -158,9 +157,17 @@ object Tip extends App {
158157
*/
159158
def processFile(file: File, options: RunOption) = {
160159
try {
161-
val program = Source.fromFile(file).mkString
160+
val program = {
161+
val bs = Source.fromFile(file)
162+
try {
163+
bs.mkString
164+
} finally {
165+
bs.close()
166+
}
167+
}
162168

163169
// parse the program
170+
log.verb("Parsing")
164171
val tipParser = new TipParser(program)
165172
val res = tipParser.InputLine.run()
166173

@@ -173,17 +180,21 @@ object Tip extends App {
173180
sys.exit(1)
174181
case Success(parsedNode: AProgram) =>
175182
// run normalizer
183+
log.verb("Normalizing")
176184
val programNode = options.normalizer.normalizeProgram(parsedNode)
177-
Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out)
185+
if (options.normalizer != NoNormalizer)
186+
Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out)
178187

179188
// run declaration analysis
180189
// (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]])
190+
log.verb("Declaration analysis")
181191
implicit val declData: DeclarationData = new DeclarationAnalysis(programNode).analyze()
182192

183193
// run selected intraprocedural flow-sensitive analyses
184194
if (options.cfg | options.dfAnalysis.exists(p => p._2 != dfo.Disabled && !dfo.interprocedural(p._2))) {
185195

186196
// generate control-flow graph
197+
log.verb("Building intraprocedural control flow graphs")
187198
val wcfg = IntraproceduralProgramCfg.generateFromProgram(programNode)
188199
if (options.cfg)
189200
Output.output(file, OtherOutput(OutputKindE.cfg), wcfg.toDot({ x =>
@@ -195,6 +206,7 @@ object Tip extends App {
195206
if (!dfo.interprocedural(v)) {
196207
FlowSensitiveAnalysis.select(s, v, wcfg).foreach { an =>
197208
// run the analysis
209+
log.verb(s"Performing ${an.getClass.getSimpleName}")
198210
val res = an.analyze().asInstanceOf[Map[CfgNode, _]]
199211
Output.output(file, DataFlowOutput(s), wcfg.toDot(Output.labeler(res), Output.dotIder), options.out)
200212
}
@@ -207,8 +219,10 @@ object Tip extends App {
207219

208220
// generate control-flow graph
209221
val wcfg = if (options.cfa) {
222+
log.verb("Building interprocedural control flow graph using control flow analysis")
210223
InterproceduralProgramCfg.generateFromProgramWithCfa(programNode)
211224
} else {
225+
log.verb("Building interprocedural control flow graph")
212226
InterproceduralProgramCfg.generateFromProgram(programNode)
213227
}
214228

@@ -223,6 +237,7 @@ object Tip extends App {
223237
if (dfo.interprocedural(v)) {
224238
FlowSensitiveAnalysis.select(s, v, wcfg).foreach { an =>
225239
// run the analysis
240+
log.verb(s"Starting ${an.getClass.getSimpleName}")
226241
val res = an.analyze()
227242
val res2 =
228243
if (dfo.contextsensitive(v))
@@ -238,19 +253,22 @@ object Tip extends App {
238253
// run type analysis, if selected
239254
if (options.types) {
240255
// (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]])
256+
log.verb("Starting TypeAnalysis")
241257
implicit val typeData: TypeData = new TypeAnalysis(programNode).analyze()
242258
Output.output(file, OtherOutput(OutputKindE.types), programNode.toTypedString, options.out)
243259
}
244260

245261
// run Andersen analysis, if selected
246262
if (options.andersen) {
263+
log.verb("Starting AndersenAnalysis")
247264
val s = new AndersenAnalysis(programNode)
248265
s.analyze()
249266
s.pointsTo()
250267
}
251268

252269
// run Steensgaard analysis, if selected
253270
if (options.steensgaard) {
271+
log.verb("Starting SteensgaardAnalysis")
254272
val s = new SteensgaardAnalysis(programNode)
255273
s.analyze()
256274
s.pointsTo()
@@ -259,31 +277,34 @@ object Tip extends App {
259277
// run control-flow analysis, if selected
260278
if (options.cfa) { // TODO: skip if InterproceduralProgramCfg.generateFromProgramWithCfa has been executed above
261279
val s = new ControlFlowAnalysis(programNode)
280+
log.verb("Starting ControlFlowAnalysis")
262281
s.analyze()
263282
}
264283

265284
// execute the program, if selected
266285
if (options.run) {
286+
log.verb("Starting ConcreteInterpreter")
267287
val intp = new ConcreteInterpreter(programNode)
268288
intp.semp()
269289
}
270290

271291
// concolically execute the program, if selected
272292
if (options.concolic) {
293+
log.verb("Starting ConcolicEngine")
273294
new ConcolicEngine(programNode).test()
274295
}
275-
276-
log.info("Success")
277296
}
278297
} catch {
298+
case e: TipProgramException =>
299+
log.error(e.getMessage)
300+
sys.exit(1)
279301
case e: Exception =>
280-
log.error(s"Error: ${e.getMessage}", e)
302+
log.error(s"Internal error: ${e.getMessage}", e)
281303
sys.exit(1)
282304
}
283305
}
284306

285307
// parse options
286-
Log.defaultLevel = Log.Level.Info
287308
val options = new RunOption()
288309
var i = 0
289310
while (i < args.length) {
@@ -322,6 +343,7 @@ object Tip extends App {
322343
options.concolic = true
323344
case "-verbose" =>
324345
Log.defaultLevel = Log.Level.Verbose
346+
log.level = Log.Level.Verbose
325347
case _ =>
326348
log.error(s"Unrecognized option $s")
327349
printUsage()

src/tip/analysis/AndersenAnalysis.scala

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ import tip.util.Log
66
import tip.ast.AstNodeData.DeclarationData
77
import scala.language.implicitConversions
88

9-
class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Null] with PointsToAnalysis {
9+
class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Unit] with PointsToAnalysis {
1010

1111
val log = Log.logger[this.type]()
1212

@@ -21,7 +21,7 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex
2121
val solver = new CubicSolver[Cell, Cell]
2222

2323
import AstOps._
24-
val allTargets: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc)
24+
val cells: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc)
2525

2626
NormalizedForPointsToAnalysis.assertContainsProgram(program)
2727
NoRecords.assertContainsProgram(program)
@@ -30,30 +30,27 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex
3030
* @inheritdoc
3131
*/
3232
def analyze(): Unit =
33-
visit(program, null)
33+
visit(program, ())
3434

3535
/**
3636
* Generates the constraints for the given sub-AST.
3737
* @param node the node for which it generates the constraints
3838
* @param arg unused for this visitor
3939
*/
40-
def visit(node: AstNode, arg: Null): Unit = {
40+
def visit(node: AstNode, arg: Unit): Unit = {
4141

4242
implicit def identifierToTarget(id: AIdentifier): Var = Var(id)
4343
implicit def allocToTarget(alloc: AAlloc): Alloc = Alloc(alloc)
4444

4545
node match {
4646
case AAssignStmt(id: AIdentifier, alloc: AAlloc, _) => ??? //<--- Complete here
47-
case AAssignStmt(id1: AIdentifier, AUnaryOp(RefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here
47+
case AAssignStmt(id1: AIdentifier, AVarRef(id2: AIdentifier, _), _) => ??? //<--- Complete here
4848
case AAssignStmt(id1: AIdentifier, id2: AIdentifier, _) => ??? //<--- Complete here
4949
case AAssignStmt(id1: AIdentifier, AUnaryOp(DerefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here
50-
case AAssignStmt(AUnaryOp(_, id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here
51-
case AAssignStmt(_: AIdentifier, ANull(_), _) =>
52-
case AAssignStmt(_: AIdentifier, _: AAtomicExpr, _) =>
53-
case ass: AAssignStmt => NormalizedForPointsToAnalysis.LanguageRestrictionViolation(s"Assignment $ass not expected")
50+
case AAssignStmt(ADerefWrite(id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here
5451
case _ =>
5552
}
56-
visitChildren(node, null)
53+
visitChildren(node, ())
5754
}
5855

5956
/**

src/tip/analysis/AvailableExpAnalysis.scala

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit dec
1414
import tip.cfg.CfgOps._
1515
import tip.ast.AstOps._
1616

17-
val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingExpressions.map(UnlabelledNode[AExpr]))
17+
val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingNonInputExpressions.map(UnlabelledNode[AExpr]))
1818

1919
NoPointers.assertContainsProgram(cfg.prog)
2020
NoRecords.assertContainsProgram(cfg.prog)
@@ -26,20 +26,20 @@ abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit dec
2626
case _: CfgFunEntryNode => Set()
2727
case r: CfgStmtNode =>
2828
r.data match {
29-
case ass: AAssignStmt =>
30-
ass.left match {
29+
case as: AAssignStmt =>
30+
as.left match {
3131
case id: AIdentifier =>
32-
(s union ass.right.appearingExpressions.map(UnlabelledNode[AExpr])).filter { e =>
32+
(s union as.right.appearingNonInputExpressions.map(UnlabelledNode[AExpr])).filter { e =>
3333
!(id.appearingIds subsetOf e.n.appearingIds)
3434
}
3535
case _ => ???
3636
}
3737
case exp: AExpr =>
38-
s union exp.appearingExpressions.map(UnlabelledNode[AExpr])
38+
s union exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr])
3939
case out: AOutputStmt =>
40-
s union out.value.appearingExpressions.map(UnlabelledNode[AExpr])
40+
s union out.exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr])
4141
case ret: AReturnStmt =>
42-
s union ret.value.appearingExpressions.map(UnlabelledNode[AExpr])
42+
s union ret.exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr])
4343
case _ => s
4444
}
4545
case _ => s

src/tip/analysis/ConstantPropagationAnalysis.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,13 +49,13 @@ object ConstantPropagationAnalysis {
4949

5050
/**
5151
* Interprocedural analysis that uses the worklist solver with reachability and propagation-style.
52-
* with call-string context sensivity.
52+
* with call-string context sensitivity.
5353
*/
5454
class CallString(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends CallStringValueAnalysis(cfg, ConstantPropagationLattice)
5555

5656
/**
5757
* Interprocedural analysis that uses the worklist solver with reachability and propagation-style.
58-
* with functional-approach context sensivity.
58+
* with functional-approach context sensitivity.
5959
*/
6060
class Functional(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends FunctionalValueAnalysis(cfg, ConstantPropagationLattice)
6161
}

src/tip/analysis/ControlFlowAnalysis.scala

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
88
import scala.language.implicitConversions
99

1010
class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
11-
extends DepthFirstAstVisitor[Null]
11+
extends DepthFirstAstVisitor[Unit]
1212
with Analysis[Map[AstNode, Set[AFunDeclaration]]] {
1313

1414
val log = Log.logger[this.type]()
@@ -35,9 +35,9 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
3535
* @inheritdoc
3636
*/
3737
def analyze(): Map[AstNode, Set[AFunDeclaration]] = {
38-
visit(program, null)
38+
visit(program, ())
3939
val sol = solver.getSolution
40-
log.info(s"Solution is:\n${sol.map { case (k, v) => s" [[$k]] = {${v.mkString(",")}}" }.mkString("\n")}")
40+
log.info(s"Solution is:\n${sol.map { case (k, v) => s" \u27E6$k\u27E7 = {${v.mkString(",")}}" }.mkString("\n")}")
4141
sol.map(vardecl => vardecl._1.n -> vardecl._2.map(_.fun))
4242
}
4343

@@ -46,7 +46,7 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
4646
* @param node the node for which it generates the constraints
4747
* @param arg unused for this visitor
4848
*/
49-
def visit(node: AstNode, arg: Null) = {
49+
def visit(node: AstNode, arg: Unit) = {
5050

5151
/**
5252
* Get the declaration if the supplied AstNode is an identifier,
@@ -63,9 +63,10 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
6363
node match {
6464
case fun: AFunDeclaration => ??? //<--- Complete here
6565
case AAssignStmt(id: AIdentifier, e, _) => ??? //<--- Complete here
66+
case ACallFuncExpr(targetFun: AIdentifier, args, _) if decl(targetFun).isInstanceOf[AFunDeclaration] => ??? //<--- Complete here (or remove this case)
6667
case ACallFuncExpr(targetFun, args, _) => ??? //<--- Complete here
6768
case _ =>
6869
}
69-
visitChildren(node, null)
70+
visitChildren(node, ())
7071
}
7172
}

src/tip/analysis/CopyConstantPropagationAnalysis.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,8 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
5858
}
5959

6060
// assignments
61-
case ass: AAssignStmt =>
62-
ass match {
61+
case as: AAssignStmt =>
62+
as match {
6363
case AAssignStmt(id: AIdentifier, right, _) =>
6464
val edges = assign(d, id.declaration, right)
6565
d match {
@@ -68,11 +68,11 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
6868
case _ =>
6969
edges
7070
}
71-
case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$ass not allowed")
71+
case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$as not allowed", as.loc)
7272
}
7373

7474
// return statement
75-
case ret: AReturnStmt => assign(d, AstOps.returnId, ret.value)
75+
case ret: AReturnStmt => assign(d, AstOps.returnId, ret.exp)
7676

7777
// all other kinds of statements: like no-ops
7878
case _ => List((d, IdEdge()))

0 commit comments

Comments
 (0)