Skip to content

Commit fe351c7

Browse files
fc63748fc63748
committed
dois testes unitarios e um teste de integracao
1 parent dadcad6 commit fe351c7

File tree

2 files changed

+302
-0
lines changed

2 files changed

+302
-0
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/BuiltinFunctionPredicate.java‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
package liquidjava.rj_language;
2+
3+
import liquidjava.errors.ErrorEmitter;
4+
import liquidjava.rj_language.parsing.ParsingException;
5+
import spoon.reflect.declaration.CtElement;
6+
7+
public class BuiltinFunctionPredicate extends Predicate {
8+
9+
public BuiltinFunctionPredicate(ErrorEmitter ee, CtElement elem, String functionName, String... params)
10+
throws ParsingException {
11+
super(functionName + "(" + getFormattedParams(params) + ")", elem, ee);
12+
}
13+
14+
public static BuiltinFunctionPredicate builtin_length(String param, CtElement elem, ErrorEmitter ee)
15+
throws ParsingException {
16+
return new BuiltinFunctionPredicate(ee, elem, "length", param);
17+
}
18+
19+
public static BuiltinFunctionPredicate builtin_addToIndex(String array, String index, String value, CtElement elem,
20+
ErrorEmitter ee) throws ParsingException {
21+
return new BuiltinFunctionPredicate(ee, elem, "addToIndex", index, value);
22+
}
23+
24+
private static String getFormattedParams(String... params) {
25+
StringBuilder sb = new StringBuilder();
26+
for (int i = 0; i < params.length; i++) {
27+
sb.append(params[i]);
28+
if (i < params.length - 1)
29+
sb.append(", ");
30+
}
31+
return sb.toString();
32+
}
33+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/Predicate.java‎

Lines changed: 269 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,269 @@
1+
package liquidjava.rj_language;
2+
3+
import java.util.ArrayList;
4+
import java.util.HashMap;
5+
import java.util.List;
6+
import java.util.Map;
7+
import java.util.stream.Collectors;
8+
import liquidjava.errors.ErrorEmitter;
9+
import liquidjava.errors.ErrorHandler;
10+
import liquidjava.processor.context.AliasWrapper;
11+
import liquidjava.processor.context.Context;
12+
import liquidjava.processor.context.GhostState;
13+
import liquidjava.processor.facade.AliasDTO;
14+
import liquidjava.rj_language.ast.BinaryExpression;
15+
import liquidjava.rj_language.ast.Expression;
16+
import liquidjava.rj_language.ast.FunctionInvocation;
17+
import liquidjava.rj_language.ast.GroupExpression;
18+
import liquidjava.rj_language.ast.Ite;
19+
import liquidjava.rj_language.ast.LiteralBoolean;
20+
import liquidjava.rj_language.ast.LiteralInt;
21+
import liquidjava.rj_language.ast.LiteralReal;
22+
import liquidjava.rj_language.ast.UnaryExpression;
23+
import liquidjava.rj_language.ast.Var;
24+
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
25+
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
26+
import liquidjava.rj_language.opt.ExpressionSimplifier;
27+
import liquidjava.rj_language.parsing.ParsingException;
28+
import liquidjava.rj_language.parsing.RefinementsParser;
29+
import liquidjava.utils.Utils;
30+
import spoon.reflect.declaration.CtElement;
31+
import spoon.reflect.declaration.CtType;
32+
import spoon.reflect.factory.Factory;
33+
34+
/**
35+
* Acts as a wrapper for Expression AST
36+
*
37+
* @author cgamboa
38+
*/
39+
public class Predicate {
40+
41+
protected Expression exp;
42+
protected String prefix;
43+
44+
/** Create a predicate with the expression true */
45+
public Predicate() {
46+
exp = new LiteralBoolean(true);
47+
}
48+
49+
/**
50+
* Create a new predicate with a refinement
51+
*
52+
* @param ref
53+
* @param element
54+
* @param e
55+
*
56+
* @throws ParsingException
57+
*/
58+
public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
59+
this(ref, element, e, element.getParent(CtType.class).getQualifiedName());
60+
}
61+
62+
/**
63+
* Create a new predicate with a refinement and a given prefix for the class
64+
*
65+
* @param ref
66+
* @param element
67+
* @param e
68+
* @param prefix
69+
*
70+
* @throws ParsingException
71+
*/
72+
public Predicate(String ref, CtElement element, ErrorEmitter e, String prefix) throws ParsingException {
73+
this.prefix = prefix;
74+
exp = parse(ref, element, e);
75+
if (e.foundError()) {
76+
return;
77+
}
78+
if (!(exp instanceof GroupExpression)) {
79+
exp = new GroupExpression(exp);
80+
}
81+
}
82+
83+
/** Create a predicate with the expression true */
84+
public Predicate(Expression e) {
85+
exp = e;
86+
}
87+
88+
protected Expression parse(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
89+
try {
90+
return RefinementsParser.createAST(ref, prefix);
91+
} catch (ParsingException e1) {
92+
ErrorHandler.printSyntaxError(e1.getMessage(), ref, element, e);
93+
throw e1;
94+
}
95+
}
96+
97+
protected Expression innerParse(String ref, ErrorEmitter e, String prefix) {
98+
try {
99+
return RefinementsParser.createAST(ref, prefix);
100+
} catch (ParsingException e1) {
101+
ErrorHandler.printSyntaxError(e1.getMessage(), ref, e);
102+
}
103+
return null;
104+
}
105+
106+
public Predicate changeAliasToRefinement(Context context, Factory f) throws Exception {
107+
Expression ref = getExpression();
108+
109+
Map<String, AliasDTO> alias = new HashMap<>();
110+
for (AliasWrapper aw : context.getAlias()) {
111+
alias.put(aw.getName(), aw.createAliasDTO());
112+
}
113+
114+
ref = ref.changeAlias(alias, context, f);
115+
return new Predicate(ref);
116+
}
117+
118+
public Predicate negate() {
119+
return new Predicate(new UnaryExpression("!", exp));
120+
}
121+
122+
public Predicate substituteVariable(String from, String to) {
123+
Expression ec = exp.clone();
124+
ec = ec.substitute(new Var(from), new Var(to));
125+
return new Predicate(ec);
126+
}
127+
128+
public List<String> getVariableNames() {
129+
List<String> l = new ArrayList<>();
130+
exp.getVariableNames(l);
131+
return l;
132+
}
133+
134+
public List<GhostState> getStateInvocations(List<GhostState> lgs) {
135+
if (lgs == null)
136+
return new ArrayList<>();
137+
List<String> all = lgs.stream().map(p -> p.getQualifiedName()).collect(Collectors.toList());
138+
List<String> toAdd = new ArrayList<>();
139+
exp.getStateInvocations(toAdd, all);
140+
141+
List<GhostState> gh = new ArrayList<>();
142+
for (String n : toAdd) {
143+
for (GhostState g : lgs)
144+
if (g.matches(n))
145+
gh.add(g);
146+
}
147+
148+
return gh;
149+
}
150+
151+
/** Change old mentions of previous name to the new name e.g., old(previousName) -> newName */
152+
public Predicate changeOldMentions(String previousName, String newName, ErrorEmitter ee) {
153+
Expression e = exp.clone();
154+
Expression prev = createVar(previousName).getExpression();
155+
List<Expression> le = new ArrayList<>();
156+
le.add(createVar(newName).getExpression());
157+
e.substituteFunction(Utils.OLD, le, prev);
158+
return new Predicate(e);
159+
}
160+
161+
public List<String> getOldVariableNames() {
162+
List<String> ls = new ArrayList<>();
163+
expressionGetOldVariableNames(this.exp, ls);
164+
return ls;
165+
}
166+
167+
private void expressionGetOldVariableNames(Expression exp, List<String> ls) {
168+
if (exp instanceof FunctionInvocation) {
169+
FunctionInvocation fi = (FunctionInvocation) exp;
170+
if (fi.getName().equals(Utils.OLD)) {
171+
List<Expression> le = fi.getArgs();
172+
for (Expression e : le) {
173+
if (e instanceof Var)
174+
ls.add(((Var) e).getName());
175+
}
176+
}
177+
}
178+
if (exp.hasChildren()) {
179+
for (var ch : exp.getChildren())
180+
expressionGetOldVariableNames(ch, ls);
181+
}
182+
}
183+
184+
public Predicate changeStatesToRefinements(List<GhostState> ghostState, String[] toChange, ErrorEmitter ee) {
185+
Map<String, Expression> nameRefinementMap = new HashMap<>();
186+
for (GhostState gs : ghostState) {
187+
if (gs.getRefinement() != null) { // is a state and not a ghost state
188+
String name = gs.getQualifiedName();
189+
Expression exp = innerParse(gs.getRefinement().toString(), ee, gs.getPrefix());
190+
nameRefinementMap.put(name, exp);
191+
// Also allow simple name lookup to enable hierarchy matching
192+
String simple = Utils.getSimpleName(name);
193+
nameRefinementMap.putIfAbsent(simple, exp);
194+
}
195+
}
196+
Expression e = exp.substituteState(nameRefinementMap, toChange);
197+
return new Predicate(e);
198+
}
199+
200+
public boolean isBooleanTrue() {
201+
return exp.isBooleanTrue();
202+
}
203+
204+
@Override
205+
public String toString() {
206+
return exp.toString();
207+
}
208+
209+
@Override
210+
public Predicate clone() {
211+
return new Predicate(exp.clone());
212+
}
213+
214+
public Expression getExpression() {
215+
return exp;
216+
}
217+
218+
public ValDerivationNode simplify() {
219+
return ExpressionSimplifier.simplify(exp.clone());
220+
}
221+
222+
public static Predicate createConjunction(Predicate c1, Predicate c2) {
223+
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
224+
}
225+
226+
public static Predicate createDisjunction(Predicate c1, Predicate c2) {
227+
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.OR, c2.getExpression()));
228+
}
229+
230+
public static Predicate createEquals(Predicate c1, Predicate c2) {
231+
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.EQ, c2.getExpression()));
232+
}
233+
234+
public static Predicate createITE(Predicate c1, Predicate c2, Predicate c3) {
235+
return new Predicate(new Ite(c1.getExpression(), c2.getExpression(), c3.getExpression()));
236+
}
237+
238+
public static Predicate createLit(String value, String type) {
239+
Expression ex;
240+
if (type.equals(Utils.BOOLEAN))
241+
ex = new LiteralBoolean(value);
242+
else if (type.equals(Utils.INT))
243+
ex = new LiteralInt(value);
244+
else if (type.equals(Utils.DOUBLE))
245+
ex = new LiteralReal(value);
246+
else if (type.equals(Utils.SHORT))
247+
ex = new LiteralInt(value);
248+
else if (type.equals(Utils.LONG))
249+
ex = new LiteralReal(value);
250+
else // if(type.equals(Utils.DOUBLE))
251+
ex = new LiteralReal(value);
252+
return new Predicate(ex);
253+
}
254+
255+
public static Predicate createOperation(Predicate c1, String op, Predicate c2) {
256+
return new Predicate(new BinaryExpression(c1.getExpression(), op, c2.getExpression()));
257+
}
258+
259+
public static Predicate createVar(String name) {
260+
return new Predicate(new Var(name));
261+
}
262+
263+
public static Predicate createInvocation(String name, Predicate... Predicates) {
264+
List<Expression> le = new ArrayList<>();
265+
for (Predicate c : Predicates)
266+
le.add(c.getExpression());
267+
return new Predicate(new FunctionInvocation(name, le));
268+
}
269+
}

0 commit comments

Comments
 (0)