Skip to content

Commit ee129ba

Browse files
committed
finish path conditions [ci skip]
1 parent 75d9281 commit ee129ba

File tree

1 file changed

+32
-13
lines changed

1 file changed

+32
-13
lines changed

src/passes/Souperify.cpp

Lines changed: 32 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -429,22 +429,23 @@ struct Trace : public Visitor<Trace> {
429429
bool bad = false;
430430
std::vector<Node*> nodes;
431431
std::unordered_set<Node*> addedNodes;
432+
std::unordered_set<Node*> pathConditions; // which conditions were added as path conditions
432433

433434
Trace(Builder& builder, SetLocal* set) : builder(builder), set(set) {
434435
auto* node = builder.setNodeMap[set];
435436
// Pull in all the dependencies, starting from the value itself.
436437
add(node);
437-
// Also pull in conditions based on the location of this node: e.g.
438-
// if it is inside an if's true branch, we can add a path-condition
439-
// for that.
440-
addPath(set);
441438
// If nothing bad showed up, still mark it as bad if it's trivial
442439
// and worthless.
443440
if (!bad) {
444441
if (nodes.size() <= 1) {
445442
bad = true;
446443
}
447444
}
445+
// Also pull in conditions based on the location of this node: e.g.
446+
// if it is inside an if's true branch, we can add a path-condition
447+
// for that.
448+
addPath(set);
448449
}
449450

450451
Node* add(Node* node) {
@@ -473,7 +474,9 @@ struct Trace : public Visitor<Trace> {
473474
break;
474475
}
475476
case Node::Type::Cond: {
476-
add(node->cond.block);
477+
if (!isPathCondition(node)) {
478+
add(node->cond.block);
479+
}
477480
add(node->cond.node);
478481
break;
479482
}
@@ -501,7 +504,7 @@ struct Trace : public Visitor<Trace> {
501504
auto iter = builder.expressionBlockMap.find(parent);
502505
if (iter != builder.expressionBlockMap.end()) {
503506
// Given the block, add a proper path-condition
504-
Node* node = iter.second;
507+
Node* node = iter->second;
505508
addPathTo(parent, curr, node);
506509
}
507510
curr = parent;
@@ -513,19 +516,26 @@ struct Trace : public Visitor<Trace> {
513516
// give as 'node'. Add a path condition for reaching the child.
514517
void addPathTo(Expression* parent, Expression* curr, Node* node) {
515518
if (auto* iff = parent->dynCast<If>()) {
519+
Index index;
516520
if (curr == iff->ifTrue) {
517-
..
518-
need to mark the Condition as pc and not a blockpc
521+
index = 0;
519522
} else if (curr == iff->ifFalse) {
520-
..
523+
index = 1;
521524
} else {
522525
WASM_UNREACHABLE();
523526
}
527+
auto* condition = node->getValue(index);
528+
pathConditions.insert(condition);
529+
add(condition);
524530
} else {
525531
WASM_UNREACHABLE();
526532
}
527533
}
528534

535+
bool isPathCondition(Node* node) {
536+
return pathConditions.count(node) == 1;
537+
}
538+
529539
bool isBad() {
530540
return bad;
531541
}
@@ -555,15 +565,17 @@ struct Printer : public Visitor<Printer> {
555565
std::cout << "\n; start LHS\n";
556566
// Index the nodes.
557567
for (auto* node : trace.nodes) {
558-
auto index = indexing.size();
559-
indexing[node] = index;
568+
if (!trace.isPathCondition(node)) { // pcs do not need to be indexed
569+
auto index = indexing.size();
570+
indexing[node] = index;
571+
}
560572
}
561573
// Print them out.
562574
for (auto* node : trace.nodes) {
563575
print(node);
564576
}
565577
// Finish up
566-
std::cout << "infer %" << indexing[trace.nodes.back()] << "\n\n";
578+
std::cout << "infer %" << indexing[builder.setNodeMap[trace.set]] << "\n\n";
567579
}
568580

569581
void print(Node* node) {
@@ -590,7 +602,14 @@ struct Printer : public Visitor<Printer> {
590602
break;
591603
}
592604
case Node::Type::Cond: {
593-
std::cout << "%" << indexing[node] << " = blockpc %" << indexing[node->cond.block] << ' ' << node->cond.index << " %" << indexing[node->cond.node] << ' ';
605+
if (!trace.isPathCondition(node)) {
606+
// blockpc
607+
std::cout << "%" << indexing[node] << " = blockpc %" << indexing[node->cond.block] << ' ' << node->cond.index;;
608+
} else {
609+
// pc
610+
std::cout << "pc";
611+
}
612+
std::cout << " %" << indexing[node->cond.node] << ' ';
594613
print(node->cond.value);
595614
break;
596615
}

0 commit comments

Comments
 (0)