Skip to content

Commit 8abce72

Browse files
Kirill GolubevKirill Golubev
Kirill Golubev
authored and
Kirill Golubev
committed
formatting
1 parent e754efe commit 8abce72

3 files changed

Lines changed: 137 additions & 178 deletions

File tree

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ public static void main(String[] args) {
1818
String file = args.length == 0 ? allPath : args[0];
1919
ErrorEmitter ee = launch(file);
2020
if (ee.foundError()) {
21+
System.out.println("Found errors. Analysis failed!");
2122
System.out.println(ee.getFullMessage());
2223
System.exit(ee.getErrorStatus());
2324
} else {
@@ -65,7 +66,7 @@ public static ErrorEmitter launch(String file) {
6566
processingManager.process(v);
6667
// To search all previous packages
6768
// processingManager.process(factory.Package().getRootPackage());
68-
69+
System.out.println("after process");
6970
return ee;
7071

7172
}

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java‎

Lines changed: 0 additions & 140 deletions
This file was deleted.

liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java renamed to liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/solver_wrapper/TranslatorToZ3.java

Lines changed: 135 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,23 @@
11
package liquidjava.smt;
22

3+
import java.util.ArrayList;
34
import java.util.HashMap;
45
import java.util.List;
56
import java.util.Map;
7+
import java.util.stream.Stream;
68

7-
import com.martiansoftware.jsap.SyntaxException;
8-
import com.microsoft.z3.ArithExpr;
9-
import com.microsoft.z3.ArrayExpr;
10-
import com.microsoft.z3.BoolExpr;
11-
import com.microsoft.z3.Expr;
12-
import com.microsoft.z3.FPExpr;
13-
import com.microsoft.z3.FuncDecl;
14-
import com.microsoft.z3.IntExpr;
15-
import com.microsoft.z3.IntNum;
16-
import com.microsoft.z3.RealExpr;
17-
import com.microsoft.z3.Solver;
18-
import com.microsoft.z3.Sort;
19-
import com.microsoft.z3.Status;
9+
import com.microsoft.z3.*;
2010

2111
import liquidjava.processor.context.AliasWrapper;
12+
import liquidjava.processor.context.GhostFunction;
13+
import liquidjava.processor.context.GhostState;
14+
import liquidjava.processor.context.RefinedVariable;
15+
import liquidjava.smt.solver_wrapper.smt;
16+
import spoon.reflect.reference.CtTypeReference;
2217

23-
public class TranslatorToZ3 {
18+
public class TranslatorToZ3 extends smt {
2419

25-
private com.microsoft.z3.Context z3 = new com.microsoft.z3.Context();
26-
private Map<String, Expr<?>> varTranslation = new HashMap<>();
27-
private Map<String, List<Expr<?>>> varSuperTypes = new HashMap<>();
28-
private Map<String, AliasWrapper> aliasTranslation = new HashMap<>();
29-
private Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
20+
private final com.microsoft.z3.Context z3 = new com.microsoft.z3.Context();
3021

3122
public TranslatorToZ3(liquidjava.processor.context.Context c) {
3223
TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation);
@@ -73,21 +64,6 @@ public Expr<?> makeBooleanLiteral(boolean value) {
7364
return z3.mkBool(value);
7465
}
7566

76-
private Expr<?> getVariableTranslation(String name) throws Exception {
77-
if (!varTranslation.containsKey(name))
78-
throw new NotFoundError("Variable '" + name.toString() + "' not found");
79-
Expr<?> e = varTranslation.get(name);
80-
if (e == null)
81-
e = varTranslation.get(String.format("this#%s", name));
82-
if (e == null)
83-
throw new SyntaxException("Unknown variable:" + name);
84-
return e;
85-
}
86-
87-
public Expr<?> makeVariable(String name) throws Exception {
88-
return getVariableTranslation(name);// int[] not in varTranslation
89-
}
90-
9167
public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exception {
9268
if (name.equals("addToIndex"))
9369
return makeStore(name, params);
@@ -117,14 +93,14 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exce
11793
}
11894

11995
@SuppressWarnings({ "unchecked", "rawtypes" })
120-
private Expr<?> makeSelect(String name, Expr<?>[] params) {
96+
public Expr<?> makeSelect(String name, Expr<?>[] params) {
12197
if (params.length == 2 && params[0] instanceof ArrayExpr)
12298
return z3.mkSelect((ArrayExpr) params[0], params[1]);
12399
return null;
124100
}
125101

126102
@SuppressWarnings({ "unchecked", "rawtypes" })
127-
private Expr<?> makeStore(String name, Expr<?>[] params) {
103+
public Expr<?> makeStore(String name, Expr<?>[] params) {
128104
if (params.length == 3 && params[0] instanceof ArrayExpr)
129105
return z3.mkStore((ArrayExpr) params[0], params[1], params[2]);
130106
return null;
@@ -243,7 +219,7 @@ public Expr<?> makeMod(Expr<?> eval, Expr<?> eval2) {
243219
return z3.mkMod((IntExpr) eval, (IntExpr) eval2);
244220
}
245221

246-
private FPExpr toFP(Expr<?> e) {
222+
public FPExpr toFP(Expr<?> e) {
247223
FPExpr f;
248224
if (e instanceof FPExpr) {
249225
f = (FPExpr) e;
@@ -270,3 +246,125 @@ public Expr<?> makeIte(Expr<?> c, Expr<?> t, Expr<?> e) {
270246
}
271247

272248
}
249+
250+
class TranslatorContextToZ3 {
251+
252+
static void translateVariables(Context z3, Map<String, CtTypeReference<?>> ctx,
253+
Map<String, Expr<?>> varTranslation) {
254+
255+
for (String name : ctx.keySet())
256+
varTranslation.put(name, getExpr(z3, name, ctx.get(name)));
257+
258+
varTranslation.put("true", z3.mkBool(true));
259+
varTranslation.put("false", z3.mkBool(false));
260+
261+
}
262+
263+
public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> variables,
264+
Map<String, List<Expr<?>>> varSuperTypes) {
265+
for (RefinedVariable v : variables) {
266+
if (!v.getSuperTypes().isEmpty()) {
267+
ArrayList<Expr<?>> a = new ArrayList<>();
268+
for (CtTypeReference<?> ctr : v.getSuperTypes())
269+
a.add(getExpr(z3, v.getName(), ctr));
270+
varSuperTypes.put(v.getName(), a);
271+
}
272+
}
273+
274+
}
275+
276+
private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
277+
String typeName = type.getQualifiedName();
278+
if (typeName.contentEquals("int"))
279+
return z3.mkIntConst(name);
280+
else if (typeName.contentEquals("short"))
281+
return z3.mkIntConst(name);
282+
else if (typeName.contentEquals("boolean"))
283+
return z3.mkBoolConst(name);
284+
else if (typeName.contentEquals("long"))
285+
return z3.mkRealConst(name);
286+
else if (typeName.contentEquals("float")) {
287+
return (FPExpr) z3.mkConst(name, z3.mkFPSort64());
288+
} else if (typeName.contentEquals("double")) {
289+
return (FPExpr) z3.mkConst(name, z3.mkFPSort64());
290+
} else if (typeName.contentEquals("int[]")) {
291+
return z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort());
292+
} else {
293+
Sort nSort = z3.mkUninterpretedSort(typeName);
294+
return z3.mkConst(name, nSort);
295+
// System.out.println("Add new type: "+typeName);
296+
}
297+
298+
}
299+
300+
static void addAlias(Context z3, List<AliasWrapper> alias, Map<String, AliasWrapper> aliasTranslation) {
301+
for (AliasWrapper a : alias) {
302+
aliasTranslation.put(a.getName(), a);
303+
}
304+
}
305+
306+
public static void addGhostFunctions(Context z3, List<GhostFunction> ghosts,
307+
Map<String, FuncDecl<?>> funcTranslation) {
308+
addBuiltinFunctions(z3, funcTranslation);
309+
if (!ghosts.isEmpty()) {
310+
for (GhostFunction gh : ghosts) {
311+
addGhostFunction(z3, gh, funcTranslation);
312+
}
313+
}
314+
}
315+
316+
private static void addBuiltinFunctions(Context z3, Map<String, FuncDecl<?>> funcTranslation) {
317+
funcTranslation.put("length", z3.mkFuncDecl("length", getSort(z3, "int[]"), getSort(z3, "int")));// ERRRRRRRRRRRRO!!!!!!!!!!!!!
318+
System.out.println("\nWorks only for int[] now! Change in future. Ignore this message, it is a glorified todo");
319+
// TODO add built-in function
320+
Sort[] s = Stream.of(getSort(z3, "int[]"), getSort(z3, "int"), getSort(z3, "int")).toArray(Sort[]::new);
321+
funcTranslation.put("addToIndex", z3.mkFuncDecl("addToIndex", s, getSort(z3, "void")));
322+
323+
s = Stream.of(getSort(z3, "int[]"), getSort(z3, "int")).toArray(Sort[]::new);
324+
funcTranslation.put("getFromIndex", z3.mkFuncDecl("getFromIndex", s, getSort(z3, "int")));
325+
326+
}
327+
328+
static Sort getSort(Context z3, String sort) {
329+
switch (sort) {
330+
case "int":
331+
return z3.getIntSort();
332+
case "boolean":
333+
return z3.getBoolSort();
334+
case "long":
335+
return z3.getRealSort();
336+
case "float":
337+
return z3.mkFPSort32();
338+
case "double":
339+
return z3.mkFPSortDouble();
340+
case "int[]":
341+
return z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort());
342+
case "String":
343+
return z3.getStringSort();
344+
case "void":
345+
return z3.mkUninterpretedSort("void");
346+
// case "List":return z3.mkListSort(name, elemSort)
347+
default:
348+
return z3.mkUninterpretedSort(sort);
349+
}
350+
}
351+
352+
public static void addGhostStates(Context z3, List<GhostState> ghostState,
353+
Map<String, FuncDecl<?>> funcTranslation) {
354+
for (GhostState g : ghostState) {
355+
addGhostFunction(z3, g, funcTranslation);
356+
// if(g.getRefinement() != null)
357+
// premisesToAdd.add(g.getRefinement().getExpression());
358+
}
359+
360+
}
361+
362+
private static void addGhostFunction(Context z3, GhostFunction gh, Map<String, FuncDecl<?>> funcTranslation) {
363+
List<CtTypeReference<?>> paramTypes = gh.getParametersTypes();
364+
Sort ret = getSort(z3, gh.getReturnType().toString());
365+
Sort[] d = paramTypes.stream().map(t -> t.toString()).map(t -> getSort(z3, t)).toArray(Sort[]::new);
366+
funcTranslation.put(gh.getName(), z3.mkFuncDecl(gh.getName(), d, ret));
367+
}
368+
369+
}
370+

0 commit comments

Comments
 (0)