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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
/*******************************************************************************
* Copyright (c) 2009 Elliott Baron
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* Elliott Baron - initial API and implementation
*******************************************************************************/
package org.eclipse.cdt.codan.extension;
import java.util.Set;
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 Set<SymbolicState> output;
private SymbolicState input;
private boolean value;
public ConditionalVisitor(SymbolicState s, Set<SymbolicState> ret, boolean value) {
output = ret;
input = s;
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(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(name, binExpr.getOperand2(), !value); // Negation
}
}
else if (op == IASTBinaryExpression.op_logicalOr) {
// Disjunction creates two possible execution states
SymbolicState s1 = input.copy();
SymbolicState s2 = input.copy();
ConditionalVisitor cv1 = new ConditionalVisitor(s1, output, value);
ConditionalVisitor cv2 = new ConditionalVisitor(s2, output, value);
IASTExpression o1 = binExpr.getOperand1();
IASTExpression o2 = binExpr.getOperand2();
o1.accept(cv1);
o2.accept(cv2);
// don't process anymore, children will take care of this
ret = PROCESS_SKIP;
}
}
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(name, !value); // Negation
}
}
}
else if (node instanceof IASTIdExpression) { // if (x)
IASTName name = ((IASTIdExpression) node).getName();
clause = parseConditional(name, value);
}
if (clause != null) {
// Add clause to input
input.getExecutionState().addClause(clause);
// TODO Theorem Prover goes here! / Determine if branch is feasible
input.getExecutionState().bindTruthAssignments();
ret = PROCESS_SKIP;
}
else {
// FIXME Handle unresolvable case
}
return ret;
}
public Set<SymbolicState> getOutput() {
return output;
}
private ExecutionStateClause parseConditional(IASTName name, IASTExpression valueExpr, boolean branchTruth) {
ExecutionStateClause clause = null;
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(IASTName name, boolean branchTruth) {
ExecutionStateClause clause = null;
IBinding binding = name.resolveBinding();
if (binding instanceof IVariable) {
IVariable var = (IVariable) binding;
clause = new ExecutionStateClause(var, branchTruth);
}
return clause;
}
}
|
