Skip to content

Commit df34460

Browse files
committed
Cumulative updates
1 parent 2a53c11 commit df34460

File tree

8 files changed

+281
-7
lines changed

8 files changed

+281
-7
lines changed

README.md

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,31 @@ where `<source>` can be a file or a directory containing `.tip` files and
9090
To see the possible options, run `tip` without options.
9191
Option `-verbose` is recommended when developing and testing analyses.
9292

93+
## Visualizing control flow graphs and analysis results
94+
95+
The main function `Tip.scala` emits control flow graphs and analysis results as ".dot" files
96+
that can be processed by [Graphviz](https://www.graphviz.org/) to produce images, for example using the Graphviz dot command-line tool:
97+
```
98+
dot -O -Tpng out/example.tip__sign.dot
99+
```
100+
101+
## Program normalization
102+
103+
Some analyses require the programs use restricted subsets of TIP.
104+
The following kinds of normalization can be performed automatically:
105+
106+
- `-normalizecalls`:
107+
normalizes function calls to be top-level only and such that arguments are identifiers
108+
(e.g. `id1 = id2(id3,id4)`)
109+
- `-normalizereturns`:
110+
normalizes return expressions to be identifiers
111+
(e.g. `return id`)
112+
- `-normalizepointers`:
113+
normalizes pointer operations to primitive statements
114+
(`id = alloc P` where `P` is null or an integer constant, `id1 = &id2`, `id1 = id2`, `id1 = *id2`, `*id1 = id2`, or`id = null`)
115+
116+
If one or more of these options are enabled, the normalized program is printed to e.g. `out/example.tip__normalized.tip`.
117+
93118
## Help to Scala novices
94119

95120
This implementation takes advantage of many cool Scala language features that allow the code to be concise and flexible.
@@ -100,6 +125,7 @@ Still, the following language features deserve some extra attention:
100125
- [traits](https://docs.scala-lang.org/tour/traits.html)
101126
- [case classes](https://docs.scala-lang.org/tour/case-classes.html)
102127
- [companion objects](https://docs.scala-lang.org/tour/singleton-objects.html)
128+
- [abstract type members](https://docs.scala-lang.org/tour/abstract-types.html) (see e.g. [GenericLattices.scala](src/tip/lattices/GenericLattices.scala))
103129
- [implicit parameters](https://docs.scala-lang.org/tour/implicit-parameters.html) (see e.g. [TypeAnalysis.scala](src/tip/analysis/TypeAnalysis.scala))
104130
- [implicit conversions](https://docs.scala-lang.org/tour/implicit-conversions.html) (see e.g. [TipType.ast2typevar](src/tip/types/Types.scala))
105131
- [implicit classes](https://docs.scala-lang.org/overviews/core/implicit-classes.html) (see e.g. [AstNodeData.AstNodeWithDeclaration](src/tip/ast/AstNodeData.scala))

src/tip/Tip.scala

Lines changed: 21 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,8 @@ class RunOption {
7474
*/
7575
var concolic = false
7676

77+
var normalizer: tip.ast.Normalizer = tip.ast.NoNormalizer
78+
7779
/**
7880
* Checks that a source file or directory has been provided.
7981
* @return true if success
@@ -104,8 +106,6 @@ object Tip extends App {
104106
|
105107
| Options for analyzing programs:
106108
|
107-
| -cfg construct the (intraprocedural) control-flow graph, but do not perform any analysis
108-
| -icfg construct the interprocedural control-flow graph, but do not perform any analysis
109109
| -types enable type analysis
110110
| -cfa enable control-flow analysis (interprocedural analyses use the call-graph obtained by this analysis)
111111
| -andersen enable Andersen pointer analysis
@@ -140,8 +140,16 @@ object Tip extends App {
140140
| -run run the program as the last step
141141
| -concolic perform concolic testing (search for failing inputs using dynamic symbolic execution)
142142
|
143+
| Options for normalizing programs (can be combined):
144+
|
145+
| -normalizereturns normalize return statements
146+
| -normalizecalls normalize function calls
147+
| -normalizepointers normalize pointer usages
148+
|
143149
| Other options:
144150
|
151+
| -cfg construct the (intraprocedural) control-flow graph, but do not perform any analysis
152+
| -icfg construct the interprocedural control-flow graph, but do not perform any analysis
145153
| -verbose verbose output
146154
""".stripMargin)
147155

@@ -163,7 +171,11 @@ object Tip extends App {
163171
case Failure(e: Throwable) =>
164172
log.error(s"Failure parsing the program: $file", e)
165173
sys.exit(1)
166-
case Success(programNode: AProgram) =>
174+
case Success(parsedNode: AProgram) =>
175+
// run normalizer
176+
val programNode = options.normalizer.normalizeProgram(parsedNode)
177+
Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out)
178+
167179
// run declaration analysis
168180
// (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]])
169181
implicit val declData: DeclarationData = new DeclarationAnalysis(programNode).analyze()
@@ -278,6 +290,12 @@ object Tip extends App {
278290
val s = args(i)
279291
if (s.head == '-')
280292
s match {
293+
case "-normalizepointers" =>
294+
options.normalizer = new tip.ast.CombineNormalizers(options.normalizer, tip.ast.PointersNormalizer)
295+
case "-normalizecalls" =>
296+
options.normalizer = new tip.ast.CombineNormalizers(options.normalizer, tip.ast.CallsNormalizer)
297+
case "-normalizereturns" =>
298+
options.normalizer = new tip.ast.CombineNormalizers(options.normalizer, tip.ast.ReturnsNormalizer)
281299
case "-cfg" =>
282300
options.cfg = true
283301
case "-icfg" =>

src/tip/analysis/SignAnalysis.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -72,8 +72,8 @@ trait InterprocSignAnalysisMisc[N] {
7272
trait InterprocSignAnalysisFunctions extends MapLiftLatticeSolver[CfgNode] with InterprocSignAnalysisMisc[CfgNode] with InterproceduralForwardDependencies {
7373

7474
override def funsub(n: CfgNode, x: lattice.Element): lattice.sublattice.Element = {
75-
import lattice.sublattice._
76-
import cfg._
75+
import lattice.sublattice._ // with this import, 'sublattice' refers to the lattice of abstract states
76+
import cfg._ // gives easy access to the functionality in InterproceduralProgramCfg
7777

7878
new NormalizedCalls().assertContainsNode(n.data)
7979

@@ -87,7 +87,7 @@ trait InterprocSignAnalysisFunctions extends MapLiftLatticeSolver[CfgNode] with
8787
// return node
8888
case CfgStmtNode(_, _, _, ret: AReturnStmt) =>
8989
val j = join(n, x)
90-
j + (AstOps.returnId -> lattice.sublattice.sublattice.sublattice.eval(ret.value, j))
90+
j + (AstOps.returnId -> sublattice.sublattice.eval(ret.value, j))
9191

9292
// call nodes (like no-ops here)
9393
case _: CfgCallNode => join(n, x)

src/tip/ast/Ast.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,8 @@ case class AProgram(funs: List[AFunDeclaration], loc: Loc) extends AstNode {
165165
private def findMainFunction(): Option[AFunDeclaration] =
166166
funs.find(decl => decl.name == "main")
167167

168+
override def toString: String =
169+
s"${this.print(PartialFunction.empty)}"
168170
}
169171

170172
case class AFunDeclaration(name: String, args: List[AIdentifierDeclaration], stmts: AFunBlockStmt, loc: Loc) extends ADeclaration {

src/tip/ast/TipNormalizers.scala

Lines changed: 221 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,221 @@
1+
package tip.ast
2+
3+
class Normalizer {
4+
5+
var lastUid: Int = 0
6+
def newVariable(): String = {
7+
lastUid += 1
8+
s"tmp_$lastUid"
9+
}
10+
11+
/** The list of declarations that have to be added in the current function */
12+
val declarations: scala.collection.mutable.ListBuffer[AIdentifierDeclaration] = scala.collection.mutable.ListBuffer.empty
13+
14+
/** Adds a declaration */
15+
def addDeclaration(decl: AIdentifierDeclaration): Unit = declarations += decl
16+
17+
/** The list of statements to be added in the current block.
18+
* This will mostly be assignments but can be any statement that can be in a nested block */
19+
val statements: scala.collection.mutable.ListBuffer[AStmtInNestedBlock] = scala.collection.mutable.ListBuffer.empty
20+
21+
/** Adds a statement */
22+
def addStatement(stmt: AStmtInNestedBlock): Unit = statements += stmt
23+
24+
/** Normalizes an AExpr */
25+
def normalizeExpr(e: AExpr): AExpr =
26+
e match {
27+
case a: Assignable => normalizeAssignable(a)
28+
case r: ARecord => r.copy(fields = r.fields.map(normalizeRecordField))
29+
case call: ACallFuncExpr => call.copy(targetFun = normalizeExpr(call.targetFun), args = call.args.map(normalizeExpr))
30+
case op: ABinaryOp => op.copy(left = normalizeExpr(op.left), right = normalizeExpr(op.right))
31+
case _ => e
32+
}
33+
34+
/** Normalizes an AExpr into an AIdentifier. This is not used by the Normalizer class but useful for subclasses, as this is a common operation */
35+
def normalizeToIdentifier(right: AExpr): AIdentifier =
36+
right match {
37+
case id: AIdentifier => id
38+
case _ =>
39+
val tmpVar = newVariable()
40+
val id = AIdentifier(tmpVar, right.loc)
41+
addDeclaration(AIdentifierDeclaration(tmpVar, right.loc))
42+
addStatement(normalizeStmtInNestedBlock(AAssignStmt(AIdentifier(tmpVar, right.loc), right, right.loc)))
43+
id
44+
}
45+
46+
/** Normalizes an ARecordField. */
47+
def normalizeRecordField(f: ARecordField): ARecordField =
48+
f.copy(exp = normalizeExpr(f.exp))
49+
50+
/** Normalizes an Assignable. */
51+
def normalizeAssignable(e: Assignable): Assignable =
52+
e match {
53+
case _: AIdentifier => e
54+
case uop: AUnaryOp => uop.copy(target = normalizeExpr(uop.target))
55+
}
56+
57+
/** Helper function to insert statements if there are any to insert before `stmt`. Otherwise, returns the same statement. */
58+
def nestedBlock(stmt: AStmtInNestedBlock): AStmtInNestedBlock =
59+
if (statements.isEmpty) { stmt } else {
60+
val res = ANestedBlockStmt(statements.toList :+ stmt, stmt.loc)
61+
statements.clear()
62+
res
63+
}
64+
65+
/** Normalizes an AStmtInNestedBlock. */
66+
def normalizeStmtInNestedBlock(stmt: AStmtInNestedBlock): AStmtInNestedBlock =
67+
stmt match {
68+
case stmt: AAssignStmt =>
69+
nestedBlock(stmt.copy(left = normalizeAssignable(stmt.left), right = normalizeExpr(stmt.right)))
70+
case stmt: ANestedBlockStmt =>
71+
stmt.copy(body = stmt.body.map(normalizeStmtInNestedBlock))
72+
case stmt: AIfStmt =>
73+
// It is important to first normalizes the if/else branches before calling nestedBlock, so that added statements for each branch remain in the corresponding branch, and added statements for the guard are added before the if.
74+
val ifBranch2 = normalizeStmtInNestedBlock(stmt.ifBranch)
75+
val elseBranch2 = stmt.elseBranch.map(normalizeStmtInNestedBlock)
76+
nestedBlock(stmt.copy(guard = normalizeExpr(stmt.guard), ifBranch = ifBranch2, elseBranch = elseBranch2))
77+
case stmt: AOutputStmt =>
78+
nestedBlock(stmt.copy(value = normalizeExpr(stmt.value)))
79+
case stmt: AErrorStmt =>
80+
nestedBlock(stmt.copy(value = normalizeExpr(stmt.value)))
81+
case stmt: AWhileStmt =>
82+
val innerBlock2 = normalizeStmtInNestedBlock(stmt.innerBlock)
83+
nestedBlock(stmt.copy(guard = normalizeExpr(stmt.guard), innerBlock = innerBlock2))
84+
}
85+
86+
/** Normalizes a AReturnStmt */
87+
def normalizeReturnStmt(ret: AReturnStmt): AReturnStmt =
88+
ret.copy(value = normalizeExpr(ret.value))
89+
90+
/** Normalizes a AFunBlockStmt */
91+
def normalizeFunBlockStmt(stmt: AFunBlockStmt): AFunBlockStmt = {
92+
// Normalizes its body
93+
val others2 = stmt.others.map(normalizeStmtInNestedBlock)
94+
// And normalizes its return statement
95+
val ret2 = normalizeReturnStmt(stmt.ret)
96+
// Add declarations to the function if needed
97+
val declarations2 = if (declarations.isEmpty) {
98+
stmt.declarations
99+
} else {
100+
stmt.declarations :+ AVarStmt(declarations.toList, stmt.loc)
101+
}
102+
// Add statements before the return statement if needed
103+
val others3 = if (statements.isEmpty) {
104+
others2
105+
} else {
106+
others2 :+ ANestedBlockStmt(statements.toList, stmt.loc)
107+
}
108+
declarations.clear()
109+
statements.clear()
110+
stmt.copy(declarations = declarations2, others = others3, ret = ret2)
111+
}
112+
113+
/** Normalizes a AFunDeclaration */
114+
def normalizeDeclaration(decl: AFunDeclaration): AFunDeclaration =
115+
decl.copy(stmts = normalizeFunBlockStmt(decl.stmts))
116+
117+
/** Normalizes a AProgram */
118+
def normalizeProgram(program: AProgram): AProgram =
119+
program.copy(funs = program.funs.map(normalizeDeclaration))
120+
}
121+
122+
/**
123+
* Combines two normalizers, running `normalizer1` followed by `normalizer2` on the input program.
124+
*/
125+
class CombineNormalizers(normalizer1: Normalizer, normalizer2: Normalizer) extends Normalizer {
126+
override def normalizeProgram(program: AProgram): AProgram =
127+
normalizer2.normalizeProgram(normalizer1.normalizeProgram(program))
128+
}
129+
130+
/** A normalizer that does nothing. */
131+
object NoNormalizer extends Normalizer {
132+
// We don't *have* to redefine normalizeProgram, because its definition in Normalizer ends up returning the same program, but this makes things clearer.
133+
override def normalizeProgram(program: AProgram): AProgram = program
134+
}
135+
136+
/**
137+
* Normalize return statements so that we only have returns of the form `return id` where id is an identifier
138+
*/
139+
object ReturnsNormalizer extends Normalizer {
140+
override def normalizeReturnStmt(ret: AReturnStmt): AReturnStmt =
141+
// [[return e]] becomes [[return id]]
142+
ret.copy(value = normalizeToIdentifier(ret.value))
143+
}
144+
145+
/**
146+
* Normalize function calls to fit into the NormalizedCalls sub-language, in which all function calls should have the form [[id = id(id1, id2, ...)]].
147+
*/
148+
object CallsNormalizer extends Normalizer {
149+
override def normalizeExpr(e: AExpr): AExpr =
150+
e match {
151+
case f: ACallFuncExpr =>
152+
// Normalizes the function call, but also replaces it by an identifier assigned to its result.
153+
// The only case where this replacement is not done is handled by normalizeStmtInNestedBlock, when we already have the form [[id = e(e1, e2, ...)]]
154+
normalizeToIdentifier(normalizeFunctionCall(f))
155+
case _ => super.normalizeExpr(e)
156+
}
157+
158+
def normalizeFunctionCall(f: ACallFuncExpr): ACallFuncExpr =
159+
// [[e(e1, e2, ...)]] becomes [[id(id1, id2, ...)]]
160+
f.copy(targetFun = normalizeToIdentifier(f.targetFun), args = f.args.map(normalizeToIdentifier))
161+
162+
override def normalizeStmtInNestedBlock(stmt: AStmtInNestedBlock) =
163+
stmt match {
164+
case AAssignStmt(left: AIdentifier, right: ACallFuncExpr, loc) =>
165+
// [[id = e(e1, e2, ...)]] form, normalize the call e(e1, e2, ...) to id(id1, id2, ...)
166+
nestedBlock(AAssignStmt(left, normalizeFunctionCall(right), loc))
167+
case _ =>
168+
// Other cases are handled by normalizeExpr.
169+
super.normalizeStmtInNestedBlock(stmt)
170+
}
171+
}
172+
173+
/**
174+
* Normalize pointers to fit in the NormalizedForPointsToAnalysis sub-language.
175+
* In that sub-language, the only allowed pointer statements are the following:
176+
* id = alloc P where P is null or an integer constant
177+
* id1 = &id2
178+
* id1 = id2
179+
* id1 = *id2
180+
* *id1 = id2
181+
* id = null
182+
*/
183+
object PointersNormalizer extends Normalizer {
184+
185+
/** Normalizes the left-hand side of an assignment so that it has the form id or *id */
186+
def normalizeLeft(left: Assignable): Assignable =
187+
left match {
188+
case _: AIdentifier => left
189+
case AUnaryOp(_, _: AIdentifier, _) => left
190+
case AUnaryOp(op, target, loc) =>
191+
val tmpVar = newVariable()
192+
val id = AIdentifier(tmpVar, left.loc)
193+
addDeclaration(AIdentifierDeclaration(tmpVar, left.loc))
194+
addStatement(normalizeStmtInNestedBlock(AAssignStmt(id, target, left.loc)))
195+
AUnaryOp(op, id, left.loc)
196+
}
197+
198+
/** Normalize the right-hand side of an assignment so that it has one of the form alloc P, null, &id, *id, or id. */
199+
def normalizeRight(right: AExpr): AExpr =
200+
right match {
201+
case op: AUnaryOp =>
202+
op.copy(target = normalizeToIdentifier(op.target))
203+
case _: AIdentifier => right
204+
case _: ANull => right
205+
case _: AAlloc => right
206+
case _ =>
207+
/* Other cases are treated as already normalized. Maybe it shouldn't be the case, but such other cases are not supported by the NormalizedForPointsToAnalysis sub-language in any case. */
208+
right
209+
}
210+
211+
override def normalizeStmtInNestedBlock(stmt: AStmtInNestedBlock) =
212+
stmt match {
213+
case AAssignStmt(left: AIdentifier, right, _) =>
214+
// [[id = right]] form, normalizes right only
215+
nestedBlock(AAssignStmt(left, normalizeRight(right), stmt.loc))
216+
case AAssignStmt(left, right, _) =>
217+
// [[left = right]] form where left is a unary operation, normalizes left, and normalizes right to an identifier.
218+
nestedBlock(AAssignStmt(normalizeLeft(left), normalizeToIdentifier(right), stmt.loc))
219+
case _ => super.normalizeStmtInNestedBlock(stmt)
220+
}
221+
}

src/tip/interpreter/Interpreter.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -269,6 +269,7 @@ abstract class Interpreter(program: AProgram)(implicit declData: DeclarationData
269269
*/
270270
private def input(): IntValue = {
271271
print(s"Enter input: ")
272+
Console.flush()
272273
val line = scala.io.StdIn.readLine()
273274
if (line == null) {
274275
spec.constInt(0)

src/tip/lattices/GenericLattices.scala

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,11 @@ trait Lattice {
99

1010
/**
1111
* The type of the elements of this lattice.
12+
*
13+
* To novice Scala programmers:
14+
* This is an example of an abstract type member. In this trait, `Element` is just a name for a type.
15+
* It is constrained in sub-traits and sub-classes, similarly to type parameters in generic classes.
16+
* For more information about abstract type members in Scala, see [[https://docs.scala-lang.org/tour/abstract-types.html]].
1217
*/
1318
type Element
1419

src/tip/util/Output.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ object Output {
2323
case OtherOutput(OutputKindE.`cfg`) => "_cfg.dot"
2424
case OtherOutput(OutputKindE.`icfg`) => "_icfg.dot"
2525
case OtherOutput(OutputKindE.`types`) => "_types.ttip"
26+
case OtherOutput(OutputKindE.`normalized`) => "_normalized.tip"
2627
case DataFlowOutput(k) =>
2728
s"_$k.dot"
2829
case _ => ???
@@ -118,7 +119,7 @@ object Output {
118119
* Different kinds of output (determine output file names).
119120
*/
120121
object OutputKindE extends Enumeration {
121-
val cfg, icfg, types = Value
122+
val cfg, icfg, types, normalized = Value
122123
}
123124

124125
sealed trait OutputKind

0 commit comments

Comments
 (0)