1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
package org.eclipse.cdt.codan.extension;
import org.eclipse.cdt.core.dom.ast.ASTVisitor;
import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
import org.eclipse.cdt.core.dom.ast.IASTExpression;
import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
import org.eclipse.cdt.core.dom.ast.IASTName;
import org.eclipse.cdt.core.dom.ast.IASTUnaryExpression;
import org.eclipse.cdt.core.dom.ast.IBinding;
import org.eclipse.cdt.core.dom.ast.IVariable;
public class ConditionalVisitor extends ASTVisitor {
private ExecutionState es;
private boolean value;
public ConditionalVisitor(ExecutionState es, boolean value) {
this.es = es;
this.value = value;
shouldVisitExpressions = true;
}
@Override
public int visit(IASTExpression node) {
int ret = PROCESS_CONTINUE;
// Modify execution state according to branch condition
ExecutionStateClause clause = null;
// *N.B.* content for condition IBlock is condition expression itself
if (node instanceof IASTBinaryExpression) { // TODO use visitor, nested BinaryExpressions
// FIXME compound conditionals
IASTBinaryExpression binExpr = (IASTBinaryExpression) node;
int op = binExpr.getOperator();
// FIXME other ops
// Check operator is an equality operator
if (op == IASTBinaryExpression.op_equals) { // if (x == 0)
IASTExpression o1 = binExpr.getOperand1();
if (o1 instanceof IASTIdExpression) {
IASTName name = ((IASTIdExpression) o1).getName();
clause = parseConditional(clause, name, binExpr.getOperand2(), value);
}
}
else if (op == IASTBinaryExpression.op_notequals) { // if (x != 0)
IASTExpression o1 = binExpr.getOperand1();
if (o1 instanceof IASTIdExpression) {
IASTName name = ((IASTIdExpression) o1).getName();
clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation
}
}
}
else if (node instanceof IASTUnaryExpression) { // if (!x)
IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
int op = uExpr.getOperator();
// Check operator is a negation operator
if (op == IASTUnaryExpression.op_not) {
IASTExpression operand = uExpr.getOperand();
if (operand instanceof IASTIdExpression) {
IASTName name = ((IASTIdExpression) operand).getName();
clause = parseConditional(clause, name, !value); // Negation
}
}
}
else if (node instanceof IASTIdExpression) { // if (x)
IASTName name = ((IASTIdExpression) node).getName();
clause = parseConditional(clause, name, value);
}
if (clause != null) {
es.addClause(clause);
// TODO Theorem Prover goes here! / Determine if branch is feasible
es.bindTruthAssignments();
ret = PROCESS_SKIP;
}
else {
// FIXME Handle unresolvable case
}
return ret;
}
private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) {
IBinding binding = name.resolveBinding();
if (binding instanceof IVariable) {
IVariable var = (IVariable) binding;
Boolean truth = ASTParserUtil.getTruthValue(valueExpr);
if (truth != null) {
clause = new ExecutionStateClause(var, truth == branchTruth);
}
}
return clause;
}
private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) {
IBinding binding = name.resolveBinding();
if (binding instanceof IVariable) {
IVariable var = (IVariable) binding;
clause = new ExecutionStateClause(var, branchTruth);
}
return clause;
}
}
|
