diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java new file mode 100644 index 00000000..5fb9b97f --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java @@ -0,0 +1,226 @@ +package de.uzl.its.swat.staticcheck; + +import java.util.Objects; +import org.objectweb.asm.tree.analysis.Value; + +/** + * Abstract value of a local variable or operand stack slot for {@link ExceptionFreedomCheck}. + * + *

Every fact is an over-approximation of the concrete values the slot can hold: {@code BOTTOM} + * holds none (not reached yet), {@code NULL} only null, {@code NONNULL} only references, {@code REF} + * references or null, {@code PRIM} a primitive and {@code UNKNOWN} anything. The optional facts + * narrow this further and are dropped (set to null) whenever two values with different facts meet. + */ +final class AbsValue implements Value { + + enum Kind { + BOTTOM, + PRIM, + NULL, + NONNULL, + REF, + UNKNOWN + } + + final Kind kind; + final int size; + /** PRIM: the int or long value, if it is a known constant. */ + final Long constant; + /** NONNULL array: its length, if it is a known constant. */ + final Integer length; + /** + * NONNULL array: its length equals the number of constants of this enum class. PRIM: the value + * is that number. + */ + final String lengthOf; + /** PRIM: the value is the ordinal of a constant of this enum class (0 <= v < its constant count). */ + final String ordinalOf; + /** NONNULL: the runtime class of the object (internal name, or descriptor for arrays). */ + final String exactType; + /** NULL/NONNULL/REF: a type every non-null value is an instance of. */ + final String staticType; + /** The receiver of the current instance method, unchanged since method entry. */ + final boolean isThis; + /** The slot may hold the receiver of the current instance method (a may-alias fact, kept by joins). */ + final boolean mayBeThis; + /** + * The exception caught by the handler with this index in the method's try-catch list (-1: not a + * caught exception, or not known to be one). + */ + final int caughtBy; + + static final AbsValue UNKNOWN1 = new AbsValue(Kind.UNKNOWN, 1, null, null, null, null, null, null, false); + static final AbsValue PRIM1 = prim(1); + static final AbsValue PRIM2 = prim(2); + static final AbsValue NULL = new AbsValue(Kind.NULL, 1, null, null, null, null, null, null, false); + + AbsValue(Kind kind, int size, Long constant, Integer length, String lengthOf, String ordinalOf, + String exactType, String staticType, boolean isThis) { + this(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, -1); + } + + AbsValue(Kind kind, int size, Long constant, Integer length, String lengthOf, String ordinalOf, + String exactType, String staticType, boolean isThis, int caughtBy) { + this(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, caughtBy, isThis); + } + + private AbsValue(Kind kind, int size, Long constant, Integer length, String lengthOf, String ordinalOf, + String exactType, String staticType, boolean isThis, int caughtBy, boolean mayBeThis) { + this.mayBeThis = mayBeThis || isThis; + this.kind = kind; + this.size = size; + this.constant = constant; + this.length = length; + this.lengthOf = lengthOf; + this.ordinalOf = ordinalOf; + this.exactType = exactType; + this.staticType = staticType; + this.isThis = isThis; + this.caughtBy = caughtBy; + } + + static AbsValue prim(int size) { + return new AbsValue(Kind.PRIM, size, null, null, null, null, null, null, false); + } + + static AbsValue constant(int size, long value) { + return new AbsValue(Kind.PRIM, size, value, null, null, null, null, null, false); + } + + static AbsValue bottom(int size) { + return new AbsValue(Kind.BOTTOM, size, null, null, null, null, null, null, false); + } + + static AbsValue ref(String staticType) { + return new AbsValue(Kind.REF, 1, null, null, null, null, null, staticType, false); + } + + static AbsValue nonNull(String staticType) { + return new AbsValue(Kind.NONNULL, 1, null, null, null, null, null, staticType, false); + } + + /** A non-null object whose runtime class is known (a fresh allocation, a String literal, ...). */ + static AbsValue exact(String type) { + return new AbsValue(Kind.NONNULL, 1, null, null, null, null, type, type, false); + } + + static AbsValue array(String type, Integer length, String lengthOf) { + return new AbsValue(Kind.NONNULL, 1, null, length, lengthOf, null, type, type, false); + } + + AbsValue withThis() { + return new AbsValue(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, true); + } + + static AbsValue caught(String type, int handler) { + return new AbsValue(Kind.NONNULL, 1, null, null, null, null, null, type, false, handler); + } + + /** The same value without the facts that only hold where it was computed (receiver, handler). */ + AbsValue escaped() { + if (!mayBeThis && caughtBy < 0) return this; + return new AbsValue(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, false, -1); + } + + AbsValue withOrdinalOf(String enumType) { + return new AbsValue(kind, size, constant, length, lengthOf, enumType, exactType, staticType, isThis, caughtBy, mayBeThis); + } + + AbsValue withLengthOf(String enumType) { + return new AbsValue(kind, size, constant, length, enumType, ordinalOf, exactType, staticType, isThis, caughtBy, mayBeThis); + } + + boolean isBottom() { + return kind == Kind.BOTTOM; + } + + boolean isNull() { + return kind == Kind.NULL; + } + + /** No concrete value of this slot can be null (BOTTOM holds no value at all). */ + boolean isNonNull() { + return kind == Kind.NONNULL || kind == Kind.BOTTOM; + } + + boolean isReference() { + return kind == Kind.NULL || kind == Kind.NONNULL || kind == Kind.REF; + } + + @Override + public int getSize() { + return size; + } + + /** The least upper bound of two values. */ + static AbsValue join(AbsValue a, AbsValue b) { + AbsValue j = joinFacts(a, b); + if ((a.mayBeThis || b.mayBeThis) && !j.mayBeThis) { + j = new AbsValue(j.kind, j.size, j.constant, j.length, j.lengthOf, j.ordinalOf, j.exactType, j.staticType, + j.isThis, j.caughtBy, true); + } + return j; + } + + private static AbsValue joinFacts(AbsValue a, AbsValue b) { + if (a.equals(b)) return a; + if (a.isBottom()) return b; + if (b.isBottom()) return a; + if (a.size != b.size) return UNKNOWN1; + if (a.kind == Kind.PRIM && b.kind == Kind.PRIM) { + return new AbsValue(Kind.PRIM, a.size, same(a.constant, b.constant), null, + same(a.lengthOf, b.lengthOf), same(a.ordinalOf, b.ordinalOf), null, null, false); + } + if (a.isReference() && b.isReference()) { + boolean thisRef = a.isThis && b.isThis; + if (a.kind == Kind.NULL || b.kind == Kind.NULL) { + AbsValue other = a.kind == Kind.NULL ? b : a; + return new AbsValue(other.kind == Kind.NULL ? Kind.NULL : Kind.REF, 1, null, null, null, null, + null, other.staticType, false); + } + if (a.kind == Kind.NONNULL && b.kind == Kind.NONNULL) { + return new AbsValue(Kind.NONNULL, 1, null, same(a.length, b.length), same(a.lengthOf, b.lengthOf), + null, same(a.exactType, b.exactType), same(a.staticType, b.staticType), thisRef, + a.caughtBy == b.caughtBy ? a.caughtBy : -1); + } + return new AbsValue(Kind.REF, 1, null, null, null, null, null, same(a.staticType, b.staticType), false); + } + return a.size == 1 ? UNKNOWN1 : new AbsValue(Kind.UNKNOWN, a.size, null, null, null, null, null, null, false); + } + + private static T same(T a, T b) { + return Objects.equals(a, b) ? a : null; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (!(o instanceof AbsValue)) return false; + AbsValue v = (AbsValue) o; + return kind == v.kind && size == v.size && isThis == v.isThis && mayBeThis == v.mayBeThis && caughtBy == v.caughtBy + && Objects.equals(constant, v.constant) + && Objects.equals(length, v.length) && Objects.equals(lengthOf, v.lengthOf) + && Objects.equals(ordinalOf, v.ordinalOf) && Objects.equals(exactType, v.exactType) + && Objects.equals(staticType, v.staticType); + } + + @Override + public int hashCode() { + return Objects.hash(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, mayBeThis, caughtBy); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(kind.name()); + if (constant != null) sb.append('=').append(constant); + if (length != null) sb.append(" len=").append(length); + if (lengthOf != null) sb.append(" lenOf=").append(lengthOf); + if (ordinalOf != null) sb.append(" ordOf=").append(ordinalOf); + if (exactType != null) sb.append(" exact=").append(exactType); + else if (staticType != null) sb.append(" type=").append(staticType); + if (isThis) sb.append(" this"); + else if (mayBeThis) sb.append(" maybe-this"); + if (caughtBy >= 0) sb.append(" caught#").append(caughtBy); + return sb.toString(); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java new file mode 100644 index 00000000..bf750356 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java @@ -0,0 +1,920 @@ +package de.uzl.its.swat.staticcheck; + +import java.nio.file.Path; +import java.util.*; +import org.objectweb.asm.ConstantDynamic; +import org.objectweb.asm.Handle; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.Type; +import org.objectweb.asm.tree.*; +import org.objectweb.asm.tree.analysis.Analyzer; +import org.objectweb.asm.tree.analysis.AnalyzerException; +import org.objectweb.asm.tree.analysis.Frame; + +/** + * A conservative static check that a program can never end with an uncaught RuntimeException, + * the SV-COMP no-runtime-exception property. If it succeeds, the property holds on every + * execution; if it fails, nothing is known. + * + *

The program is every class on its classpath, entered through {@code Main.main}. The check + * proves that no RuntimeException can escape {@code main} or a static initializer that may run: + * + *

+ * + *

Errors (AssertionError, StackOverflowError, OutOfMemoryError, linkage errors, ...) are not + * RuntimeExceptions and are not considered. Enum classes are assumed to be compiled from Java + * source, so the ordinal of a constant is below the number of constants. + */ +public final class ExceptionFreedomCheck implements FactInterpreter.Facts, Opcodes { + + static final String MAIN_CLASS = "Main"; + static final String MAIN_DESC = "([Ljava/lang/String;)V"; + private static final int MAX_ROUNDS = 100; + + /** + * The outcome: whether the program is proven free of uncaught RuntimeExceptions, whether it is + * proven to never create an AssertionError (so no assert can fail), and why not. + */ + public static final class Result { + public final boolean exceptionFree; + public final String reason; + public final boolean assertionFree; + public final String assertionReason; + + Result(boolean exceptionFree, String reason, boolean assertionFree, String assertionReason) { + this.exceptionFree = exceptionFree; + this.reason = reason; + this.assertionFree = assertionFree; + this.assertionReason = assertionReason; + } + + static Result neither(String reason) { + return new Result(false, reason, false, reason); + } + } + + private final Program program; + private final Map fieldFacts = new HashMap<>(); + private final Map parameterFacts = new HashMap<>(); + private final Map returnFacts = new HashMap<>(); + private final Set initializedBeforeRead = new HashSet<>(); + private final Map[]> frames = new HashMap<>(); + private final Map targetCache = new IdentityHashMap<>(); + private final Set unknownTargets = Collections.newSetFromMap(new IdentityHashMap<>()); + private Program.Method entry; + private boolean changed; + + ExceptionFreedomCheck(Program program) { + this.program = program; + } + + public static Result check(List classpath) { + try { + return new ExceptionFreedomCheck(new Program(classpath)).run(); + } catch (Exception | StackOverflowError e) { + return Result.neither("analysis failed: " + e); + } + } + + Result run() throws AnalyzerException { + if (program.unsupportedClasspath() != null) return Result.neither(program.unsupportedClasspath()); + entry = program.method(MAIN_CLASS, "main", MAIN_DESC); + if (entry == null || !entry.isStatic() || !entry.hasCode()) return Result.neither("no Main.main"); + + computeInitializedBeforeRead(); + for (ClassNode c : program.appClasses()) { + for (FieldNode f : c.fields) { + String key = c.name + "." + f.name + ":" + f.desc; + Type t = Type.getType(f.desc); + if (t.getSort() != Type.OBJECT && t.getSort() != Type.ARRAY) { + fieldFacts.put(key, AbsValue.prim(t.getSize())); + continue; + } + // The JVM only applies a ConstantValue attribute to static fields. + if (f.value instanceof String && (f.access & ACC_STATIC) != 0) fieldFacts.put(key, AbsValue.exact("java/lang/String")); + else if (!initializedBeforeRead.contains(key)) fieldFacts.put(key, AbsValue.NULL); + } + } + + // Facts: least fixpoint, from "no value" upwards. + int round = 0; + do { + if (++round > MAX_ROUNDS) return Result.neither("facts did not converge"); + changed = false; + for (Program.Method m : program.methods()) { + if (!m.hasCode()) continue; + Frame[] f = new Analyzer<>(new FactInterpreter(this, m)).analyze(m.owner.name, m.node); + frames.put(m.key, f); + collectFacts(m, f); + } + } while (changed); + + // May-throw: least fixpoint over the call graph. + Map mayThrow = new LinkedHashMap<>(); + boolean grew; + do { + grew = false; + for (Program.Method m : program.methods()) { + if (!m.hasCode() || mayThrow.containsKey(m.key)) continue; + String reason = escapingException(m, mayThrow); + if (reason != null) { + mayThrow.put(m.key, reason); + grew = true; + } + } + } while (grew); + + List roots = new ArrayList<>(); + roots.add(entry); + roots.addAll(initializers(MAIN_CLASS)); + for (ClassNode c : program.appClasses()) { + // The finalizer thread may run it on any unreachable object, even one whose constructor + // threw before it assigned its fields. + Program.Method fin = program.method(c.name, "finalize", "()V"); + if (fin != null && !fin.isStatic()) return Result.neither("finalizer " + fin.key); + } + Set reachable = new LinkedHashSet<>(); + String open = openWorldCall(roots, reachable); + if (open != null) return Result.neither(open); + String assertion = assertionCreation(reachable); + boolean assertionFree = assertion == null; + if (assertionFree) assertion = "no AssertionError is created in code reachable from Main.main or a static initializer"; + // Main.main and every static initializer that may run (an exception escaping one surfaces + // as an ExceptionInInitializerError, but is still counted). + List mustNotThrow = new ArrayList<>(); + mustNotThrow.add(entry); + for (Program.Method m : reachable) if (m.node.name.equals("")) mustNotThrow.add(m); + for (Program.Method r : mustNotThrow) { + if (mayThrow.containsKey(r.key)) return new Result(false, explain(r.key, mayThrow), assertionFree, assertion); + } + return new Result(true, "no instruction reachable from Main.main or a static initializer can throw an uncaught RuntimeException", + assertionFree, assertion); + } + + /** + * Where reachable code may create an AssertionError (null if nowhere). With a closed world, + * only application code creates objects of application classes or of AssertionError: the + * modelled library methods create none, and no assert of the JDK is enabled. + */ + private String assertionCreation(Set reachable) { + for (Program.Method m : reachable) { + Frame[] f = frames.get(m.key); + AbstractInsnNode[] insns = m.node.instructions.toArray(); + for (int i = 0; i < insns.length; i++) { + if (f[i] == null) continue; + String type = null; + if (insns[i].getOpcode() == NEW) type = ((TypeInsnNode) insns[i]).desc; + else if (insns[i].getOpcode() == INVOKESPECIAL && ((MethodInsnNode) insns[i]).name.equals("")) + type = ((MethodInsnNode) insns[i]).owner; + if (type != null && program.isAssignable(type, "java/lang/AssertionError")) + return m.key + ": line " + line(insns[i]) + ": creates " + type; + } + } + return null; + } + + /** + * The analysis assumes a closed world: application code only runs when application code calls + * it, with arguments the facts account for. A reachable call that may run unknown code (an + * unmodelled library method, which could call back into the application) breaks that even if a + * handler catches what it throws, so it fails the check. Returns why, or null, and collects the + * reachable methods, including the static initializers of every class reachable code may + * initialize (new, getstatic, putstatic, invokestatic). Classes are initialized in no other way: + * reflection and method handles are not modelled. + */ + private String openWorldCall(List roots, Set reachable) { + Deque work = new ArrayDeque<>(roots); + while (!work.isEmpty()) { + Program.Method m = work.poll(); + if (!reachable.add(m)) continue; + Frame[] f = frames.get(m.key); + if (f == null) return "reachable method without code: " + m.key; + AbstractInsnNode[] insns = m.node.instructions.toArray(); + for (int i = 0; i < insns.length; i++) { + if (f[i] == null) continue; + if (insns[i] instanceof InvokeDynamicInsnNode && !isStringConcat((InvokeDynamicInsnNode) insns[i])) + return m.key + ": line " + line(insns[i]) + ": invokedynamic"; + if (insns[i] instanceof LdcInsnNode && (((LdcInsnNode) insns[i]).cst instanceof Handle + || ((LdcInsnNode) insns[i]).cst instanceof ConstantDynamic)) + return m.key + ": line " + line(insns[i]) + ": ldc of a method handle or dynamic constant"; + int op = insns[i].getOpcode(); + if (op == NEW) work.addAll(initializers(((TypeInsnNode) insns[i]).desc)); + else if (op == GETSTATIC || op == PUTSTATIC) work.addAll(initializers(((FieldInsnNode) insns[i]).owner)); + else if (op == INVOKESTATIC) work.addAll(initializers(((MethodInsnNode) insns[i]).owner)); + if (!(insns[i] instanceof MethodInsnNode)) continue; + MethodInsnNode mi = (MethodInsnNode) insns[i]; + String reason = openWorldReason(mi, f[i]); + if (reason != null) return m.key + ": line " + line(mi) + ": " + reason; + Program.Targets t = mi.owner.startsWith(Program.VERIFIER_PACKAGE) ? null : targets(mi); + if (t != null) work.addAll(t.methods); + } + } + return null; + } + + /** + * The static initializers that may run when a class is initialized: its own and those of its + * application supertypes (a superset of what the JVM initializes, see JVMS 5.5). + */ + private List initializers(String className) { + List out = new ArrayList<>(); + if (!program.isApp(className)) return out; + for (String t : program.appSupertypes(className)) { + Program.Method clinit = program.method(t, "", "()V"); + if (clinit != null) out.add(clinit); + } + return out; + } + + /** Follows the may-throw reasons from a root down to the instruction that may throw. */ + private static String explain(String key, Map mayThrow) { + StringBuilder sb = new StringBuilder(); + Set seen = new HashSet<>(); + String k = key; + while (k != null && seen.add(k)) { + String reason = mayThrow.get(k); + if (sb.length() > 0) sb.append(" <- "); + sb.append(k).append(": ").append(reason); + k = null; + int i = reason.indexOf("call to "); + if (i >= 0) { + String callee = reason.substring(i + "call to ".length()); + if (mayThrow.containsKey(callee)) k = callee; + } + } + return sb.toString(); + } + + // --------------------------------------------------------------------------------------------- + // Facts + + private void joinInto(Map map, String key, AbsValue v) { + v = v.escaped(); + AbsValue old = map.get(key); + AbsValue joined = old == null ? v : AbsValue.join(old, v); + if (!joined.equals(old)) { + map.put(key, joined); + changed = true; + } + } + + private void collectFacts(Program.Method m, Frame[] f) { + AbstractInsnNode[] insns = m.node.instructions.toArray(); + for (int i = 0; i < insns.length; i++) { + Frame fr = f[i]; + if (fr == null) continue; + AbstractInsnNode insn = insns[i]; + int op = insn.getOpcode(); + if (op == PUTFIELD || op == PUTSTATIC) { + FieldInsnNode fi = (FieldInsnNode) insn; + String key = fieldKey(fi); + if (key != null && isReferenceDesc(fi.desc)) joinInto(fieldFacts, key, top(fr, 0)); + } else if (op == ARETURN) { + joinInto(returnFacts, m.key, top(fr, 0)); + } else if (op >= IRETURN && op <= DRETURN) { + joinInto(returnFacts, m.key, top(fr, 0)); + } else if (insn instanceof MethodInsnNode) { + MethodInsnNode mi = (MethodInsnNode) insn; + Program.Targets t = targets(mi); + if (t == null) continue; + Type[] args = Type.getArgumentTypes(mi.desc); + for (Program.Method target : t.methods) { + AbsValue[] params = parameterFacts.computeIfAbsent(target.key, k -> new AbsValue[args.length]); + for (int a = 0; a < args.length; a++) { + AbsValue v = top(fr, args.length - 1 - a).escaped(); + AbsValue joined = params[a] == null ? v : AbsValue.join(params[a], v); + if (!joined.equals(params[a])) { + params[a] = joined; + changed = true; + } + } + } + } + } + } + + private static boolean isReferenceDesc(String desc) { + return desc.startsWith("L") || desc.startsWith("["); + } + + private static AbsValue top(Frame f, int depth) { + return f.getStack(f.getStackSize() - 1 - depth); + } + + /** The key of the application field a field instruction accesses, or null for a library field. */ + private String fieldKey(FieldInsnNode fi) { + String[] decl = new String[1]; + FieldNode f = program.resolveField(fi.owner, fi.name, fi.desc, decl); + return f == null ? null : decl[0] + "." + f.name + ":" + f.desc; + } + + @Override + public AbsValue field(FieldInsnNode insn) { + if (insn.getOpcode() == GETSTATIC && insn.owner.equals("java/lang/System") + && (insn.name.equals("out") || insn.name.equals("err")) && insn.desc.equals("Ljava/io/PrintStream;")) { + // Non-null, and exactly a PrintStream: System.setOut/setErr are not modelled, so no + // program that passes the check can replace them. + return AbsValue.exact("java/io/PrintStream"); + } + String key = fieldKey(insn); + if (key == null) return FactInterpreter.ofType(Type.getType(insn.desc)); + AbsValue v = fieldFacts.get(key); + if (v == null) return AbsValue.bottom(Type.getType(insn.desc).getSize()); + return v; + } + + @Override + public AbsValue parameter(Program.Method method, int index, Type type) { + AbsValue[] params = parameterFacts.get(method.key); + if (method == entry) { + // The launcher passes a non-null array; the program may call main itself as well. + AbsValue launcher = AbsValue.array(MAIN_DESC.substring(1, MAIN_DESC.indexOf(')')), null, null); + return params == null || params[index] == null ? launcher : AbsValue.join(launcher, params[index]); + } + if (params == null || params[index] == null) return AbsValue.bottom(type.getSize()); + return params[index]; + } + + @Override + public AbsValue callResult(MethodInsnNode insn, List args) { + Type ret = Type.getReturnType(insn.desc); + if (ret.getSort() == Type.VOID) return null; + if (insn.owner.startsWith(Program.VERIFIER_PACKAGE)) { + if (insn.name.equals("nondetString")) return AbsValue.exact("java/lang/String"); + return FactInterpreter.ofType(ret); + } + if (insn.getOpcode() == INVOKESTATIC && insn.name.equals("values") && program.isEnum(insn.owner) + && insn.desc.equals("()[L" + insn.owner + ";")) { + return AbsValue.array("[L" + insn.owner + ";", null, insn.owner); + } + if (insn.name.equals("ordinal") && insn.desc.equals("()I") && insn.getOpcode() != INVOKESTATIC) { + return program.isEnum(insn.owner) ? AbsValue.PRIM1.withOrdinalOf(insn.owner) : AbsValue.PRIM1; + } + Program.Targets t = targets(insn); + if (t == null) return FactInterpreter.ofType(ret); + AbsValue result = null; + for (Program.Method m : t.methods) { + AbsValue r = returnFacts.get(m.key); + if (r == null) r = AbsValue.bottom(ret.getSize()); + result = result == null ? r : AbsValue.join(result, r); + } + for (String lib : t.libraryMethods) { + AbsValue r = libraryResult(lib, ret, args); + result = result == null ? r : AbsValue.join(result, r); + } + return result == null ? FactInterpreter.ofType(ret) : result; + } + + private static AbsValue libraryResult(String lib, Type ret, List args) { + String[] parts = splitMethod(lib); + JdkModel.Entry e = JdkModel.lookup(parts[0], parts[1], parts[2]); + if (e == null) return FactInterpreter.ofType(ret); + switch (e.returns) { + case NONNULL_EXACT: + return AbsValue.exact(ret.getInternalName()); + case RECEIVER: + return args.get(0).escaped(); + case CLONE: { + AbsValue r = args.get(0); + return new AbsValue(AbsValue.Kind.NONNULL, 1, null, r.length, r.lengthOf, null, r.exactType, + r.exactType != null ? r.exactType : r.staticType, false); + } + default: + return FactInterpreter.ofType(ret); + } + } + + /** owner, name and descriptor of "owner.name(desc)". */ + static String[] splitMethod(String key) { + int paren = key.indexOf('('); + int dot = key.lastIndexOf('.', paren); + return new String[] {key.substring(0, dot), key.substring(dot + 1, paren), key.substring(paren)}; + } + + /** The possible targets of a call, or null if they cannot be determined. Not for Verifier calls. */ + private Program.Targets targets(MethodInsnNode mi) { + if (unknownTargets.contains(mi)) return null; + Program.Targets cached = targetCache.get(mi); + if (cached != null) return cached; + Program.Targets t = computeTargets(mi); + if (t == null) unknownTargets.add(mi); + else targetCache.put(mi, t); + return t; + } + + private Program.Targets computeTargets(MethodInsnNode mi) { + if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) return new Program.Targets(); + int op = mi.getOpcode(); + if ((op == INVOKEVIRTUAL || op == INVOKEINTERFACE) && program.isApp(mi.owner)) { + return program.virtualTargets(mi.owner, mi.name, mi.desc); + } + Program.Targets t = new Program.Targets(); + if (op == INVOKEVIRTUAL || op == INVOKEINTERFACE) { + t.libraryMethods.add(mi.owner + "." + mi.name + mi.desc); + return t; + } + if (op == INVOKESPECIAL && mi.name.equals("")) { + Program.Method m = program.method(mi.owner, mi.name, mi.desc); + if (m != null) t.methods.add(m); + else if (program.isApp(mi.owner)) return null; + else t.libraryMethods.add(mi.owner + "." + mi.name + mi.desc); + return t; + } + String[] lib = new String[1]; + Program.Method m = program.resolveInChain(mi.owner, mi.name, mi.desc, lib); + if (m != null) { + if (!m.hasCode()) return null; + t.methods.add(m); + } else if (lib[0] != null) { + t.libraryMethods.add(lib[0] + "." + mi.name + mi.desc); + } else { + return null; + } + return t; + } + + // --------------------------------------------------------------------------------------------- + // Fields initialized before any read + + /** + * Finds the reference fields that hold a value from their first assignment on, before any code + * that could read them runs. Such a field never shows its default null, so its fact is the join + * of the values stored into it only. + * + *

A static field qualifies if its class initializer assigns it in its straight-line prefix + * (no jumps and no exception handlers), and nothing that prefix may execute (the methods it calls + * and the static initializers of the classes it, its callees or the superclasses touch, all + * transitively) reads a field of that name. An instance field qualifies if every constructor of + * its class assigns it on the receiver in such a prefix, which neither lets the receiver escape + * nor may execute a read of the field. An object is only reachable through the receiver of its + * constructor until it escapes, so no read can come from elsewhere; a constructor that throws + * before the assignment leaves no reference to its object behind. + */ + private void computeInitializedBeforeRead() throws AnalyzerException { + for (ClassNode c : program.appClasses()) { + for (FieldNode f : c.fields) { + if (!isReferenceDesc(f.desc)) continue; + String key = c.name + "." + f.name + ":" + f.desc; + boolean isStatic = (f.access & ACC_STATIC) != 0; + if (isStatic ? staticFieldInitializedFirst(c, f) : instanceFieldInitializedFirst(c, f)) { + initializedBeforeRead.add(key); + } + } + } + } + + /** The instructions every execution of the method runs first, in order, up to the first jump. */ + private static List straightLinePrefix(MethodNode m) { + List out = new ArrayList<>(); + for (AbstractInsnNode insn = m.instructions.getFirst(); insn != null; insn = insn.getNext()) { + if (insn.getOpcode() < 0) continue; // labels, line numbers, frames + int op = insn.getOpcode(); + if (insn instanceof JumpInsnNode || insn instanceof TableSwitchInsnNode || insn instanceof LookupSwitchInsnNode + || op == ATHROW || op == RET || (op >= IRETURN && op <= RETURN)) break; + out.add(insn); + } + return out; + } + + private static boolean coveredByHandler(MethodNode m, AbstractInsnNode insn) { + int idx = m.instructions.indexOf(insn); + for (TryCatchBlockNode tcb : m.tryCatchBlocks) { + if (m.instructions.indexOf(tcb.start) <= idx && idx < m.instructions.indexOf(tcb.end)) return true; + } + return false; + } + + private boolean staticFieldInitializedFirst(ClassNode c, FieldNode f) { + Program.Method clinit = program.method(c.name, "", "()V"); + if (clinit == null) return false; + List before = new ArrayList<>(); + for (AbstractInsnNode insn : straightLinePrefix(clinit.node)) { + if (coveredByHandler(clinit.node, insn)) return false; + if (insn.getOpcode() == PUTSTATIC && assigns((FieldInsnNode) insn, c, f)) { + // The supertypes are initialized before the class; the class itself is being + // initialized already, so touching it again does not rerun its initializer. + Set supertypes = new HashSet<>(program.appSupertypes(c.name)); + supertypes.remove(c.name); + return !mayRead(before, supertypes, Set.of(c.name), f.name, f.desc, true); + } + before.add(insn); + } + return false; + } + + private boolean instanceFieldInitializedFirst(ClassNode c, FieldNode f) throws AnalyzerException { + boolean any = false; + for (MethodNode mn : c.methods) { + if (!mn.name.equals("")) continue; + any = true; + Program.Method ctor = program.method(c.name, mn.name, mn.desc); + Frame[] fr = new Analyzer<>(new FactInterpreter(UNKNOWN_FACTS, ctor)).analyze(c.name, mn); + List before = new ArrayList<>(); + boolean assigned = false; + for (AbstractInsnNode insn : straightLinePrefix(mn)) { + if (coveredByHandler(mn, insn)) return false; + Frame frame = fr[mn.instructions.indexOf(insn)]; + if (frame == null) return false; + if (insn.getOpcode() == PUTFIELD && assigns((FieldInsnNode) insn, c, f) && top(frame, 1).isThis + && !top(frame, 0).mayBeThis) { + assigned = true; + break; + } + if (letsReceiverEscape(insn, frame, new HashSet<>())) return false; + before.add(insn); + } + if (!assigned || mayRead(before, Set.of(), Set.of(), f.name, f.desc, false)) return false; + } + return any; + } + + private boolean assigns(FieldInsnNode fi, ClassNode c, FieldNode f) { + String[] decl = new String[1]; + FieldNode target = program.resolveField(fi.owner, fi.name, fi.desc, decl); + return target == f && c.name.equals(decl[0]); + } + + /** + * Whether the instruction hands the receiver (this) to code that could keep it: as an argument + * or receiver of a call, or as a value stored into a field or an array. The superclass or + * delegated constructor may take it if its own code does not let it escape either. + */ + private boolean letsReceiverEscape(AbstractInsnNode insn, Frame frame, Set checking) { + int op = insn.getOpcode(); + if (op == PUTFIELD || op == PUTSTATIC || op == AASTORE || op == ARETURN || op == ATHROW) { + return top(frame, 0).mayBeThis; + } + if (insn instanceof InvokeDynamicInsnNode) { + int n = Type.getArgumentTypes(((InvokeDynamicInsnNode) insn).desc).length; + for (int i = 0; i < n; i++) if (top(frame, i).mayBeThis) return true; + return false; + } + if (!(insn instanceof MethodInsnNode)) return false; + MethodInsnNode mi = (MethodInsnNode) insn; + int n = Type.getArgumentTypes(mi.desc).length; + for (int i = 0; i < n; i++) if (top(frame, i).mayBeThis) return true; + if (op == INVOKESTATIC || !top(frame, n).mayBeThis) return false; + if (op != INVOKESPECIAL || !mi.name.equals("") || !top(frame, n).isThis) return true; + if (mi.owner.equals("java/lang/Object") && mi.desc.equals("()V")) return false; + if (mi.owner.equals("java/lang/Enum") && mi.desc.equals("(Ljava/lang/String;I)V")) return false; + Program.Method ctor = program.method(mi.owner, mi.name, mi.desc); + if (ctor == null || !ctor.hasCode() || !checking.add(ctor.key)) return true; + try { + Frame[] fr = new Analyzer<>(new FactInterpreter(UNKNOWN_FACTS, ctor)).analyze(ctor.owner.name, ctor.node); + AbstractInsnNode[] insns = ctor.node.instructions.toArray(); + for (int i = 0; i < insns.length; i++) { + if (fr[i] != null && letsReceiverEscape(insns[i], fr[i], checking)) return true; + } + return false; + } catch (AnalyzerException e) { + return true; + } + } + + /** + * Whether running the given instructions may read a field with this name and descriptor: + * directly, in a method they may call (transitively), or in a static initializer they may + * trigger (except those of the classes being initialized already). Unknown callees count as + * reads. + */ + private boolean mayRead(List start, Set initializedClasses, Set initializing, + String name, String desc, boolean isStatic) { + Deque work = new ArrayDeque<>(); + Set seen = new HashSet<>(); + Set classes = new HashSet<>(initializing); + Deque pendingClasses = new ArrayDeque<>(initializedClasses); + List insns = new ArrayList<>(start); + while (true) { + for (AbstractInsnNode insn : insns) { + int op = insn.getOpcode(); + if (insn instanceof FieldInsnNode) { + FieldInsnNode fi = (FieldInsnNode) insn; + if ((op == (isStatic ? GETSTATIC : GETFIELD)) && fi.name.equals(name) && fi.desc.equals(desc)) return true; + if (op == GETSTATIC || op == PUTSTATIC) pendingClasses.add(fi.owner); + } else if (op == NEW) { + pendingClasses.add(((TypeInsnNode) insn).desc); + } else if (insn instanceof InvokeDynamicInsnNode) { + if (!isStringConcat((InvokeDynamicInsnNode) insn)) return true; + } else if (insn instanceof MethodInsnNode) { + MethodInsnNode mi = (MethodInsnNode) insn; + if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) { + if (!isModelledVerifierCall(mi)) return true; + continue; + } + if (op == INVOKESTATIC) pendingClasses.add(mi.owner); + Program.Targets t = targets(mi); + if (t == null) return true; + for (String lib : t.libraryMethods) { + String[] p = splitMethod(lib); + JdkModel.Entry e = JdkModel.lookup(p[0], p[1], p[2]); + // Without values, a library call is only known not to call back if its model + // has no argument condition about callbacks and no override can intervene. + if (e == null || e.condition == JdkModel.Condition.STRING_ARGS) return true; + if (op != INVOKESTATIC && !program.isApp(mi.owner) && !JdkModel.cannotBeOverridden(p[0], p[1], p[2]) + && !e.exactReceiver) return true; + } + for (Program.Method m : t.methods) if (seen.add(m.key)) work.add(m); + } + } + while (!pendingClasses.isEmpty()) { + String cls = pendingClasses.poll(); + if (cls.startsWith("[") || !program.isApp(cls)) continue; + for (String sup : program.appSupertypes(cls)) { + if (!classes.add(sup)) continue; + Program.Method clinit = program.method(sup, "", "()V"); + if (clinit != null && seen.add(clinit.key)) work.add(clinit); + } + } + if (work.isEmpty()) return false; + Program.Method m = work.poll(); + insns = new ArrayList<>(); + if (!m.hasCode()) return true; + for (AbstractInsnNode insn : m.node.instructions) insns.add(insn); + } + } + + /** Facts for analyses that only need the receiver flag: nothing is known about other values. */ + private static final FactInterpreter.Facts UNKNOWN_FACTS = new FactInterpreter.Facts() { + @Override + public AbsValue field(FieldInsnNode insn) { + return FactInterpreter.ofType(Type.getType(insn.desc)); + } + + @Override + public AbsValue parameter(Program.Method method, int index, Type type) { + return FactInterpreter.ofType(type); + } + + @Override + public AbsValue callResult(MethodInsnNode insn, List args) { + return FactInterpreter.ofType(Type.getReturnType(insn.desc)); + } + }; + + // --------------------------------------------------------------------------------------------- + // Checking instructions + + static boolean isStringConcat(InvokeDynamicInsnNode indy) { + if (!indy.bsm.getOwner().equals("java/lang/invoke/StringConcatFactory")) return false; + for (Type t : Type.getArgumentTypes(indy.desc)) { + if (t.getSort() == Type.OBJECT && !t.getInternalName().equals("java/lang/String")) return false; + if (t.getSort() == Type.ARRAY) return false; + } + return true; + } + + private static boolean isModelledVerifierCall(MethodInsnNode mi) { + return mi.owner.equals(Program.VERIFIER_PACKAGE + "Verifier") && mi.getOpcode() == INVOKESTATIC + && (mi.name.equals("assume") || (mi.name.startsWith("nondet") && !mi.name.equals("nondetObject"))); + } + + /** + * Why a RuntimeException may escape the method, or null if none can, given the methods already + * known to let one escape. + */ + private String escapingException(Program.Method m, Map mayThrow) { + Frame[] f = frames.get(m.key); + MethodNode mn = m.node; + AbstractInsnNode[] insns = mn.instructions.toArray(); + int n = insns.length; + List handlers = mn.tryCatchBlocks; + boolean[][] covers = new boolean[handlers.size()][n]; + for (int h = 0; h < handlers.size(); h++) { + TryCatchBlockNode tcb = handlers.get(h); + int s = mn.instructions.indexOf(tcb.start), e = mn.instructions.indexOf(tcb.end); + for (int i = s; i < e; i++) covers[h][i] = true; + } + // An instruction may raise a RuntimeException; handlers that may catch one. Rethrowing a + // caught exception raises one only if its handler may have caught one: iterate. + String[] raises = new String[n]; + boolean[] handlerCatches = new boolean[handlers.size()]; + boolean grew = true; + while (grew) { + grew = false; + for (int i = 0; i < n; i++) { + if (f[i] == null || raises[i] != null) continue; + String r = raises(m, insns[i], f[i], mayThrow, handlerCatches); + if (r == null) continue; + raises[i] = r; + grew = true; + // Over-approximated: every handler that covers it may have caught it. + for (int h = 0; h < handlers.size(); h++) if (covers[h][i]) handlerCatches[h] = true; + } + } + for (int i = 0; i < n; i++) { + if (raises[i] == null) continue; + boolean caught = false; + for (int h = 0; h < handlers.size() && !caught; h++) { + caught = covers[h][i] && catchesEveryRuntimeException(handlers.get(h).type, insns[i]); + } + if (!caught) return "line " + line(insns[i]) + ": " + raises[i]; + } + return null; + } + + private static int line(AbstractInsnNode insn) { + for (AbstractInsnNode p = insn; p != null; p = p.getPrevious()) { + if (p instanceof LineNumberNode) return ((LineNumberNode) p).line; + } + return -1; + } + + private static boolean catchesEveryRuntimeException(String type, AbstractInsnNode insn) { + if (type == null || type.equals("java/lang/Throwable") || type.equals("java/lang/Exception") + || type.equals("java/lang/RuntimeException")) return true; + // Integer division can only throw ArithmeticException. + int op = insn.getOpcode(); + return type.equals("java/lang/ArithmeticException") && (op == IDIV || op == IREM || op == LDIV || op == LREM); + } + + private String raises(Program.Method m, AbstractInsnNode insn, Frame f, Map mayThrow, + boolean[] handlerCatches) { + int op = insn.getOpcode(); + switch (op) { + case IDIV: case IREM: case LDIV: case LREM: { + AbsValue d = top(f, 0); + if (d.isBottom() || (d.constant != null && d.constant != 0)) return null; + return "division by a value that may be zero"; + } + case IALOAD: case LALOAD: case FALOAD: case DALOAD: case BALOAD: case CALOAD: case SALOAD: case AALOAD: + return arrayAccess(top(f, 1), top(f, 0)); + case IASTORE: case LASTORE: case FASTORE: case DASTORE: case BASTORE: case CASTORE: case SASTORE: + return arrayAccess(top(f, 2), top(f, 1)); + case AASTORE: { + String r = arrayAccess(top(f, 2), top(f, 1)); + if (r != null) return r; + AbsValue arr = top(f, 2), v = top(f, 0); + if (v.isNull() || v.isBottom() || arr.isBottom()) return null; + String elem = arr.exactType != null ? arr.exactType.substring(1) : null; + if (elem != null && elem.startsWith("L")) elem = elem.substring(1, elem.length() - 1); + if (elem != null && program.isAssignable(trustedType(v), elem)) return null; + return "array store of a value that may not fit the array"; + } + case ARRAYLENGTH: + return top(f, 0).isNonNull() ? null : "length of an array that may be null"; + case NEWARRAY: case ANEWARRAY: + return nonNegative(top(f, 0)) ? null : "array size may be negative"; + case MULTIANEWARRAY: { + int dims = ((MultiANewArrayInsnNode) insn).dims; + for (int i = 0; i < dims; i++) if (!nonNegative(top(f, i))) return "array size may be negative"; + return null; + } + case GETFIELD: + return top(f, 0).isNonNull() ? null : "field read on a reference that may be null"; + case PUTFIELD: + return top(f, 1).isNonNull() ? null : "field write on a reference that may be null"; + case CHECKCAST: { + AbsValue v = top(f, 0); + if (v.isNull() || v.isBottom() || program.isAssignable(trustedType(v), ((TypeInsnNode) insn).desc)) return null; + return "cast that may fail"; + } + case ATHROW: { + AbsValue v = top(f, 0); + if (v.isBottom()) return null; + if (v.caughtBy >= 0) return handlerCatches[v.caughtBy] ? "rethrow of a caught RuntimeException" : null; + if (v.exactType != null && isNeverRuntimeException(v.exactType)) return null; + return "throw of a value that may be a RuntimeException"; + } + case MONITORENTER: case MONITOREXIT: + return "monitor instruction"; + case INVOKEDYNAMIC: + return isStringConcat((InvokeDynamicInsnNode) insn) ? null : "invokedynamic"; + case INVOKEVIRTUAL: case INVOKESPECIAL: case INVOKESTATIC: case INVOKEINTERFACE: + return call((MethodInsnNode) insn, f, mayThrow); + default: + return null; + } + } + + private String arrayAccess(AbsValue arr, AbsValue idx) { + if (arr.isBottom() || idx.isBottom()) return null; + if (!arr.isNonNull()) return "access to an array that may be null"; + if (arr.length != null && idx.constant != null && idx.constant >= 0 && idx.constant < arr.length) return null; + if (arr.lengthOf != null && arr.lengthOf.equals(idx.ordinalOf)) return null; + return "array index that may be out of bounds"; + } + + private static boolean nonNegative(AbsValue count) { + return count.isBottom() || (count.constant != null && count.constant >= 0) || count.lengthOf != null; + } + + /** A type every non-null value of the slot is an instance of, if one is reliably known. */ + private String trustedType(AbsValue v) { + if (v.exactType != null) return v.exactType; + String t = v.staticType; + if (t == null) return null; + // The verifier does not check interface types, so only class and array types are trusted. + if (t.startsWith("[") || t.equals("java/lang/Object") || JdkModel.isFinalClass(t)) return t; + ClassNode c = program.clazz(t); + if (c != null && program.isApp(t) && (c.access & ACC_INTERFACE) == 0) return t; + return null; + } + + /** The runtime class is a Throwable that is not a RuntimeException. */ + private boolean isNeverRuntimeException(String exactType) { + List chain = program.superChain(exactType); + String root = chain.get(chain.size() - 1); + if (program.isApp(root)) return false; + return root.equals("java/lang/AssertionError") || root.equals("java/lang/Error") + || root.equals("java/lang/Exception") || root.equals("java/lang/Throwable"); + } + + /** + * Why the call may run code the analysis does not know (null if it cannot): an unresolved or + * unmodelled callee, or a library method whose model does not cover this receiver or these + * arguments. + */ + private String openWorldReason(MethodInsnNode mi, Frame f) { + int op = mi.getOpcode(); + if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) { + return isModelledVerifierCall(mi) ? null : "call to " + mi.owner + "." + mi.name; + } + Type[] args = Type.getArgumentTypes(mi.desc); + AbsValue receiver = op == INVOKESTATIC ? null : top(f, args.length); + if (receiver != null && receiver.isBottom()) return null; + Program.Targets t = targets(mi); + if (t == null) return "unresolved call to " + mi.owner + "." + mi.name + mi.desc; + for (String lib : t.libraryMethods) { + String[] p = splitMethod(lib); + JdkModel.Entry e = JdkModel.lookup(p[0], p[1], p[2]); + if (e == null) return "library call to " + lib; + boolean viaLibraryOwner = !program.isApp(mi.owner) && op != INVOKESTATIC && !(op == INVOKESPECIAL && mi.name.equals("")); + boolean exactOwner = receiver != null && p[0].equals(receiver.exactType); + if (viaLibraryOwner && !JdkModel.cannotBeOverridden(p[0], p[1], p[2]) && !exactOwner) + return "library call that an override may intercept: " + lib; + if (e.exactReceiver && !exactOwner) return "library call on a receiver of unknown class: " + lib; + if (e.condition != JdkModel.Condition.STRING_ARGS) continue; + for (int a = 0; a < args.length; a++) { + if (args[a].getSort() != Type.OBJECT && args[a].getSort() != Type.ARRAY) continue; + AbsValue v = top(f, args.length - 1 - a); + if (!v.isNull() && !v.isBottom() + && (trustedType(v) == null || !JdkModel.SAFE_TO_STRING.contains(trustedType(v)))) + return "library call that may call toString() of the argument: " + lib; + } + } + return null; + } + + private String call(MethodInsnNode mi, Frame f, Map mayThrow) { + String open = openWorldReason(mi, f); + if (open != null) return open; + if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) return null; + int op = mi.getOpcode(); + Type[] args = Type.getArgumentTypes(mi.desc); + AbsValue receiver = op == INVOKESTATIC ? null : top(f, args.length); + if (receiver != null && !receiver.isNonNull()) return "call on a reference that may be null: " + mi.owner + "." + mi.name; + if (receiver != null && receiver.isBottom()) return null; + Program.Targets t = targets(mi); + for (String lib : t.libraryMethods) { + String[] p = splitMethod(lib); + JdkModel.Entry e = JdkModel.lookup(p[0], p[1], p[2]); + if (e.condition != JdkModel.Condition.NONNULL_ARGS) continue; + for (int a = 0; a < args.length; a++) { + if (args[a].getSort() != Type.OBJECT && args[a].getSort() != Type.ARRAY) continue; + if (!top(f, args.length - 1 - a).isNonNull()) + return "library call with an argument that may be null: " + lib; + } + } + for (Program.Method target : t.methods) { + if (mayThrow.containsKey(target.key)) return "call to " + target.key; + } + return null; + } + + // --------------------------------------------------------------------------------------------- + + /** + * Command line: the classpath entries of the program. Prints one JSON object with the result. + */ + public static void main(String[] args) { + List cp = new ArrayList<>(); + for (String a : args) for (String p : a.split(java.io.File.pathSeparator)) if (!p.isEmpty()) cp.add(Path.of(p)); + Result r = check(cp); + System.out.println("{\"exception_free\": " + r.exceptionFree + ", \"reason\": \"" + escape(r.reason) + + "\", \"assertion_free\": " + r.assertionFree + ", \"assertion_reason\": \"" + escape(r.assertionReason) + "\"}"); + } + + private static String escape(String s) { + StringBuilder sb = new StringBuilder(); + for (char c : s.toCharArray()) { + if (c == '"' || c == '\\') sb.append('\\').append(c); + else if (c < 0x20) sb.append(String.format("\\u%04x", (int) c)); + else sb.append(c); + } + return sb.toString(); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java new file mode 100644 index 00000000..71fb8bff --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java @@ -0,0 +1,277 @@ +package de.uzl.its.swat.staticcheck; + +import java.util.List; +import org.objectweb.asm.Handle; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.Type; +import org.objectweb.asm.tree.*; +import org.objectweb.asm.tree.analysis.AnalyzerException; +import org.objectweb.asm.tree.analysis.Frame; +import org.objectweb.asm.tree.analysis.Interpreter; + +/** + * Computes {@link AbsValue}s for one method, using the facts the check has collected so far for + * fields, parameters and the results of calls. + */ +final class FactInterpreter extends Interpreter implements Opcodes { + + /** Facts about the rest of the program, as far as they are known. */ + interface Facts { + AbsValue field(FieldInsnNode insn); + + /** The value of parameter number {@code index} (not counting the receiver) of the method. */ + AbsValue parameter(Program.Method method, int index, Type type); + + AbsValue callResult(MethodInsnNode insn, List args); + } + + private final Facts facts; + private final Program.Method method; + private final int[] localToParameter; + + FactInterpreter(Facts facts, Program.Method method) { + super(ASM9); + this.facts = facts; + this.method = method; + Type[] params = Type.getArgumentTypes(method.node.desc); + int locals = method.isStatic() ? 0 : 1; + for (Type t : params) locals += t.getSize(); + localToParameter = new int[locals]; + java.util.Arrays.fill(localToParameter, -1); + int local = method.isStatic() ? 0 : 1; + for (int i = 0; i < params.length; i++) { + localToParameter[local] = i; + local += params[i].getSize(); + } + } + + static AbsValue ofType(Type type) { + if (type == null) return AbsValue.UNKNOWN1; + switch (type.getSort()) { + case Type.VOID: + return null; + case Type.LONG: + case Type.DOUBLE: + return AbsValue.PRIM2; + case Type.OBJECT: + case Type.ARRAY: + return AbsValue.ref(type.getInternalName()); + case Type.METHOD: + return AbsValue.UNKNOWN1; + default: + return AbsValue.PRIM1; + } + } + + @Override + public AbsValue newValue(Type type) { + return ofType(type); + } + + @Override + public AbsValue newParameterValue(boolean isInstanceMethod, int local, Type type) { + if (isInstanceMethod && local == 0) return AbsValue.nonNull(type.getInternalName()).withThis(); + int index = local < localToParameter.length ? localToParameter[local] : -1; + if (index < 0) return ofType(type); + return facts.parameter(method, index, type); + } + + @Override + public AbsValue newEmptyValue(int local) { + return AbsValue.UNKNOWN1; + } + + @Override + public AbsValue newExceptionValue(TryCatchBlockNode tryCatch, Frame handlerFrame, Type exceptionType) { + return AbsValue.caught(exceptionType.getInternalName(), method.node.tryCatchBlocks.indexOf(tryCatch)); + } + + @Override + public AbsValue newOperation(AbstractInsnNode insn) throws AnalyzerException { + switch (insn.getOpcode()) { + case ACONST_NULL: + return AbsValue.NULL; + case ICONST_M1: case ICONST_0: case ICONST_1: case ICONST_2: case ICONST_3: case ICONST_4: case ICONST_5: + return AbsValue.constant(1, insn.getOpcode() - ICONST_0); + case LCONST_0: case LCONST_1: + return AbsValue.constant(2, insn.getOpcode() - LCONST_0); + case FCONST_0: case FCONST_1: case FCONST_2: + return AbsValue.PRIM1; + case DCONST_0: case DCONST_1: + return AbsValue.PRIM2; + case BIPUSH: case SIPUSH: + return AbsValue.constant(1, ((IntInsnNode) insn).operand); + case LDC: { + Object c = ((LdcInsnNode) insn).cst; + if (c instanceof Integer) return AbsValue.constant(1, (Integer) c); + if (c instanceof Long) return AbsValue.constant(2, (Long) c); + if (c instanceof Float) return AbsValue.PRIM1; + if (c instanceof Double) return AbsValue.PRIM2; + if (c instanceof String) return AbsValue.exact("java/lang/String"); + if (c instanceof Type) { + int sort = ((Type) c).getSort(); + if (sort == Type.METHOD) return AbsValue.exact("java/lang/invoke/MethodType"); + return AbsValue.exact("java/lang/Class"); + } + if (c instanceof Handle) return AbsValue.nonNull("java/lang/invoke/MethodHandle"); + return AbsValue.UNKNOWN1; + } + case JSR: + return AbsValue.UNKNOWN1; + case GETSTATIC: + return facts.field((FieldInsnNode) insn); + case NEW: + return AbsValue.exact(((TypeInsnNode) insn).desc); + default: + throw new AnalyzerException(insn, "Unexpected opcode"); + } + } + + @Override + public AbsValue copyOperation(AbstractInsnNode insn, AbsValue value) { + return value; + } + + @Override + public AbsValue unaryOperation(AbstractInsnNode insn, AbsValue value) throws AnalyzerException { + switch (insn.getOpcode()) { + case INEG: + return value.constant != null ? AbsValue.constant(1, (int) -value.constant) : AbsValue.PRIM1; + case IINC: + return value.constant != null + ? AbsValue.constant(1, (int) (value.constant + ((IincInsnNode) insn).incr)) : AbsValue.PRIM1; + case L2I: + return value.constant != null ? AbsValue.constant(1, (int) (long) value.constant) : AbsValue.PRIM1; + case I2L: + return value.constant != null ? AbsValue.constant(2, value.constant) : AbsValue.PRIM2; + case I2B: + return value.constant != null ? AbsValue.constant(1, (byte) (long) value.constant) : AbsValue.PRIM1; + case I2C: + return value.constant != null ? AbsValue.constant(1, (char) (long) value.constant) : AbsValue.PRIM1; + case I2S: + return value.constant != null ? AbsValue.constant(1, (short) (long) value.constant) : AbsValue.PRIM1; + case LNEG: + return value.constant != null ? AbsValue.constant(2, -value.constant) : AbsValue.PRIM2; + case FNEG: case I2F: case L2F: case D2F: case F2I: case D2I: + return AbsValue.PRIM1; + case DNEG: case I2D: case L2D: case F2D: case F2L: case D2L: + return AbsValue.PRIM2; + case IFEQ: case IFNE: case IFLT: case IFGE: case IFGT: case IFLE: + case TABLESWITCH: case LOOKUPSWITCH: + case IRETURN: case LRETURN: case FRETURN: case DRETURN: case ARETURN: + case PUTSTATIC: case ATHROW: case MONITORENTER: case MONITOREXIT: case IFNULL: case IFNONNULL: + return null; + case GETFIELD: + return facts.field((FieldInsnNode) insn); + case NEWARRAY: { + String desc = "[" + primitiveDescriptor(((IntInsnNode) insn).operand); + return AbsValue.array(desc, nonNegative(value), value.lengthOf); + } + case ANEWARRAY: { + String elem = ((TypeInsnNode) insn).desc; + String desc = "[" + (elem.startsWith("[") ? elem : "L" + elem + ";"); + return AbsValue.array(desc, nonNegative(value), value.lengthOf); + } + case ARRAYLENGTH: { + AbsValue len = value.length != null ? AbsValue.constant(1, value.length) : AbsValue.PRIM1; + return value.lengthOf != null ? len.withLengthOf(value.lengthOf) : len; + } + case CHECKCAST: + return value; + case INSTANCEOF: + return AbsValue.PRIM1; + default: + throw new AnalyzerException(insn, "Unexpected opcode"); + } + } + + private static Integer nonNegative(AbsValue count) { + if (count.constant == null || count.constant < 0 || count.constant > Integer.MAX_VALUE) return null; + return (int) (long) count.constant; + } + + static String primitiveDescriptor(int operand) { + switch (operand) { + case T_BOOLEAN: return "Z"; + case T_CHAR: return "C"; + case T_BYTE: return "B"; + case T_SHORT: return "S"; + case T_INT: return "I"; + case T_FLOAT: return "F"; + case T_DOUBLE: return "D"; + case T_LONG: return "J"; + default: return "?"; + } + } + + @Override + public AbsValue binaryOperation(AbstractInsnNode insn, AbsValue v1, AbsValue v2) throws AnalyzerException { + int op = insn.getOpcode(); + switch (op) { + case IALOAD: case BALOAD: case CALOAD: case SALOAD: case FALOAD: + return AbsValue.PRIM1; + case LALOAD: case DALOAD: + return AbsValue.PRIM2; + case AALOAD: { + String t = v1.staticType; + if (t != null && t.startsWith("[")) return AbsValue.ref(Type.getType(t.substring(1)).getInternalName()); + return AbsValue.ref(null); + } + case IADD: case ISUB: case IMUL: case ISHL: case ISHR: case IUSHR: case IAND: case IOR: case IXOR: + if (v1.constant != null && v2.constant != null) { + int a = (int) (long) v1.constant, b = (int) (long) v2.constant; + switch (op) { + case IADD: return AbsValue.constant(1, a + b); + case ISUB: return AbsValue.constant(1, a - b); + case IMUL: return AbsValue.constant(1, a * b); + case ISHL: return AbsValue.constant(1, a << b); + case ISHR: return AbsValue.constant(1, a >> b); + case IUSHR: return AbsValue.constant(1, a >>> b); + case IAND: return AbsValue.constant(1, a & b); + case IOR: return AbsValue.constant(1, a | b); + default: return AbsValue.constant(1, a ^ b); + } + } + return AbsValue.PRIM1; + case IDIV: case IREM: case FADD: case FSUB: case FMUL: case FDIV: case FREM: + case LCMP: case FCMPL: case FCMPG: case DCMPL: case DCMPG: + return AbsValue.PRIM1; + case LADD: case LSUB: case LMUL: case LDIV: case LREM: case LSHL: case LSHR: case LUSHR: + case LAND: case LOR: case LXOR: case DADD: case DSUB: case DMUL: case DDIV: case DREM: + return AbsValue.PRIM2; + case IF_ICMPEQ: case IF_ICMPNE: case IF_ICMPLT: case IF_ICMPGE: case IF_ICMPGT: case IF_ICMPLE: + case IF_ACMPEQ: case IF_ACMPNE: case PUTFIELD: + return null; + default: + throw new AnalyzerException(insn, "Unexpected opcode"); + } + } + + @Override + public AbsValue ternaryOperation(AbstractInsnNode insn, AbsValue v1, AbsValue v2, AbsValue v3) { + return null; + } + + @Override + public AbsValue naryOperation(AbstractInsnNode insn, List values) { + int op = insn.getOpcode(); + if (op == MULTIANEWARRAY) { + String desc = ((MultiANewArrayInsnNode) insn).desc; + return AbsValue.array(desc, nonNegative(values.get(0)), values.get(0).lengthOf); + } + if (op == INVOKEDYNAMIC) { + InvokeDynamicInsnNode indy = (InvokeDynamicInsnNode) insn; + if (ExceptionFreedomCheck.isStringConcat(indy)) return AbsValue.exact("java/lang/String"); + return ofType(Type.getReturnType(indy.desc)); + } + return facts.callResult((MethodInsnNode) insn, values); + } + + @Override + public void returnOperation(AbstractInsnNode insn, AbsValue value, AbsValue expected) {} + + @Override + public AbsValue merge(AbsValue a, AbsValue b) { + return AbsValue.join(a, b); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java new file mode 100644 index 00000000..79f64a51 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java @@ -0,0 +1,281 @@ +package de.uzl.its.swat.staticcheck; + +import java.util.*; + +/** + * The library (JDK) methods {@link ExceptionFreedomCheck} lets a program call. + * + *

Every method listed here throws no RuntimeException for any arguments that meet its + * condition, and never calls back into application code: it calls no method of an argument or + * receiver that an application class could override. A call to any other library method fails the + * check. Entries are matched by owner, name and descriptor as written in the call instruction. + */ +final class JdkModel { + + enum Condition { + NONE, + /** Every reference argument is non-null. */ + NONNULL_ARGS, + /** + * Every reference argument is null or of a final library type whose toString() is one of the + * listed safe methods (the method converts its argument with String.valueOf). + */ + STRING_ARGS + } + + enum Returns { + /** Nothing known beyond the declared return type. */ + DECLARED, + /** A non-null object of exactly the declared return type. */ + NONNULL_EXACT, + /** The receiver (StringBuilder.append). */ + RECEIVER, + /** A copy of the receiver array (same runtime type and length). */ + CLONE + } + + static final class Entry { + final Condition condition; + final Returns returns; + /** The receiver must be exactly of the owner class: subclasses could override the method. */ + final boolean exactReceiver; + + Entry(Condition condition, Returns returns, boolean exactReceiver) { + this.condition = condition; + this.returns = returns; + this.exactReceiver = exactReceiver; + } + } + + /** Final classes: no subclass can override their methods. */ + private static final Set FINAL_CLASSES = Set.of( + "java/lang/String", "java/lang/StringBuilder", "java/lang/StringBuffer", "java/lang/Integer", + "java/lang/Long", "java/lang/Short", "java/lang/Byte", "java/lang/Character", "java/lang/Boolean", + "java/lang/Double", "java/lang/Float", "java/lang/Math", "java/lang/StrictMath", "java/lang/System", + "java/lang/Class"); + + /** Library types whose toString() neither throws nor calls application code. */ + static final Set SAFE_TO_STRING = Set.of( + "java/lang/String", "java/lang/Integer", "java/lang/Long", "java/lang/Short", "java/lang/Byte", + "java/lang/Character", "java/lang/Boolean", "java/lang/Double", "java/lang/Float", + "java/lang/StringBuilder", "java/lang/StringBuffer"); + + /** Math/StrictMath methods that never throw, for every overload. */ + private static final Set MATH = Set.of( + "abs", "max", "min", "sqrt", "cbrt", "pow", "exp", "expm1", "log", "log10", "log1p", "sin", "cos", + "tan", "asin", "acos", "atan", "atan2", "sinh", "cosh", "tanh", "hypot", "ceil", "floor", "rint", + "round", "signum", "toRadians", "toDegrees", "ulp", "copySign", "getExponent", "nextUp", "nextDown", + "nextAfter", "scalb", "IEEEremainder", "random", "fma"); + + private static final Map ENTRIES = new HashMap<>(); + + /** Methods declared by java/lang/Object and java/lang/Enum, the library superclasses we know. */ + private static final Map> DECLARED = new HashMap<>(); + + /** Known library supertypes, for assignability. */ + private static final Map> SUPERTYPES = new HashMap<>(); + + private static void add(String owner, Condition c, Returns r, String... methods) { + for (String m : methods) ENTRIES.put(owner + "." + m, new Entry(c, r, false)); + } + + private static void addExact(String owner, Condition c, Returns r, String... methods) { + for (String m : methods) ENTRIES.put(owner + "." + m, new Entry(c, r, true)); + } + + static { + Condition none = Condition.NONE, nonNull = Condition.NONNULL_ARGS, str = Condition.STRING_ARGS; + Returns decl = Returns.DECLARED, fresh = Returns.NONNULL_EXACT, self = Returns.RECEIVER; + + DECLARED.put("java/lang/Object", Set.of("()V", "getClass()Ljava/lang/Class;", "hashCode()I", + "equals(Ljava/lang/Object;)Z", "clone()Ljava/lang/Object;", "toString()Ljava/lang/String;", + "notify()V", "notifyAll()V", "wait()V", "wait(J)V", "wait(JI)V", "finalize()V")); + DECLARED.put("java/lang/Enum", Set.of("(Ljava/lang/String;I)V", "name()Ljava/lang/String;", + "ordinal()I", "toString()Ljava/lang/String;", "equals(Ljava/lang/Object;)Z", "hashCode()I", + "clone()Ljava/lang/Object;", "compareTo(Ljava/lang/Enum;)I", "getDeclaringClass()Ljava/lang/Class;", + "finalize()V", "describeConstable()Ljava/util/Optional;")); + + SUPERTYPES.put("java/lang/String", List.of("java/lang/Object", "java/io/Serializable", + "java/lang/Comparable", "java/lang/CharSequence")); + SUPERTYPES.put("java/lang/Enum", List.of("java/lang/Object", "java/io/Serializable", "java/lang/Comparable")); + for (String n : List.of("Integer", "Long", "Short", "Byte", "Double", "Float")) + SUPERTYPES.put("java/lang/" + n, List.of("java/lang/Number", "java/lang/Comparable")); + SUPERTYPES.put("java/lang/Number", List.of("java/lang/Object", "java/io/Serializable")); + SUPERTYPES.put("java/lang/Character", List.of("java/lang/Object", "java/io/Serializable", "java/lang/Comparable")); + SUPERTYPES.put("java/lang/Boolean", List.of("java/lang/Object", "java/io/Serializable", "java/lang/Comparable")); + SUPERTYPES.put("java/lang/AssertionError", List.of("java/lang/Error")); + SUPERTYPES.put("java/lang/Error", List.of("java/lang/Throwable")); + SUPERTYPES.put("java/lang/Exception", List.of("java/lang/Throwable")); + SUPERTYPES.put("java/lang/Throwable", List.of("java/lang/Object", "java/io/Serializable")); + + // Object and Enum: the implementations an application class may inherit. The final methods + // are safe for every receiver; the others only as the implementation a class inherits. + add("java/lang/Object", none, decl, "()V", "hashCode()I", "equals(Ljava/lang/Object;)Z"); + add("java/lang/Object", none, Returns.DECLARED, "getClass()Ljava/lang/Class;"); + add("java/lang/Enum", none, decl, "(Ljava/lang/String;I)V", "name()Ljava/lang/String;", "ordinal()I", + "toString()Ljava/lang/String;", "equals(Ljava/lang/Object;)Z", "hashCode()I", + "getDeclaringClass()Ljava/lang/Class;"); + + add("java/lang/Class", none, decl, "desiredAssertionStatus()Z"); + + // Throwables: constructing one is safe as long as the object is exactly the library class (a + // subclass could override fillInStackTrace). Throwing it is checked separately. + addExact("java/lang/AssertionError", none, decl, "()V", "(Z)V", "(C)V", "(I)V", + "(J)V", "(F)V", "(D)V", "(Ljava/lang/String;Ljava/lang/Throwable;)V"); + addExact("java/lang/AssertionError", str, decl, "(Ljava/lang/Object;)V"); + for (String t : List.of("java/lang/Error", "java/lang/Exception", "java/lang/RuntimeException")) + addExact(t, none, decl, "()V", "(Ljava/lang/String;)V"); + + // Boxes and their static helpers (no parsing: that throws NumberFormatException). + for (String[] b : new String[][] {{"Integer", "I"}, {"Long", "J"}, {"Short", "S"}, {"Byte", "B"}}) { + String o = "java/lang/" + b[0], p = b[1]; + add(o, none, fresh, "valueOf(" + p + ")L" + o + ";", "toString(" + p + ")Ljava/lang/String;", + "toString()Ljava/lang/String;"); + add(o, none, decl, "compare(" + p + p + ")I", "hashCode(" + p + ")I", "hashCode()I", + "equals(Ljava/lang/Object;)Z", "intValue()I", "longValue()J", "shortValue()S", "byteValue()B", + "floatValue()F", "doubleValue()D"); + add(o, nonNull, decl, "compareTo(L" + o + ";)I"); + } + for (String o : List.of("java/lang/Integer", "java/lang/Long")) { + String p = o.endsWith("Integer") ? "I" : "J"; + add(o, none, decl, "signum(" + p + ")I", "bitCount(" + p + ")I", "reverse(" + p + ")" + p, + "reverseBytes(" + p + ")" + p, "highestOneBit(" + p + ")" + p, "lowestOneBit(" + p + ")" + p, + "numberOfLeadingZeros(" + p + ")I", "numberOfTrailingZeros(" + p + ")I", + "rotateLeft(" + p + "I)" + p, "rotateRight(" + p + "I)" + p, "sum(" + p + p + ")" + p, + "max(" + p + p + ")" + p, "min(" + p + p + ")" + p, "compareUnsigned(" + p + p + ")I"); + add(o, none, fresh, "toString(" + p + "I)Ljava/lang/String;", "toBinaryString(" + p + ")Ljava/lang/String;", + "toHexString(" + p + ")Ljava/lang/String;", "toOctalString(" + p + ")Ljava/lang/String;"); + } + add("java/lang/Integer", none, decl, "toUnsignedLong(I)J"); + for (String[] b : new String[][] {{"Double", "D", "J"}, {"Float", "F", "I"}}) { + String o = "java/lang/" + b[0], p = b[1], bits = b[2]; + String toBits = p.equals("D") ? "doubleToLongBits" : "floatToIntBits"; + String toRaw = p.equals("D") ? "doubleToRawLongBits" : "floatToRawIntBits"; + String fromBits = p.equals("D") ? "longBitsToDouble" : "intBitsToFloat"; + add(o, none, fresh, "valueOf(" + p + ")L" + o + ";", "toString(" + p + ")Ljava/lang/String;", + "toHexString(" + p + ")Ljava/lang/String;", "toString()Ljava/lang/String;"); + add(o, none, decl, "isNaN(" + p + ")Z", "isInfinite(" + p + ")Z", "isFinite(" + p + ")Z", + "compare(" + p + p + ")I", toBits + "(" + p + ")" + bits, toRaw + "(" + p + ")" + bits, + fromBits + "(" + bits + ")" + p, "hashCode(" + p + ")I", "sum(" + p + p + ")" + p, + "max(" + p + p + ")" + p, "min(" + p + p + ")" + p, "isNaN()Z", "isInfinite()Z", "hashCode()I", + "equals(Ljava/lang/Object;)Z", "intValue()I", "longValue()J", "shortValue()S", "byteValue()B", + "floatValue()F", "doubleValue()D"); + add(o, nonNull, decl, "compareTo(L" + o + ";)I"); + } + add("java/lang/Boolean", none, fresh, "valueOf(Z)Ljava/lang/Boolean;", "toString(Z)Ljava/lang/String;", + "toString()Ljava/lang/String;"); + add("java/lang/Boolean", none, decl, "booleanValue()Z", "compare(ZZ)I", "hashCode(Z)I", "hashCode()I", + "equals(Ljava/lang/Object;)Z", "logicalAnd(ZZ)Z", "logicalOr(ZZ)Z", "logicalXor(ZZ)Z", + "parseBoolean(Ljava/lang/String;)Z"); + add("java/lang/Character", none, fresh, "valueOf(C)Ljava/lang/Character;", "toString(C)Ljava/lang/String;", + "toString()Ljava/lang/String;"); + add("java/lang/Character", none, decl, "charValue()C", "compare(CC)I", "hashCode(C)I", "hashCode()I", + "equals(Ljava/lang/Object;)Z", "digit(CI)I", "digit(II)I", "forDigit(II)C", "getNumericValue(C)I", + "getNumericValue(I)I"); + for (String pred : List.of("isDigit", "isLetter", "isLetterOrDigit", "isWhitespace", "isSpaceChar", + "isUpperCase", "isLowerCase", "isAlphabetic", "isJavaIdentifierStart", "isJavaIdentifierPart", + "isISOControl", "isTitleCase", "isDefined")) { + add("java/lang/Character", none, decl, pred + "(C)Z", pred + "(I)Z"); + } + add("java/lang/Character", none, decl, "toUpperCase(C)C", "toLowerCase(C)C", "toUpperCase(I)I", + "toLowerCase(I)I"); + + // String (final): methods that neither index nor parse. + add("java/lang/String", none, decl, "length()I", "isEmpty()Z", "hashCode()I", "equals(Ljava/lang/Object;)Z", + "equalsIgnoreCase(Ljava/lang/String;)Z", "indexOf(I)I", "indexOf(II)I", "lastIndexOf(I)I", + "lastIndexOf(II)I"); + add("java/lang/String", none, fresh, "toString()Ljava/lang/String;", "intern()Ljava/lang/String;", + "trim()Ljava/lang/String;", + "replace(CC)Ljava/lang/String;", "valueOf(I)Ljava/lang/String;", "valueOf(J)Ljava/lang/String;", + "valueOf(F)Ljava/lang/String;", "valueOf(D)Ljava/lang/String;", "valueOf(Z)Ljava/lang/String;", + "valueOf(C)Ljava/lang/String;", "()V"); + add("java/lang/String", nonNull, decl, "compareTo(Ljava/lang/String;)I", + "compareToIgnoreCase(Ljava/lang/String;)I", "startsWith(Ljava/lang/String;)Z", + "startsWith(Ljava/lang/String;I)Z", "endsWith(Ljava/lang/String;)Z", "indexOf(Ljava/lang/String;)I", + "indexOf(Ljava/lang/String;I)I", "lastIndexOf(Ljava/lang/String;)I", "(Ljava/lang/String;)V", + "([C)V"); + // Not concat, toLowerCase, toUpperCase or new StringBuilder(String): on JDK 8 their size + // computations overflow for huge strings and throw NegativeArraySizeException. + add("java/lang/String", nonNull, fresh, "valueOf([C)Ljava/lang/String;"); + add("java/lang/String", none, Returns.NONNULL_EXACT, "toCharArray()[C"); + add("java/lang/String", str, fresh, "valueOf(Ljava/lang/Object;)Ljava/lang/String;"); + + for (String sb : List.of("java/lang/StringBuilder", "java/lang/StringBuffer")) { + String l = "L" + sb + ";"; + add(sb, none, decl, "()V", "length()I"); + add(sb, none, self, "append(Z)" + l, "append(C)" + l, "append(I)" + l, "append(J)" + l, + "append(F)" + l, "append(D)" + l, "append(Ljava/lang/String;)" + l, "reverse()" + l); + add(sb, str, self, "append(Ljava/lang/Object;)" + l, "append(Ljava/lang/CharSequence;)" + l); + add(sb, nonNull, self, "append([C)" + l); + add(sb, none, fresh, "toString()Ljava/lang/String;"); + } + + // System.out / System.err (exactly java.io.PrintStream, see FactInterpreter). + String ps = "java/io/PrintStream"; + addExact(ps, none, decl, "println()V", "println(Z)V", "println(C)V", "println(I)V", "println(J)V", + "println(F)V", "println(D)V", "println(Ljava/lang/String;)V", "print(Z)V", "print(C)V", "print(I)V", + "print(J)V", "print(F)V", "print(D)V", "print(Ljava/lang/String;)V", "flush()V"); + addExact(ps, str, decl, "println(Ljava/lang/Object;)V", "print(Ljava/lang/Object;)V"); + addExact(ps, nonNull, decl, "println([C)V", "print([C)V"); + + add("java/lang/System", none, decl, "currentTimeMillis()J", "nanoTime()J", + "identityHashCode(Ljava/lang/Object;)I", "exit(I)V"); + add("java/lang/System", none, fresh, "lineSeparator()Ljava/lang/String;"); + } + + /** The model of a library method, or null if calls to it fail the check. */ + static Entry lookup(String owner, String name, String desc) { + if (owner.equals("java/lang/Math") || owner.equals("java/lang/StrictMath")) { + return MATH.contains(name) ? new Entry(Condition.NONE, Returns.DECLARED, false) : null; + } + if (owner.startsWith("[") && name.equals("clone") && desc.equals("()Ljava/lang/Object;")) { + return new Entry(Condition.NONE, Returns.CLONE, false); + } + return ENTRIES.get(owner + "." + name + desc); + } + + /** No class can override this library method: its class is final, or the method is. */ + static boolean cannotBeOverridden(String owner, String name, String desc) { + if (FINAL_CLASSES.contains(owner) || owner.startsWith("[")) return true; + if (owner.equals("java/lang/Object")) return name.equals("getClass") || name.equals(""); + if (owner.equals("java/lang/Enum")) { + return !name.equals("toString"); + } + return name.equals(""); + } + + /** Whether we know every method the class (with its library superclasses) declares. */ + static boolean knowsMethodsOf(String owner) { + return DECLARED.containsKey(owner); + } + + /** Whether the library class or one of its library superclasses declares the method. */ + static boolean declares(String owner, String name, String desc) { + return declaringClass(owner, name, desc) != null; + } + + /** The class among the known library classes that declares the method an instance of owner inherits. */ + static String declaringClass(String owner, String name, String desc) { + for (String c = owner; c != null; c = c.equals("java/lang/Enum") ? "java/lang/Object" : null) { + Set d = DECLARED.get(c); + if (d != null && d.contains(name + desc)) return c; + } + return null; + } + + static List knownSupertypes(String type) { + return SUPERTYPES.getOrDefault(type, List.of("java/lang/Object")); + } + + /** Library interfaces known to declare no default methods (on JDK 8 to 21). */ + private static final Set NO_DEFAULTS = Set.of("java/io/Serializable", "java/lang/Cloneable", + "java/lang/Comparable", "java/lang/Runnable", "java/lang/AutoCloseable", "java/io/Closeable"); + + static boolean hasNoDefaultMethods(String iface) { + return NO_DEFAULTS.contains(iface); + } + + static boolean isFinalClass(String owner) { + return FINAL_CLASSES.contains(owner); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java new file mode 100644 index 00000000..b99e2b8d --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java @@ -0,0 +1,361 @@ +package de.uzl.its.swat.staticcheck; + +import java.io.IOException; +import java.io.InputStream; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; +import java.util.jar.JarEntry; +import java.util.jar.JarFile; +import java.util.stream.Stream; +import org.objectweb.asm.ClassReader; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.tree.ClassNode; +import org.objectweb.asm.tree.FieldNode; +import org.objectweb.asm.tree.MethodNode; + +/** + * The application classes of a program (every class file on its classpath) and the queries the + * check needs on them: hierarchy, method and field resolution, and the possible targets of a call. + * Every class that is not on the classpath is a library (JDK) class. + */ +final class Program { + + /** + * The SV-COMP Verifier package: modelled by the check instead of analysed. Built at run time, + * so that the shadow jar's relocation of org.sosy_lab (java-smt) does not rewrite it. + */ + static final String VERIFIER_PACKAGE = "org/".concat("sosy_lab/sv_benchmarks/"); + + /** A method of an application class. */ + static final class Method { + final ClassNode owner; + final MethodNode node; + final String key; + + Method(ClassNode owner, MethodNode node) { + this.owner = owner; + this.node = node; + this.key = owner.name + "." + node.name + node.desc; + } + + boolean isStatic() { + return (node.access & Opcodes.ACC_STATIC) != 0; + } + + boolean hasCode() { + return (node.access & (Opcodes.ACC_ABSTRACT | Opcodes.ACC_NATIVE)) == 0; + } + + @Override + public String toString() { + return key; + } + } + + /** + * Where a call may go: application methods, plus library methods (owner.name+desc) when the + * receiver can be a library object or inherit a library implementation. + */ + static final class Targets { + final Set methods = new LinkedHashSet<>(); + final Set libraryMethods = new LinkedHashSet<>(); + } + + private final Map classes = new LinkedHashMap<>(); + private final Map methods = new LinkedHashMap<>(); + private final Map> subtypes = new HashMap<>(); + + Program(List classpath) throws IOException { + for (Path entry : classpath) { + if (Files.isDirectory(entry)) { + try (Stream files = Files.walk(entry)) { + for (Path p : (Iterable) files.filter(f -> f.toString().endsWith(".class"))::iterator) { + try (InputStream in = Files.newInputStream(p)) { + add(in); + } + } + } + } else if (entry.toString().endsWith(".jar") && Files.isRegularFile(entry)) { + try (JarFile jar = new JarFile(entry.toFile())) { + for (JarEntry e : Collections.list(jar.entries())) { + if (e.getName().endsWith(".class") && !e.getName().startsWith("META-INF/")) { + try (InputStream in = jar.getInputStream(e)) { + add(in); + } + } + } + } + } + } + for (ClassNode c : classes.values()) { + if (c.superName != null) subtypes.computeIfAbsent(c.superName, k -> new ArrayList<>()).add(c.name); + for (String i : c.interfaces) subtypes.computeIfAbsent(i, k -> new ArrayList<>()).add(c.name); + } + } + + private void add(InputStream in) throws IOException { + ClassNode c = new ClassNode(); + new ClassReader(in).accept(c, ClassReader.SKIP_FRAMES); + // The first definition on the classpath wins, as for the JVM's class loader. + if (classes.containsKey(c.name)) return; + if (unsupported == null) unsupported = unsupportedReason(c.name); + classes.put(c.name, c); + if (c.name.startsWith(VERIFIER_PACKAGE)) return; + for (MethodNode m : c.methods) { + Method method = new Method(c, m); + methods.put(method.key, method); + } + } + + /** + * Why a class on the classpath breaks the assumption that the classpath is the program (null + * if it does not). The JVM does not load such a class the way the analysis models it: it + * refuses java/ packages, serves packages the platform defines from the platform, and the + * analysis models only Verifier and ObjectFactory of the Verifier package, so the static + * initializer of any other class there would run unanalysed. + */ + private static String unsupportedReason(String name) { + int slash = name.lastIndexOf('/'); + String pkg = slash < 0 ? "" : name.substring(0, slash); + if (name.startsWith(VERIFIER_PACKAGE)) { + if (name.equals(VERIFIER_PACKAGE + "Verifier") || name.equals(VERIFIER_PACKAGE + "ObjectFactory")) return null; + return "class " + name + " in the Verifier package"; + } + for (String prefix : PLATFORM_PREFIXES) { + if (name.startsWith(prefix)) return "class " + name + " in a platform package"; + } + if (PLATFORM_PACKAGES.contains(pkg.replace('/', '.'))) return "class " + name + " in a package of the JDK"; + return null; + } + + /** + * Package prefixes of the platform: java/, javax/, jdk/, sun/, and those that exist only in the + * JDK 8 runtime (not as modules of the JDK the check runs on). + */ + private static final List PLATFORM_PREFIXES = List.of("java/", "javax/", "jdk/", "sun/", "com/sun/", + "org/omg/", "org/w3c/", "org/xml/", "org/ietf/", "org/jcp/"); + + /** The packages of the JDK's boot modules (the platform the check runs on). */ + private static final Set PLATFORM_PACKAGES = new HashSet<>(); + + static { + for (Module m : ModuleLayer.boot().modules()) PLATFORM_PACKAGES.addAll(m.getPackages()); + } + + /** Set if a class on the classpath breaks the model of class loading; the check then fails. */ + private String unsupported; + + String unsupportedClasspath() { + return unsupported; + } + + /** An application class (not a library class, and not the modelled Verifier package). */ + boolean isApp(String internalName) { + return classes.containsKey(internalName) && !internalName.startsWith(VERIFIER_PACKAGE); + } + + boolean isOnClasspath(String internalName) { + return classes.containsKey(internalName); + } + + ClassNode clazz(String internalName) { + return classes.get(internalName); + } + + Collection methods() { + return methods.values(); + } + + Method method(String owner, String name, String desc) { + return methods.get(owner + "." + name + desc); + } + + Collection appClasses() { + List out = new ArrayList<>(); + for (ClassNode c : classes.values()) if (isApp(c.name)) out.add(c); + return out; + } + + boolean isEnum(String internalName) { + ClassNode c = classes.get(internalName); + return c != null && isApp(internalName) && (c.access & Opcodes.ACC_ENUM) != 0 + && "java/lang/Enum".equals(c.superName); + } + + /** The class and its application superclasses, ending with the first library class (if any). */ + List superChain(String internalName) { + List chain = new ArrayList<>(); + String c = internalName; + while (c != null) { + chain.add(c); + ClassNode node = classes.get(c); + if (node == null || !isApp(c)) break; + c = node.superName; + } + return chain; + } + + /** All application types that are subtypes of the given type, the type itself included. */ + Set appSubtypes(String type) { + Set out = new LinkedHashSet<>(); + Deque work = new ArrayDeque<>(); + work.add(type); + while (!work.isEmpty()) { + String t = work.poll(); + if (isApp(t) && !out.add(t)) continue; + for (String s : subtypes.getOrDefault(t, List.of())) if (!out.contains(s)) work.add(s); + } + return out; + } + + /** All application supertypes (classes and interfaces) of an application type, itself included. */ + Set appSupertypes(String type) { + Set out = new LinkedHashSet<>(); + Deque work = new ArrayDeque<>(); + work.add(type); + while (!work.isEmpty()) { + String t = work.poll(); + ClassNode c = classes.get(t); + if (c == null || !isApp(t) || !out.add(t)) continue; + if (c.superName != null) work.add(c.superName); + work.addAll(c.interfaces); + } + return out; + } + + /** The field a field instruction refers to: declared in the owner or a superclass/superinterface. */ + FieldNode resolveField(String owner, String name, String desc, String[] declaringClass) { + Deque work = new ArrayDeque<>(); + work.add(owner); + Set seen = new HashSet<>(); + while (!work.isEmpty()) { + String t = work.poll(); + if (!seen.add(t)) continue; + ClassNode c = classes.get(t); + if (c == null || !isApp(t)) continue; + for (FieldNode f : c.fields) { + if (f.name.equals(name) && f.desc.equals(desc)) { + declaringClass[0] = t; + return f; + } + } + work.addAll(c.interfaces); + if (c.superName != null) work.add(c.superName); + } + return null; + } + + /** + * The method a static or special call (or a virtual call on a known runtime class) executes, + * searching the class and its superclasses. Returns the application method, or null with + * libraryOwner[0] set to the first library class of the chain when the search leaves the + * application. + */ + Method resolveInChain(String owner, String name, String desc, String[] libraryOwner) { + for (String c : superChain(owner)) { + if (!isApp(c)) { + libraryOwner[0] = c; + return null; + } + Method m = method(c, name, desc); + if (m != null) return m; + } + return null; + } + + /** All default methods for name+desc in the application interfaces of a class. */ + private List defaults(String clazz, String name, String desc) { + List out = new ArrayList<>(); + for (String t : appSupertypes(clazz)) { + ClassNode c = classes.get(t); + if ((c.access & Opcodes.ACC_INTERFACE) == 0) continue; + Method m = method(t, name, desc); + if (m != null && m.hasCode() && !m.isStatic() && (m.node.access & Opcodes.ACC_PRIVATE) == 0) out.add(m); + } + return out; + } + + /** + * The targets of an invokevirtual/invokeinterface on an application owner type: a superset of + * the methods the JVM may select for each concrete application subtype of the owner (JVMS + * 5.4.6). Rather than following the selection rules exactly (package-private overriding, + * maximally-specific default methods), every non-private instance method with that name and + * descriptor in the superclass chain, and every default method of the application + * superinterfaces, counts. A library implementation counts unless a public or protected + * application method overrides it. Returns null if a library class or library interface whose + * methods are unknown might provide it. + */ + Targets virtualTargets(String owner, String name, String desc) { + Targets t = new Targets(); + Method declared = method(owner, name, desc); + if (declared != null && (declared.node.access & Opcodes.ACC_PRIVATE) != 0) { + // A private method is selected directly (invokevirtual on a nestmate's private method). + if (!declared.hasCode()) return null; + t.methods.add(declared); + return t; + } + for (String sub : appSubtypes(owner)) { + ClassNode c = classes.get(sub); + if ((c.access & (Opcodes.ACC_ABSTRACT | Opcodes.ACC_INTERFACE)) != 0) continue; + boolean overridesLibrary = false; + String lib = null; + for (String k : superChain(sub)) { + if (!isApp(k)) { + lib = k; + break; + } + Method m = method(k, name, desc); + if (m == null || m.isStatic() || (m.node.access & Opcodes.ACC_PRIVATE) != 0) continue; + if ((m.node.access & Opcodes.ACC_NATIVE) != 0) return null; + if (m.hasCode()) t.methods.add(m); + if ((m.node.access & (Opcodes.ACC_PUBLIC | Opcodes.ACC_PROTECTED)) != 0) overridesLibrary = true; + } + t.methods.addAll(defaults(sub, name, desc)); + if (overridesLibrary) continue; + // A default method of a library interface could be selected instead, and we do not know them. + for (String sup : appSupertypes(sub)) { + for (String i : classes.get(sup).interfaces) { + if (!isApp(i) && !JdkModel.hasNoDefaultMethods(i)) return null; + } + } + if (lib == null) continue; + String declaring = JdkModel.declaringClass(lib, name, desc); + if (declaring != null) t.libraryMethods.add(declaring + "." + name + desc); + else if (!JdkModel.knowsMethodsOf(lib)) return null; + } + return t; + } + + /** Whether a value of type {@code from} is always assignable to type {@code to}. */ + boolean isAssignable(String from, String to) { + if (from == null || to == null) return false; + if (from.equals(to) || to.equals("java/lang/Object")) return true; + if (from.startsWith("[")) { + if (to.equals("java/lang/Cloneable") || to.equals("java/io/Serializable")) return true; + if (!to.startsWith("[")) return false; + String fe = from.substring(1), te = to.substring(1); + if (fe.startsWith("[") || te.startsWith("[")) return isAssignable(fe, te); + if (fe.startsWith("L") && te.startsWith("L")) + return isAssignable(fe.substring(1, fe.length() - 1), te.substring(1, te.length() - 1)); + return fe.equals(te); + } + if (to.startsWith("[")) return false; + Deque work = new ArrayDeque<>(); + work.add(from); + Set seen = new HashSet<>(); + while (!work.isEmpty()) { + String t = work.poll(); + if (!seen.add(t)) continue; + if (t.equals(to)) return true; + if (isApp(t)) { + ClassNode c = classes.get(t); + if (c.superName != null) work.add(c.superName); + work.addAll(c.interfaces); + } else { + work.addAll(JdkModel.knownSupertypes(t)); + } + } + return false; + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy new file mode 100644 index 00000000..038e9251 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy @@ -0,0 +1,152 @@ +package de.uzl.its.swat.staticcheck + +import spock.lang.Specification +import spock.lang.TempDir +import spock.lang.Unroll + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path + +/** + * Compiles small programs and checks the verdict of the exception-freedom check. The programs + * that may throw an uncaught RuntimeException must never pass; the others document what the + * check is able to prove. + */ +class ExceptionFreedomCheckSpec extends Specification { + + static final String VERIFIER = ''' +package org.sosy_lab.sv_benchmarks; +public final class Verifier { + public static void assume(boolean c) { if (!c) Runtime.getRuntime().halt(1); } + public static boolean nondetBoolean() { return new java.util.Random().nextBoolean(); } + public static int nondetInt() { return new java.util.Random().nextInt(); } + public static long nondetLong() { return new java.util.Random().nextLong(); } + public static double nondetDouble() { return new java.util.Random().nextDouble(); } + public static String nondetString() { return "" + new java.util.Random().nextInt(); } + public static T nondetObject(Class t, ObjectFactory f) { return f.createObject(); } +} +''' + static final String FACTORY = ''' +package org.sosy_lab.sv_benchmarks; +public interface ObjectFactory { T createObject(); } +''' + + @TempDir + Path dir + + ExceptionFreedomCheck.Result check(String main, String release = '8', Map extra = [:]) { + Path src = dir.resolve('src'), out = dir.resolve('classes') + Files.createDirectories(src.resolve('org/sosy_lab/sv_benchmarks')) + Files.createDirectories(out) + Files.writeString(src.resolve('org/sosy_lab/sv_benchmarks/Verifier.java'), VERIFIER) + Files.writeString(src.resolve('org/sosy_lab/sv_benchmarks/ObjectFactory.java'), FACTORY) + Files.writeString(src.resolve('Main.java'), 'import org.sosy_lab.sv_benchmarks.Verifier;\n' + main) + extra.each { path, code -> + Files.createDirectories(src.resolve(path).parent) + Files.writeString(src.resolve(path), code) + } + def files = [] + src.toFile().eachFileRecurse { if (it.name.endsWith('.java')) files << it.path } + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, null, + (['--release', release, '-nowarn', '-d', out.toString()] + files) as String[]) + assert rc == 0 + return ExceptionFreedomCheck.check([out]) + } + + @Unroll + def "may throw: #name"() { + expect: + !check(program, release).exceptionFree + + where: + name | release | program + 'division by input' | '8' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); int y = 10 / x; } }' + 'long division by zero constant' | '8' | 'public class Main { public static void main(String[] a) { long x = Verifier.nondetLong(); long y = x / 0L; } }' + 'array index from input' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[3]; arr[Verifier.nondetInt()] = 1; } }' + 'array index past the end' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[3]; int i = 2; i++; arr[i] = 1; } }' + 'array index in a loop' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[3]; for (int i = 0; i < 4; i++) arr[i] = 1; } }' + 'negative array size' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[Verifier.nondetInt()]; } }' + 'field never assigned' | '8' | 'class B { void g() {} } class A { B b; } public class Main { public static void main(String[] a) { new A().b.g(); } }' + 'field assigned on one path' | '8' | 'class B { void g() {} } class A { B b; A(boolean c) { if (c) b = new B(); } } public class Main { public static void main(String[] a) { new A(Verifier.nondetBoolean()).b.g(); } }' + 'field set to null later' | '8' | 'class B { void g() {} } class A { B b = new B(); } public class Main { public static void main(String[] a) { A x = new A(); if (Verifier.nondetBoolean()) x.b = null; x.b.g(); } }' + 'read in overridden method from super constructor' | '8' | 'class B { void g() {} } class P { P() { init(); } void init() {} } class C extends P { B b = new B(); void init() { b.g(); } } public class Main { public static void main(String[] a) { new C(); } }' + 'receiver escapes before assignment' | '8' | 'class B { void g() {} } class Reg { static A last = new A(1); } class A { B b; A(int x) { Reg.last = this; int y = 10 / x; b = new B(); } } public class Main { public static void main(String[] a) { try { new A(Verifier.nondetInt()); } catch (Exception e) {} Reg.last.b.g(); } }' + 'static field read before assignment' | '8' | 'class B { void g() {} } class T { static B peek() { return S.b; } } class S { static B a = T.peek(); static B b = new B(); } public class Main { public static void main(String[] a) { S.a.g(); } }' + 'static field never assigned' | '8' | 'class B { void g() {} } class S { static B b; } public class Main { public static void main(String[] a) { S.b.g(); } }' + 'null argument' | '8' | 'class B { void g() {} } public class Main { static void f(B b) { b.g(); } public static void main(String[] a) { f(Verifier.nondetBoolean() ? new B() : null); } }' + 'null return value' | '8' | 'class B { void g() {} } public class Main { static B make() { return Verifier.nondetBoolean() ? new B() : null; } public static void main(String[] a) { make().g(); } }' + 'interface implementation throws' | '8' | 'interface I { void f(); } class A implements I { public void f() { throw new IllegalStateException(); } } class C implements I { public void f() {} } public class Main { public static void main(String[] a) { I i = Verifier.nondetBoolean() ? new A() : new C(); i.f(); } }' + 'toString callback through valueOf' | '8' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { String s = String.valueOf(new A()); } }' + 'toString callback in concatenation' | '8' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { String s = "x" + new A(); } }' + 'toString callback through indy' | '17' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { String s = "x" + new A(); } }' + 'rethrow of caught exception' | '8' | 'public class Main { public static void main(String[] a) { try { int y = 1 / Verifier.nondetInt(); } catch (ArithmeticException e) { throw e; } } }' + 'finally after a throwing body' | '8' | 'public class Main { static int n; public static void main(String[] a) { try { int y = 1 / Verifier.nondetInt(); } finally { n++; } } }' + 'inner handler rethrows' | '8' | 'public class Main { public static void main(String[] a) { try { try { int y = 1 / Verifier.nondetInt(); } catch (Exception e) { throw new IllegalStateException(); } } catch (ArithmeticException e) {} } }' + 'static initializer throws' | '8' | 'class S { static int x = 10 / Verifier.nondetInt(); } public class Main { public static void main(String[] a) { int y = S.x; } }' + 'array store of wrong type' | '8' | 'public class Main { public static void main(String[] a) { Object[] arr = new String[1]; arr[0] = new Object(); } }' + 'failing cast' | '8' | 'public class Main { public static void main(String[] a) { Object o = Verifier.nondetBoolean() ? (Object) "s" : (Object) new Object(); String s = (String) o; } }' + 'unboxing null' | '8' | 'public class Main { public static void main(String[] a) { Integer i = Verifier.nondetBoolean() ? null : 3; int x = i; } }' + 'callback from a caught library call' | '8' | 'class B { void g() {} } class H { static B b = new B(); } class Cmp implements java.util.Comparator { public int compare(Object x, Object y) { H.b = (B) x; return 0; } } public class Main { public static void main(String[] a) { try { java.util.Arrays.sort(new Object[] {null, null}, new Cmp()); } catch (Exception e) {} H.b.g(); } }' + 'lambda' | '8' | 'public class Main { public static void main(String[] a) { Runnable r = () -> { int y = 1 / Verifier.nondetInt(); }; r.run(); } }' + 'runtime exception subclass thrown' | '8' | 'class E extends RuntimeException {} public class Main { public static void main(String[] a) { if (Verifier.nondetBoolean()) throw new E(); } }' + 'private method of abstract class' | '17' | 'public class Main { static abstract class P { private void m() { int z = Verifier.nondetInt(); int q = 1 / z; } void call() { m(); } } static class Q extends P { void m() {} } public static void main(String[] a) { new Q().call(); } }' + 'nondetObject' | '8' | 'class B { void g() {} } public class Main { public static void main(String[] a) { B b = Verifier.nondetObject(B.class, () -> new B()); b.g(); } }' + 'finalizer' | '8' | 'class B { protected void finalize() {} } public class Main { public static void main(String[] a) { new B(); } }' + 'unmodelled library call' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetString(); char c = s.charAt(3); } }' + 'println of an object' | '8' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { System.out.println(new A()); } }' + 'null string argument' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetBoolean() ? null : "x"; boolean b = "abc".startsWith(s); } }' + 'main called with null' | '8' | 'public class Main { public static void main(String[] a) { if (Verifier.nondetBoolean()) { main(null); } else { int n = a.length; } } }' + 'more specific default method' | '8' | 'interface I { default int m() { return 0; } } interface J extends I { default int m() { throw new IllegalStateException(); } } class C implements I, J {} public class Main { public static void main(String[] a) { new C().m(); } }' + 'private method does not implement' | '17' | 'interface I { default void m() { throw new IllegalStateException(); } } class B { private void m() {} } class C extends B implements I {} public class Main { public static void main(String[] a) { I x = new C(); x.m(); } }' + 'receiver escapes through a join' | '8' | 'interface G { String get(); } class G0 implements G { public String get() { return "ok"; } } class Holder { G g; Holder() { this.g = new G0(); } } abstract class Base implements G { Base() { G o = Verifier.nondetBoolean() ? this : Main.H.g; Main.H.g = o; } } class C extends Base { String f; C(int d) { super(); int z = 10 / d; this.f = "x"; } public String get() { return this.f; } } public class Main { static Holder H = new Holder(); public static void main(String[] a) { try { new C(Verifier.nondetInt()); } catch (RuntimeException e) { } String s = H.g.get(); int n = s.length(); } }' + 'concat overflows on JDK 8' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetString(); String t = s.concat(s); } }' + 'StringBuilder constructor overflows' | '8' | 'public class Main { public static void main(String[] a) { StringBuilder sb = new StringBuilder(Verifier.nondetString()); } }' + 'library default method' | '8' | 'class It implements java.util.Iterator { public boolean hasNext() { return false; } public Object next() { return null; } } public class Main { public static void main(String[] a) { if (Verifier.nondetInt() == 42) new It().remove(); } }' + 'library default calls back' | '17' | 'class X implements CharSequence { public int length() { throw new IllegalStateException(); } public char charAt(int i) { return 0; } public CharSequence subSequence(int s, int e) { return this; } public String toString() { return ""; } } public class Main { public static void main(String[] a) { if (Verifier.nondetBoolean()) { boolean b = new X().isEmpty(); } } }' + 'library default via app interface' | '8' | 'interface J extends java.util.Iterator {} abstract class Ab implements J { public boolean hasNext() { return false; } } class It extends Ab { public Object next() { return null; } } public class Main { public static void main(String[] a) { J j = new It(); j.remove(); } }' + } + + static final String STEAL = 'static { try { java.lang.reflect.Field f = Class.forName("Main").getDeclaredField("o"); f.setAccessible(true); f.set(null, null); } catch (Exception e) {} }' + + @Unroll + def "classes the JVM loads differently than modelled: #name"() { + when: + def r = check(program, '8', extra) + + then: + !r.exceptionFree + !r.assertionFree + + where: + name | program | extra + 'Verifier package helper' | 'public class Main { static Object o = new Object(); public static void main(String[] a) { int z = org.sosy_lab.sv_benchmarks.Helper.X; System.out.println(o.hashCode() + z); } }' | ['org/sosy_lab/sv_benchmarks/Helper.java': 'package org.sosy_lab.sv_benchmarks; public class Helper { public static int X; ' + STEAL + ' }'] + 'javax class nulls a field' | 'public class Main { static Object o = new Object(); public static void main(String[] a) { int z = javax.mine.Helper.X; System.out.println(o.hashCode() + z); } }' | ['javax/mine/Helper.java': 'package javax.mine; public class Helper { public static int X; ' + STEAL + ' }'] + 'javax class asserts' | 'public class Main { public static void main(String[] a) { int z = javax.mine.Config.LEVEL; System.out.println(z); } }' | ['javax/mine/Config.java': 'package javax.mine; public class Config { public static int LEVEL; static { LEVEL = -1; assert LEVEL >= 0 : "bad level"; } }'] + 'java class field' | 'public class Main { public static void main(String[] a) { int z = java.mine.Config.LEVEL; System.out.println(z); } }' | ['java/mine/Config.java': 'package java.mine; public class Config { public static int LEVEL = 1; }'] + 'java class array' | 'public class Main { public static void main(String[] a) { Object[] arr = new java.mine.Config[1]; System.out.println(arr.length); } }' | ['java/mine/Config.java': 'package java.mine; public class Config { public static int LEVEL = 1; }'] + 'class shadowed by the JDK' | 'import org.xml.sax.helpers.AttributesImpl; public class Main { public static void main(String[] a) { AttributesImpl x = new AttributesImpl(); x.removeAttribute(0); } }' | ['org/xml/sax/helpers/AttributesImpl.java': 'package org.xml.sax.helpers; public class AttributesImpl { public AttributesImpl() {} public void removeAttribute(int index) {} }'] + } + + @Unroll + def "proven exception-free: #name"() { + expect: + check(program, release).exceptionFree + + where: + name | release | program + 'arithmetic and an assert' | '8' | 'public class Main { public static void main(String[] a) { double x = Verifier.nondetDouble(); Verifier.assume(x > 0); double y = Math.sin(x) * x; assert y < 10; } }' + 'division by a constant' | '8' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); int d = 4; int y = x / d + x % 3; } }' + 'array with constant indices' | '8' | 'public class Main { public static void main(String[] a) { double[] arr = new double[] {1, 2, 3}; arr[2] = arr[0] + Verifier.nondetDouble(); } }' + 'fields assigned in the constructor' | '8' | 'class B { boolean on; boolean isOn() { return on; } } class A { B b; B c; A() { b = new B(); c = b; } void step() { if (b.isOn()) c.on = false; } } public class Main { public static void main(String[] a) { A x = new A(); while (Verifier.nondetBoolean()) x.step(); } }' + 'enum switch' | '8' | 'enum L { LOW, HIGH } class S { L l = L.LOW; void up() { switch (l) { case LOW: l = L.HIGH; break; default: break; } } } public class Main { public static void main(String[] a) { S s = new S(); if (Verifier.nondetBoolean()) s.up(); assert s.l != L.HIGH; } }' + 'string switch on input' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetString(); int r; switch (s) { case "a": r = 1; break; default: r = 0; } } }' + 'recursion' | '8' | 'public class Main { static int f(int n) { return n <= 0 ? 0 : 1 + f(n - 1); } public static void main(String[] a) { int r = f(Verifier.nondetInt()); assert r >= 0; } }' + 'caught division' | '8' | 'public class Main { public static void main(String[] a) { try { int y = 1 / Verifier.nondetInt(); } catch (ArithmeticException e) { assert false; } } }' + 'finally after a safe body' | '8' | 'public class Main { static int n; public static void main(String[] a) { try { n = Verifier.nondetInt(); } finally { n++; } } }' + 'checked exception' | '8' | 'public class Main { public static void main(String[] a) throws Exception { if (Verifier.nondetBoolean()) throw new Exception(); } }' + 'printing' | '8' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); System.out.println("x=" + x); } }' + 'static field from initializer' | '8' | 'public class Main { static String s = "abc"; static int[] t = new int[2]; public static void main(String[] a) { t[1] = s.length(); } }' + 'string concatenation with indy' | '17' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); String s = "x=" + x + Verifier.nondetString(); assert s.length() > 0; } }' + } +} diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index be21affd..a07bb20c 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -137,6 +137,7 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("--sa-no-callback-targets", action="store_true", help="Do not count library calls as possible asserts when application code that library code may call back (overrides of library methods, lambdas) can reach an assert. Unsound: an assert reached only through such a callback can then give a false SAFE", default=False) parser.add_argument("--sa-rank-distance", action="store_true", help="Try branches closest to an assert (by static pre-analysis graph distance) first, instead of in plain DFS order", default=False) parser.add_argument("--solver-rlimit", type=int, default=0, help="Z3 resource limit (rlimit) for the first query of each branch in sv-comp mode; a branch that runs out is retried later with a growing limit. 0 (default): unlimited") + parser.add_argument("--no-property-precheck", action="store_true", help="Do not run the static property pre-check (sv-comp mode), which can prove no-runtime-exception (no uncaught RuntimeException is possible) or valid-assert (no AssertionError is ever created) for the whole program", default=False) parser.add_argument("--parallel-sa", action="store_true", help="Run the static pre-analysis in the background and use it once it is ready (sv-comp mode). By default exploration waits for it: running it in parallel makes runs nondeterministic", default=False) # SV-COMP witness arguments: the explorer writes the violation witness from the trace of the diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..61de0013 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -16,6 +16,7 @@ from strategy.StrategyService import StrategyService from data.StaticAnalysisGraph.SAGraph import SAGraph from svcomp.StaticPreAnalysis import StaticPreAnalysis +from svcomp.PropertyPreCheck import PropertyPreCheck from enum import Enum from svcomp.SymbolicStorage import SymbolicStorage, DataTypes @@ -92,6 +93,7 @@ def __init__(self, args): self.verification_category = VerificationCategory(self.args.property) self.sa_graph = SAGraph() # static analysis graph, empty until the pre-analysis is adopted self.sa = StaticPreAnalysis(args) + self.precheck = PropertyPreCheck(args, self.verification_category.value) self.sa_adopted_round: int | None = None self.round_idx = 0 self.nr_solver_calls = 0 @@ -216,7 +218,10 @@ def log_output(self, output: List[str]): def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, cp) -> Verdict: """Runs the testcase using the constructed Java command.""" - + + # Static property pre-check: if it proves the property, round 0 only cross-checks it. + self.precheck.run() + # Static pre-analysis: an external Java subprocess plus loading its graph. By default # exploration waits for it, and the wait is its own timing stage (otherwise it would be # folded into the symbolic explorer residual). With --parallel-sa it runs in the background @@ -260,6 +265,9 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, self.log_output(output) logger.info(f'[STATUS] {status}') next_step: Action = self.determine_next_step(status, output) + if self.precheck.proven: + self.round_idx += 1 + return self.verdict_with_proof(next_step) # Visualize DB tree # print("Plotting DB Tree...", flush=True) @@ -294,6 +302,19 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, + def verdict_with_proof(self, next_step: Action) -> Verdict: + """The verdict after round 0 once the pre-check proved the property: SAFE, as no execution + can violate it, whatever the exploration could model. A violation found in round 0 + contradicts the proof, and then neither is trusted.""" + if next_step == Action.REPORTVERDICT and self.state.verdict == Verdict.VIOLATION: + logger.error(f'[PRECHECK] Round 0 found a violation of a property the pre-check proved; reporting UNKNOWN') + Database.instance().record_execution_error(ENDPOINT_ID, 'precheck_contradiction', self.precheck.reason or '') + self.state.verdict = Verdict.UNKNOWN + else: + logger.info(f'[PRECHECK] Property proven statically: {self.precheck.reason}') + self.state.verdict = Verdict.SAFE + return self.state.verdict + def check_divergence(self, trace) -> None: """Checks that the last run took the side of branch_to_explore its solution was solved for. @@ -442,25 +463,29 @@ def run(self): if self.sa.duration is not None: TimingManager.instance().record_static_analysis_time(self.sa.duration, blocking=not self.args.parallel_sa) - if (verdict == Verdict.SAFE) and Database.instance().get_tree(ENDPOINT_ID).symbolic_context_loss: + # The soundness downgrades below guard a SAFE that rests on the exploration. A SAFE from the + # property pre-check rests on a static proof for all executions instead, so they do not apply. + downgrade = not (verdict == Verdict.SAFE and self.precheck.proven) + + if downgrade and (verdict == Verdict.SAFE) and Database.instance().get_tree(ENDPOINT_ID).symbolic_context_loss: logger.warning(f'[SVCOMP] Found symbolic context loss') verdict = Verdict.UNKNOWN - if (verdict == Verdict.SAFE) and Database.instance().get_tree(ENDPOINT_ID).symbolic_precision_loss: + if downgrade and (verdict == Verdict.SAFE) and Database.instance().get_tree(ENDPOINT_ID).symbolic_precision_loss: logger.warning(f'[SVCOMP] Found symbolic precision loss') verdict = Verdict.UNKNOWN - if (verdict == Verdict.SAFE) and any(e.get('kind') == 'unexpected_divergence' + if downgrade and (verdict == Verdict.SAFE) and any(e.get('kind') == 'unexpected_divergence' for e in Database.instance().get_tree(ENDPOINT_ID).execution_errors): logger.warning(f'[SVCOMP] A solution did not reach the side of the branch it was solved for') verdict = Verdict.UNKNOWN - if (verdict == Verdict.SAFE) and any(e.get('kind') == 'sa_desync' + if downgrade and (verdict == Verdict.SAFE) and any(e.get('kind') == 'sa_desync' for e in Database.instance().get_tree(ENDPOINT_ID).execution_errors): logger.warning(f'[SVCOMP] The SA walk fell out of step with the execution (see [DFS] SA desync)') verdict = Verdict.UNKNOWN - if (verdict == Verdict.SAFE) and Database.instance().get_tree(ENDPOINT_ID).uncaught_exceptions > 0: + if downgrade and (verdict == Verdict.SAFE) and Database.instance().get_tree(ENDPOINT_ID).uncaught_exceptions > 0: logger.warning(f'[SVCOMP] Found uncaught exceptions during symbolic execution') verdict = Verdict.UNKNOWN @@ -490,7 +515,7 @@ def run(self): stats_file = os.path.join(log_dir, 'stats.json') write_testcase_stats(Path(stats_file), verdict, self.verification_category, Database.instance().get_tree(ENDPOINT_ID), self.round_idx, self.nr_solver_calls, self.sa.stats(self.sa_adopted_round), - self.solver_limit_hits) + self.solver_limit_hits, self.precheck.stats()) self.kill_current_process() diff --git a/symbolic-explorer/svcomp/PropertyPreCheck.py b/symbolic-explorer/svcomp/PropertyPreCheck.py new file mode 100644 index 00000000..624e6056 --- /dev/null +++ b/symbolic-explorer/svcomp/PropertyPreCheck.py @@ -0,0 +1,81 @@ +""" +Static property pre-check for the SV-COMP driver. + +The executor jar contains a conservative bytecode analysis (de.uzl.its.swat.staticcheck. +ExceptionFreedomCheck) of the whole program on the classpath. It proves, or fails to prove: + +- for no-runtime-exception: no RuntimeException can escape Main.main or a static initializer; +- for valid-assert: no AssertionError is ever created, so no assert can fail. + +A proven property holds on every execution, independently of what the symbolic exploration can +model, so the driver may answer SAFE even where context loss, precision loss, uncaught exceptions +or an unexhausted path space would otherwise prevent it. A failed, crashed or timed-out check +proves nothing, and the driver proceeds as without it. +""" + +import json +import os +import subprocess +import time + +import log +logger = log.get_logger() + +CHECK_CLASS = "de.uzl.its.swat.staticcheck.ExceptionFreedomCheck" +CHECK_TIMEOUT_S = 60 + +# The property file name -> the field of the check's result that proves it. +PROVES = { + "no-runtime-exception.prp": ("exception_free", "reason"), + "valid-assert.prp": ("assertion_free", "assertion_reason"), +} + + +class PropertyPreCheck: + def __init__(self, args, prop: str): + self.args = args + self.prop = prop + self.enabled = prop in PROVES and not getattr(args, "no_property_precheck", False) + self.status = "disabled" if not self.enabled else "not_started" + self.proven = False + self.reason: str | None = None + self.duration: float | None = None + + @staticmethod + def _is_swat_library(path: str) -> bool: + """Z3's Java bindings, which SWAT itself puts on the target's classpath: not part of the program.""" + return os.path.basename(path) == "com.microsoft.z3.jar" + + def command(self) -> list[str]: + classpath = [os.path.abspath(p) for p in self.args.classpath if not self._is_swat_library(p)] + return [self.args.java_path, "-Xmx2g", "-cp", self.args.agent, CHECK_CLASS, *classpath] + + def run(self) -> bool: + """Runs the check (blocking) and returns whether it proved the property.""" + if not self.enabled: + return False + start = time.perf_counter() + try: + proc = subprocess.run(self.command(), capture_output=True, text=True, timeout=CHECK_TIMEOUT_S) + result = json.loads(proc.stdout.strip().splitlines()[-1]) + field, reason_field = PROVES[self.prop] + self.proven = result.get(field) is True + self.reason = result.get(reason_field) + self.status = "proven" if self.proven else "not_proven" + except subprocess.TimeoutExpired: + self.status = "timeout" + except Exception as e: + logger.error(f'[PRECHECK] Property pre-check failed: {type(e).__name__}: {e}') + self.status = "failed" + self.duration = time.perf_counter() - start + logger.info(f'[PRECHECK] {self.prop}: {self.status} after {self.duration:.2f}s ({self.reason})') + return self.proven + + def stats(self) -> dict: + return { + 'enabled': self.enabled, + 'status': self.status, + 'proven': self.proven, + 'reason': self.reason, + 'duration_s': self.duration, + } diff --git a/symbolic-explorer/svcomp/TestcaseStats.py b/symbolic-explorer/svcomp/TestcaseStats.py index 6f129eaa..e2e5ef10 100644 --- a/symbolic-explorer/svcomp/TestcaseStats.py +++ b/symbolic-explorer/svcomp/TestcaseStats.py @@ -25,7 +25,7 @@ def _signature(inv: dict) -> str: def build_testcase_stats(verdict, category, tree, symbolic_exec_iterations: int, nr_solver_calls: int, static_analysis: dict, - solver_limit_hits: int = 0) -> dict: + solver_limit_hits: int = 0, property_precheck: dict | None = None) -> dict: """ Assemble the consolidated per-testcase statistics dictionary. @@ -34,6 +34,7 @@ def build_testcase_stats(verdict, category, tree, symbolic_exec_iterations: int, category: The VerificationCategory enum for the property. tree: The per-endpoint Tree holding accumulated metadata for the testcase. static_analysis: The pre-analysis outcome, see StaticPreAnalysis.stats(). + property_precheck: The property pre-check outcome, see PropertyPreCheck.stats(). Returns: A JSON-serializable dict describing the testcase outcome. @@ -73,13 +74,15 @@ def build_testcase_stats(verdict, category, tree, symbolic_exec_iterations: int, 'expected_divergences': tree.expected_divergences, }, 'static_analysis': static_analysis, + 'property_precheck': property_precheck, } def write_testcase_stats(filepath: Path, verdict, category, tree, symbolic_exec_iterations: int, nr_solver_calls: int, static_analysis: dict, - solver_limit_hits: int = 0): + solver_limit_hits: int = 0, property_precheck: dict | None = None): """Write the consolidated per-testcase statistics to ``filepath`` as JSON.""" - data = build_testcase_stats(verdict, category, tree, symbolic_exec_iterations, nr_solver_calls, static_analysis, solver_limit_hits) + data = build_testcase_stats(verdict, category, tree, symbolic_exec_iterations, nr_solver_calls, static_analysis, solver_limit_hits, + property_precheck) filepath.parent.mkdir(parents=True, exist_ok=True) with open(filepath, 'w') as f: diff --git a/symbolic-explorer/tests/test_property_precheck.py b/symbolic-explorer/tests/test_property_precheck.py new file mode 100644 index 00000000..3fe61a29 --- /dev/null +++ b/symbolic-explorer/tests/test_property_precheck.py @@ -0,0 +1,109 @@ +""" +Unit tests for the static property pre-check: how its result is read per property, and the verdict +the driver gives after round 0 when the property is proven. + +It imports the driver, which needs the explorer's dependencies (z3, fastapi, ...) that the system +Python lacks, so run it with the harness venv, from symbolic-explorer/: + ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_property_precheck -v +""" + +import json +import os +import subprocess +import sys +import unittest +from types import SimpleNamespace +from unittest import mock + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from driver import SVCompDriver as svcomp +from svcomp import PropertyPreCheck as precheck + +RESULT = {"exception_free": True, "reason": "no throw", "assertion_free": False, "assertion_reason": "Main.main: assert"} + + +def args(**kw): + a = dict(classpath=['/task/common', '/task/Main', '/libs/com.microsoft.z3.jar'], agent='/swat/executor.jar', + java_path='java', no_property_precheck=False) + a.update(kw) + return SimpleNamespace(**a) + + +def completed(stdout): + return subprocess.CompletedProcess(args=[], returncode=0, stdout=stdout, stderr='') + + +class PropertyPreCheckTest(unittest.TestCase): + + def run_check(self, prop, stdout=json.dumps(RESULT), **kw): + check = precheck.PropertyPreCheck(args(**kw), prop) + with mock.patch.object(precheck.subprocess, 'run', return_value=completed(stdout)) as run: + proven = check.run() + return check, proven, run + + def test_no_runtime_exception_uses_exception_freedom(self): + check, proven, _ = self.run_check('no-runtime-exception.prp') + self.assertTrue(proven) + self.assertEqual(check.status, 'proven') + self.assertEqual(check.reason, 'no throw') + + def test_valid_assert_uses_assertion_freedom(self): + check, proven, _ = self.run_check('valid-assert.prp') + self.assertFalse(proven) + self.assertEqual(check.status, 'not_proven') + self.assertEqual(check.reason, 'Main.main: assert') + + def test_command_leaves_out_z3(self): + _, _, run = self.run_check('no-runtime-exception.prp') + cmd = run.call_args[0][0] + self.assertEqual(cmd[:4], ['java', '-Xmx2g', '-cp', '/swat/executor.jar']) + self.assertEqual(cmd[-2:], ['/task/common', '/task/Main']) + + def test_other_property_and_flag_disable_it(self): + for check, proven, run in (self.run_check('no-deadlock.prp'), + self.run_check('no-runtime-exception.prp', no_property_precheck=True)): + self.assertFalse(proven) + self.assertEqual(check.status, 'disabled') + run.assert_not_called() + + def test_garbage_output_proves_nothing(self): + check, proven, _ = self.run_check('no-runtime-exception.prp', stdout='Exception in thread "main"') + self.assertFalse(proven) + self.assertEqual(check.status, 'failed') + + def test_timeout_proves_nothing(self): + check = precheck.PropertyPreCheck(args(), 'no-runtime-exception.prp') + with mock.patch.object(precheck.subprocess, 'run', side_effect=subprocess.TimeoutExpired('java', 60)): + self.assertFalse(check.run()) + self.assertEqual(check.status, 'timeout') + + +class VerdictWithProofTest(unittest.TestCase): + + def setUp(self): + self.errors = [] + db = SimpleNamespace(record_execution_error=lambda endpoint, kind, message: self.errors.append(kind)) + patcher = mock.patch.object(svcomp.Database, 'instance', return_value=db) + patcher.start() + self.addCleanup(patcher.stop) + self.driver = svcomp.SVCompDriver.__new__(svcomp.SVCompDriver) + self.driver.state = svcomp.State() + self.driver.precheck = SimpleNamespace(proven=True, reason='no throw') + + def test_safe_when_round_0_would_explore(self): + self.assertEqual(self.driver.verdict_with_proof(svcomp.Action.SYMBOLICNEXT), svcomp.Verdict.SAFE) + self.assertEqual(self.errors, []) + + def test_safe_when_round_0_gave_up(self): + self.driver.state.verdict = svcomp.Verdict.UNKNOWN + self.assertEqual(self.driver.verdict_with_proof(svcomp.Action.REPORTVERDICT), svcomp.Verdict.SAFE) + + def test_violation_contradicts_the_proof(self): + self.driver.state.verdict = svcomp.Verdict.VIOLATION + self.assertEqual(self.driver.verdict_with_proof(svcomp.Action.REPORTVERDICT), svcomp.Verdict.UNKNOWN) + self.assertEqual(self.errors, ['precheck_contradiction']) + + +if __name__ == '__main__': + unittest.main()