Skip to content

Commit c06c210

Browse files
ailrstailrst
authored
fixes from cntlm with offline lifter (#311)
* support new lifter error format * more debugging asserts * fix cilvisitor repeatbits * keep going on lift failure * escape dotgraph label
1 parent d241006 commit c06c210

File tree

7 files changed

+130
-82
lines changed

7 files changed

+130
-82
lines changed

‎src/main/scala/cfg_visualiser/DotTools.scala

+15-5
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,13 @@ object IDGenerator {
1111
}
1212
}
1313

14+
15+
def escape(s: String) = {
16+
val n = s.replace("\"", "\\\"")
17+
n
18+
}
19+
20+
1421
def wrap(_input: String, width: Integer = 20, first : Boolean = true): String =
1522
var input = _input
1623

@@ -61,10 +68,12 @@ class DotNode(val id: String, val label: String) extends DotElement {
6168

6269
def equals(other: DotNode): Boolean = toDotString.equals(other.toDotString)
6370

64-
override def toString: String = toDotString
6571

6672
def toDotString: String =
67-
s"\"$id\"" + "[label=\"" + wrap(label, 100) + "\", shape=\"box\", fontname=\"Mono\", fontsize=\"5\"]"
73+
s"\"$id\"" + "[label=\"" + escape(wrap(label, 100)) + "\", shape=\"box\", fontname=\"Mono\", fontsize=\"5\"]"
74+
75+
76+
override def toString: String = toDotString
6877

6978
}
7079

@@ -81,8 +90,9 @@ class DotNode(val id: String, val label: String) extends DotElement {
8190

8291
def equals(other: DotArrow): Boolean = toDotString.equals(other.toDotString)
8392

93+
8494
def toDotString: String =
85-
s"\"${fromNode.id}\" $arrow \"${toNode.id}\"[label=\"$label\", style=\"$style\", color=\"$colour\"]"
95+
s"\"${fromNode.id}\" $arrow \"${toNode.id}\"[label=\"${escape(label)}\", style=\"$style\", color=\"$colour\"]"
8696
}
8797

8898
/** Represents a directed edge between two regular cfg nodes in a Graphviz dot file.
@@ -161,7 +171,7 @@ class DotStruct(val id: String, val details: String, val fields: Option[Iterable
161171
override def toString: String = toDotString
162172

163173
override def toDotString: String =
164-
s"$id " + "[label=" + label + "]"
174+
s"$id " + "[label=" + escape(label) + "]"
165175
}
166176

167177
class DotStructElement(val id: String, val field: Option[String]) extends DotElement {
@@ -183,7 +193,7 @@ case class StructArrow(
183193
def equals(other: DotArrow): Boolean = toDotString.equals(other.toDotString)
184194

185195
def toDotString: String =
186-
s"${from.toString} $arrow ${to.toString} [label=\"$label\", style=\"$style\", color=\"$colour\"]"
196+
s"${from.toString} $arrow ${to.toString} [label=\"${escape(label)}\", style=\"$style\", color=\"$colour\"]"
187197
}
188198

189199

‎src/main/scala/ir/cilvisitor/CILVisitor.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ class CILVisitorImpl(val v: CILVisitor) {
9090
}
9191
case Repeat(repeats, arg) => {
9292
val narg = visit_expr(arg)
93-
if (narg ne arg) Repeat(repeats, arg) else n
93+
if (narg ne arg) Repeat(repeats, narg) else n
9494
}
9595
case ZeroExtend(bits, arg) => {
9696
val narg = visit_expr(arg)
@@ -132,8 +132,8 @@ class CILVisitorImpl(val v: CILVisitor) {
132132
i.target = visit_rvar(i.target)
133133
i
134134
case m: MemoryStore =>
135-
m.value = visit_expr(m.value)
136135
m.index = visit_expr(m.index)
136+
m.value = visit_expr(m.value)
137137
m.mem = visit_mem(m.mem)
138138
m
139139
case m: MemoryLoad =>

‎src/main/scala/ir/eval/SimplifyExpr.scala

+61-45
Original file line numberDiff line numberDiff line change
@@ -15,18 +15,31 @@ var trace = false
1515
class SimpExpr(simplifier: Expr => (Expr, Boolean)) extends CILVisitor {
1616
var changedAnything = false
1717
var count = 0
18-
override def vexpr(e: Expr) =
19-
val (ne, changed) = simplifier(e)
18+
19+
def simplify(e: Expr) = {
20+
val (n, changed) = simplifier(e)
21+
2022
changedAnything = changedAnything || changed
23+
24+
if (changed) logSimp(e, n)
25+
(n, changed)
26+
}
27+
28+
override def vexpr(e: Expr) = {
29+
val e1 = e
30+
val cbefore = changedAnything
31+
val (ne, changed) = simplify(e)
2132
ChangeDoChildrenPost(
2233
ne,
23-
(e: Expr) => {
24-
val one = e
25-
val (ne, c) = simplifier(e)
26-
changedAnything = changedAnything || c
27-
ne
34+
(oe: Expr) => {
35+
val (ne2, c) = simplify(oe)
36+
if (!cbefore && changedAnything && (oe == e1)) {
37+
throw Exception(s"Intermediate changes but $e1 -> $oe -> $ne2")
38+
}
39+
ne2
2840
}
2941
)
42+
}
3043

3144
def apply(e: Expr) = {
3245
val ns = SimpExpr(simplifier)
@@ -38,18 +51,17 @@ class SimpExpr(simplifier: Expr => (Expr, Boolean)) extends CILVisitor {
3851
def sequenceSimp(a: Expr => (Expr, Boolean), b: Expr => (Expr, Boolean))(e: Expr): (Expr, Boolean) = {
3952
val (ne1, changed1) = a(e)
4053
if (ne1 == e && changed1) {
41-
Logger.error(s" ${SimplifyValidation.debugTrace.last}")
42-
throw Exception(s"No simp $e \n -> $ne1")
54+
val change = s" ${SimplifyValidation.debugTrace.last}"
55+
throw Exception(s"Simplifier $change returned 'changed' for identical expression $e \n -> $ne1")
4356
}
4457
val (ne2, changed2) = b(ne1)
4558
if (ne2 == ne1 && changed2) {
46-
// throw Exception("No simp")
47-
Logger.error(s" ${SimplifyValidation.debugTrace.last}")
48-
throw Exception(s"No simp $ne1 \n -> $ne2")
59+
val change = SimplifyValidation.debugTrace.takeRight(5).map(" " + _ ).mkString("\n")
60+
throw Exception(s"$change\nSimplifier returned 'changed' for identical expression $ne1 \n -> $ne2")
4961
}
5062
if (ne2 == e && (changed1 || changed2)) {
51-
Logger.error(s" ${SimplifyValidation.debugTrace.last}")
52-
throw Exception(s"No simp $e \n -> $ne1\n -> $ne2")
63+
val change = SimplifyValidation.debugTrace.takeRight(5).map(" " + _ ).mkString("\n")
64+
throw Exception(s"$change\nSimplifier returned 'changed' for identical expression $e \n -> $ne1\n -> $ne2")
5365
}
5466
(ne2, changed1 || changed2)
5567
}
@@ -234,15 +246,15 @@ def simplifyCmpInequalities(e: Expr): (Expr, Boolean) = {
234246
case _ => false
235247
}
236248
} =>
237-
BinaryExpr(BVADD, r, l)
249+
logSimp(e, BinaryExpr(BVADD, r, l))
238250

239251
case BinaryExpr(BoolAND, l @ BinaryExpr(BVEQ, _, _), r @ BinaryExpr(relop, _, _))
240252
if ineqToStrict.contains(relop) || strictIneq.contains(relop) => {
241-
BinaryExpr(BoolAND, r, l)
253+
logSimp(e, BinaryExpr(BoolAND, r, l))
242254
}
243255
case BinaryExpr(BoolAND, l @ UnaryExpr(BoolNOT, BinaryExpr(BVEQ, _, _)), r @ BinaryExpr(relop, _, _))
244256
if ineqToStrict.contains(relop) || strictIneq.contains(relop) => {
245-
BinaryExpr(BoolAND, r, l)
257+
logSimp(e, BinaryExpr(BoolAND, r, l))
246258
}
247259

248260
case BinaryExpr(BVCOMP, l, r) => {
@@ -636,7 +648,7 @@ def simplifyCmpInequalities(e: Expr): (Expr, Boolean) = {
636648
UnaryExpr(BoolNOT, BinaryExpr(BVEQ, lhs2, rhs2: BitVecLiteral))
637649
)
638650
if (ineqToStrict.contains(op) || strictIneq
639-
.contains(op)) && simplifyCond(BinaryExpr(ineqToStrict.get(op).getOrElse(op), rhs, rhs2)) == TrueLiteral
651+
.contains(op)) && rhs.getType == rhs2.getType && simplifyCond(BinaryExpr(ineqToStrict.get(op).getOrElse(op), rhs, rhs2)) == TrueLiteral
640652
&& lhs == lhs2 => {
641653
logSimp(e, l)
642654
}
@@ -847,27 +859,27 @@ def cleanupExtends(e: Expr): (Expr, Boolean) = {
847859
var changedAnything = true
848860

849861
val res = e match {
850-
case Extract(ed, 0, body) if size(body).get == ed => (body)
851-
case ZeroExtend(0, body) => (body)
852-
case SignExtend(0, body) => (body)
853-
case BinaryExpr(BVADD, body, BitVecLiteral(0, _)) => (body)
854-
case BinaryExpr(BVMUL, body, BitVecLiteral(1, _)) => (body)
855-
case Repeat(1, body) => (body)
856-
case Extract(ed, 0, ZeroExtend(extension, body)) if (body.getType == BitVecType(ed)) => (body)
857-
case Extract(ed, 0, SignExtend(extension, body)) if (body.getType == BitVecType(ed)) => (body)
862+
case Extract(ed, 0, body) if size(body).get == ed => logSimp(e, body)
863+
case ZeroExtend(0, body) => logSimp(e, body)
864+
case SignExtend(0, body) => logSimp(e, body)
865+
case BinaryExpr(BVADD, body, BitVecLiteral(0, _)) => logSimp(e, body)
866+
case BinaryExpr(BVMUL, body, BitVecLiteral(1, _)) => logSimp(e, body)
867+
case Repeat(1, body) => logSimp(e, body)
868+
case Extract(ed, 0, ZeroExtend(extension, body)) if (body.getType == BitVecType(ed)) => logSimp(e, body)
869+
case Extract(ed, 0, SignExtend(extension, body)) if (body.getType == BitVecType(ed)) => logSimp(e, body)
858870
case Extract(ed, 0, ZeroExtend(exts, body)) if exts + size(body).get >= ed && ed > size(body).get =>
859-
ZeroExtend(ed - size(body).get, body)
871+
logSimp(e, ZeroExtend(ed - size(body).get, body))
860872

861873
case BinaryExpr(BVEQ, ZeroExtend(x, body), y: BitVecLiteral) if y.value <= BigInt(2).pow(size(body).get) - 1 =>
862-
BinaryExpr(BVEQ, body, BitVecLiteral(y.value, size(body).get))
874+
logSimp(e, BinaryExpr(BVEQ, body, BitVecLiteral(y.value, size(body).get)))
863875

864876
case BinaryExpr(BVEQ, ZeroExtend(sz, expr), BitVecLiteral(0, sz2)) =>
865-
BinaryExpr(BVEQ, expr, BitVecLiteral(0, size(expr).get))
877+
logSimp(e, BinaryExpr(BVEQ, expr, BitVecLiteral(0, size(expr).get)))
866878

867879
// compose slices
868-
case Extract(ed1, be1, Extract(ed2, be2, body)) => Extract(ed1 + be2, be1 + be2, (body))
869-
case SignExtend(sz1, SignExtend(sz2, exp)) => SignExtend(sz1 + sz2, exp)
870-
case ZeroExtend(sz1, ZeroExtend(sz2, exp)) => ZeroExtend(sz1 + sz2, exp)
880+
case Extract(ed1, be1, Extract(ed2, be2, body)) => logSimp(e, Extract(ed1 + be2, be1 + be2, (body)))
881+
case SignExtend(sz1, SignExtend(sz2, exp)) => logSimp(e, SignExtend(sz1 + sz2, exp))
882+
case ZeroExtend(sz1, ZeroExtend(sz2, exp)) => logSimp(e, ZeroExtend(sz1 + sz2, exp))
871883

872884
// make subs more readable
873885
//case BinaryExpr(BVADD, x, b: BitVecLiteral) if eval.BitVectorEval.isNegative(b) => {
@@ -878,49 +890,49 @@ def cleanupExtends(e: Expr): (Expr, Boolean) = {
878890
case BinaryExpr(BVCONCAT, Extract(hi1, lo1, x1), ZeroExtend(ext, Extract(hi2, 0, x2))) if lo1 == ext + hi2 => {
879891
val b = "1" * (hi1 - lo1) ++ ("0" * ext) ++ "1" * hi2
880892
val n = BinaryExpr(BVAND, Extract(hi1, 0, x2), BitVecLiteral(BigInt(b, 2), hi1))
881-
n
893+
logSimp(e, n)
882894
}
883895

884896
// redundant extends
885897
// extract extended zero part
886-
case Extract(ed, bg, ZeroExtend(x, expr)) if (bg > size(expr).get) => BitVecLiteral(0, ed - bg)
898+
case Extract(ed, bg, ZeroExtend(x, expr)) if (bg > size(expr).get) => logSimp(e, BitVecLiteral(0, ed - bg))
887899
// extract below extend
888-
case Extract(ed, bg, ZeroExtend(x, expr)) if (bg < size(expr).get) && (ed < size(expr).get) => Extract(ed, bg, expr)
889-
case Extract(ed, bg, SignExtend(x, expr)) if (bg < size(expr).get) && (ed < size(expr).get) => Extract(ed, bg, expr)
900+
case Extract(ed, bg, ZeroExtend(x, expr)) if (bg < size(expr).get) && (ed < size(expr).get) => logSimp(e, Extract(ed, bg, expr))
901+
case Extract(ed, bg, SignExtend(x, expr)) if (bg < size(expr).get) && (ed < size(expr).get) => logSimp(e, Extract(ed, bg, expr))
890902

891-
case ZeroExtend(ed, Extract(hi, 0, e)) if size(e).get == hi + ed => BinaryExpr(BVAND, e, BinaryExpr(BVCONCAT, BitVecLiteral(0, ed), BitVecLiteral(BigInt(2).pow(hi)-1, hi)))
903+
case ZeroExtend(ed, Extract(hi, 0, e)) if size(e).get == hi + ed => logSimp(e, BinaryExpr(BVAND, e, BinaryExpr(BVCONCAT, BitVecLiteral(0, ed), BitVecLiteral(BigInt(2).pow(hi)-1, hi))))
892904

893-
case BinaryExpr(BVSHL, body, BitVecLiteral(n, _)) if size(body).get <= n => BitVecLiteral(0, size(body).get)
905+
case BinaryExpr(BVSHL, body, BitVecLiteral(n, _)) if size(body).get <= n => logSimp(e, BitVecLiteral(0, size(body).get))
894906

895907
// simplify convoluted bit test
896908
case BinaryExpr(BVEQ, BinaryExpr(BVSHL, ZeroExtend(n1, body), BitVecLiteral(n, _)), BitVecLiteral(0, _))
897909
if n1 == n => {
898-
BinaryExpr(BVEQ, body, BitVecLiteral(0, size(body).get))
910+
logSimp(e, BinaryExpr(BVEQ, body, BitVecLiteral(0, size(body).get)))
899911
}
900912
// assume (!(bvshl8(zero_extend6_2(R3_19[8:6]), 6bv8) == 128bv8));
901913
case BinaryExpr(
902914
BVEQ,
903915
BinaryExpr(BVSHL, ZeroExtend(n1, body @ Extract(hi, lo, v)), BitVecLiteral(n, _)),
904916
c @ BitVecLiteral(cval, _)
905917
) if lo == n && cval >= BigInt(2).pow(lo + n.toInt) => {
906-
BinaryExpr(BVEQ, body, Extract(hi + n.toInt, lo + n.toInt, c))
918+
logSimp(e, BinaryExpr(BVEQ, body, Extract(hi + n.toInt, lo + n.toInt, c)))
907919
}
908920
case BinaryExpr(BVEQ, BinaryExpr(BVSHL, b, BitVecLiteral(n, _)), c @ BitVecLiteral(0, _)) => {
909921
// b low bits are all zero due to shift
910-
BinaryExpr(BVEQ, b, BitVecLiteral(0, size(b).get))
922+
logSimp(e, BinaryExpr(BVEQ, b, BitVecLiteral(0, size(b).get)))
911923
}
912924
case BinaryExpr(BVEQ, BinaryExpr(BVSHL, b, BitVecLiteral(n, _)), c @ BitVecLiteral(cval, _))
913925
if cval != 0 && cval < BigInt(2).pow(n.toInt) => {
914926
// low bits are all zero due to shift, and cval low bits are not zero
915-
FalseLiteral
927+
logSimp(e, FalseLiteral)
916928
}
917929
case BinaryExpr(
918930
BVEQ,
919931
BinaryExpr(BVSHL, ZeroExtend(n1, body @ Extract(hi, lo, v)), BitVecLiteral(n, _)),
920932
c @ BitVecLiteral(cval, _)
921933
) if lo == n && cval >= BigInt(2).pow(n.toInt) => {
922934
// extract the part of cval we are testing and remove the shift on the lhs operand
923-
BinaryExpr(BVEQ, body, Extract((hi - lo) + n.toInt, n.toInt, c))
935+
logSimp(e, BinaryExpr(BVEQ, body, Extract((hi - lo) + n.toInt, n.toInt, c)))
924936
}
925937

926938
// bvnot to bvneg
@@ -997,10 +1009,13 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = {
9971009

9981010
case BinaryExpr(BVADD, ed @ SignExtend(sz, UnaryExpr(BVNOT, x)), bo @ BitVecLiteral(bv, sz2))
9991011
if size(ed).contains(sz2) && !BitVectorEval.isNegative(bo) =>
1000-
logSimp(e, BinaryExpr(BVADD, UnaryExpr(BVNEG, SignExtend(sz, x)), BitVecLiteral(bv - 1, sz2)), actual = false)
1012+
didAnything = false
1013+
logSimp(e, BinaryExpr(BVADD, UnaryExpr(BVNEG, SignExtend(sz, x)), BitVecLiteral(bv - 1, sz2)),
1014+
actual = false)
10011015

10021016
case BinaryExpr(BVADD, BinaryExpr(BVADD, y, ed @ UnaryExpr(BVNOT, x)), bo @ BitVecLiteral(off, sz2))
10031017
if size(ed).contains(sz2) && !(y.isInstanceOf[BitVecLiteral]) && !BitVectorEval.isNegative(bo) =>
1018+
didAnything = false
10041019
logSimp(
10051020
e,
10061021
BinaryExpr(BVADD, BinaryExpr(BVADD, y, UnaryExpr(BVNEG, x)), BitVecLiteral(off - 1, sz2)),
@@ -1009,6 +1024,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = {
10091024

10101025
case BinaryExpr(BVADD, BinaryExpr(BVADD, y, ed @ SignExtend(sz, UnaryExpr(BVNOT, x))), BitVecLiteral(off, sz2))
10111026
if size(ed).contains(sz2) && !(y.isInstanceOf[BitVecLiteral]) =>
1027+
didAnything = false
10121028
logSimp(
10131029
e,
10141030
BinaryExpr(BVADD, BinaryExpr(BVADD, y, UnaryExpr(BVNEG, SignExtend(sz, x))), BitVecLiteral(off - 1, sz2)),
@@ -1019,7 +1035,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = {
10191035
//case BinaryExpr(BVADD, BitVecLiteral(1, _), UnaryExpr(BVNEG, x)) => logSimp(e, UnaryExpr(BVNOT, x))
10201036
// case BinaryExpr(BVADD, UnaryExpr(BVNEG, x), BitVecLiteral(c, sz)) => logSimp(e, BinaryExpr(UnaryExpr(BVNOT, x), ))
10211037

1022-
case BinaryExpr(BVADD, UnaryExpr(BVNOT, x), BitVecLiteral(1, _)) => UnaryExpr(BVNEG, x)
1038+
case BinaryExpr(BVADD, UnaryExpr(BVNOT, x), BitVecLiteral(1, _)) => logSimp(e, UnaryExpr(BVNEG, x))
10231039

10241040
//case BinaryExpr(BVEQ, BinaryExpr(BVADD, x, y: BitVecLiteral), BitVecLiteral(0, _))
10251041
// if (eval.BitVectorEval.isNegative(y)) =>

‎src/main/scala/translating/GTIRBLoader.scala

+3-10
Original file line numberDiff line numberDiff line change
@@ -53,16 +53,7 @@ class GTIRBLoader(parserMap: immutable.Map[String, List[InsnSemantics]]) {
5353
instructionAddress.toString + "$" + i
5454
}
5555

56-
statements.appendAll(
57-
try {
58-
visitStmt(s, label)
59-
} catch {
60-
case e => {
61-
Logger.error(s"Failed to load insn: $e\n${e.getStackTrace.mkString("\n")}")
62-
Seq(Assert(FalseLiteral, Some(" Failed to load instruction")))
63-
}
64-
}
65-
)
56+
statements.appendAll(visitStmt(s, label))
6657
}
6758
instructionCount += 1
6859
}
@@ -238,6 +229,7 @@ class GTIRBLoader(parserMap: immutable.Map[String, List[InsnSemantics]]) {
238229
case c: TypeConstructorContext => visitIdent(c.str).match {
239230
case "FPRounding" => BitVecType(3)
240231
case "integer" => BitVecType(64)
232+
case "boolean" => BoolType
241233
case _ => throw Exception(s"unknown type ${ctx.getText}")
242234
}
243235
case _ => throw Exception(s"unknown type ${ctx.getText}")
@@ -331,6 +323,7 @@ class GTIRBLoader(parserMap: immutable.Map[String, List[InsnSemantics]]) {
331323
}
332324
(result, load)
333325

326+
334327
case "not_bool.0" => (resolveUnaryOp(BoolNOT, function, 0, typeArgs, args, ctx.getText), None)
335328
case "eq_enum.0" => (resolveBinaryOp(BoolEQ, function, 0, typeArgs, args, ctx.getText))
336329
case "or_bool.0" => (resolveBinaryOp(BoolOR, function, 0, typeArgs, args, ctx.getText))

‎src/main/scala/translating/GTIRBToIR.scala

+12-13
Original file line numberDiff line numberDiff line change
@@ -177,21 +177,20 @@ class GTIRBToIR(mods: Seq[Module], parserMap: immutable.Map[String, List[InsnSem
177177
procedure.removeBlocks(block)
178178
} else {
179179
if (!blockOutgoingEdges.contains(blockUUID)) {
180-
throw Exception (s"block ${block.label} in subroutine ${procedure.name} has no outgoing edges")
181-
}
182-
val outgoingEdges = blockOutgoingEdges(blockUUID)
183-
if (outgoingEdges.isEmpty) {
184-
throw Exception(s"block ${block.label} in subroutine ${procedure.name} has no outgoing edges")
185-
}
186-
187-
val (calls, jump) = if (outgoingEdges.size == 1) {
188-
val edge = outgoingEdges.head
189-
handleSingleEdge(block, edge, procedure, procedures)
180+
Logger.warn(s"block ${block.label} in subroutine ${procedure.name} no outgoing edges")
181+
} else if (blockOutgoingEdges(blockUUID).isEmpty) {
182+
Logger.warn(s"block ${block.label} in subroutine ${procedure.name} has no outgoing edges")
190183
} else {
191-
handleMultipleEdges(block, outgoingEdges, procedure)
184+
val outgoingEdges = blockOutgoingEdges(blockUUID)
185+
val (calls, jump) = if (outgoingEdges.size == 1) {
186+
val edge = outgoingEdges.head
187+
handleSingleEdge(block, edge, procedure, procedures)
188+
} else {
189+
handleMultipleEdges(block, outgoingEdges, procedure)
190+
}
191+
calls.foreach(c => block.statements.append(c))
192+
block.replaceJump(jump)
192193
}
193-
calls.foreach(c => block.statements.append(c))
194-
block.replaceJump(jump)
195194

196195
if (block.statements.nonEmpty) {
197196
cleanUpIfPCAssign(block, procedure)

0 commit comments

Comments
 (0)