From 508db532aa25cab47a41e98389bd516949959c4e Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:01:34 +0000 Subject: [PATCH 1/7] Add a static check for uncaught RuntimeExceptions and AssertionErrors ExceptionFreedomCheck analyses every class on the program's classpath with ASM and proves, conservatively, that no RuntimeException can escape Main.main or a static initializer, and whether reachable code creates an AssertionError at all. It tracks nullness, int constants, array lengths, enum ordinals and runtime types through fields, parameters and return values (least fixpoints), treats only modelled library methods as callable and fails on anything it cannot model. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/staticcheck/AbsValue.java | 208 ++++ .../staticcheck/ExceptionFreedomCheck.java | 887 ++++++++++++++++++ .../its/swat/staticcheck/FactInterpreter.java | 277 ++++++ .../de/uzl/its/swat/staticcheck/JdkModel.java | 273 ++++++ .../de/uzl/its/swat/staticcheck/Program.java | 304 ++++++ .../ExceptionFreedomCheckSpec.groovy | 118 +++ 6 files changed, 2067 insertions(+) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy 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..d54ebbb7 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java @@ -0,0 +1,208 @@ +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 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 = 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 (!isThis && 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); + } + + AbsValue withLengthOf(String enumType) { + return new AbsValue(kind, size, constant, length, enumType, ordinalOf, exactType, staticType, isThis); + } + + 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) { + 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 && 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, 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"); + 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..db31ba74 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java @@ -0,0 +1,887 @@ +package de.uzl.its.swat.staticcheck; + +import java.nio.file.Path; +import java.util.*; +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 any static initializer: + * + *

+ * + *

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 { + 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; + } + if (f.value instanceof String) 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); + for (ClassNode c : program.appClasses()) { + Program.Method clinit = program.method(c.name, "", "()V"); + if (clinit != null) roots.add(clinit); + } + 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"; + for (Program.Method r : roots) { + 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. + */ + 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 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; + } + + /** 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) { + if (method == entry) return AbsValue.array(MAIN_DESC.substring(1, MAIN_DESC.indexOf(')')), null, null); + AbsValue[] params = parameterFacts.get(method.key); + 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).isThis) { + 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).isThis; + } + if (insn instanceof InvokeDynamicInsnNode) { + int n = Type.getArgumentTypes(((InvokeDynamicInsnNode) insn).desc).length; + for (int i = 0; i < n; i++) if (top(frame, i).isThis) 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).isThis) return true; + if (op == INVOKESTATIC || !top(frame, n).isThis) return false; + if (op != INVOKESPECIAL || !mi.name.equals("")) 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..8a4197e2 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java @@ -0,0 +1,273 @@ +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")); + + 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;", "toLowerCase()Ljava/lang/String;", "toUpperCase()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"); + add("java/lang/String", nonNull, fresh, "concat(Ljava/lang/String;)Ljava/lang/String;", + "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, nonNull, decl, "(Ljava/lang/String;)V"); + 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")); + } + + 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..d88b4ea9 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java @@ -0,0 +1,304 @@ +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; + 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); + } + } + + /** 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; + } + + /** A default method for name+desc in the application interfaces of a class (null if none). */ + private Method resolveDefault(String clazz, String name, String desc) { + 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()) return m; + } + return null; + } + + /** + * The targets of an invokevirtual/invokeinterface on an application owner type: the method each + * concrete application subtype of the owner resolves to. Returns null if some subtype resolves + * to a library method that is not one of the known methods of java/lang/Object or java/lang/Enum. + */ + 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; + String[] lib = new String[1]; + Method m = resolveInChain(sub, name, desc, lib); + if (m != null) { + if (m.hasCode()) t.methods.add(m); + else if ((m.node.access & Opcodes.ACC_NATIVE) != 0) return null; + // abstract in a concrete class cannot happen for verified classes + continue; + } + String declaring = lib[0] == null ? null : JdkModel.declaringClass(lib[0], name, desc); + if (declaring != null) { + t.libraryMethods.add(declaring + "." + name + desc); + continue; + } + if (lib[0] != null && !JdkModel.knowsMethodsOf(lib[0])) return null; + Method d = resolveDefault(sub, name, desc); + if (d != null) t.methods.add(d); + // else: AbstractMethodError, an Error + } + 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..573b7de9 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy @@ -0,0 +1,118 @@ +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') { + 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) + 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); } }' + } + + @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; } }' + } +} From 2273466a877682134c39a2b01c966e8b9753ff4f Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:01:34 +0000 Subject: [PATCH 2/7] Answer SAFE when the property pre-check proves the property For no-runtime-exception and valid-assert, the SV-COMP driver runs the executor jar's ExceptionFreedomCheck before round 0. If it proves the property, round 0 only cross-checks the proof (a violation found there makes the verdict UNKNOWN) and the verdict is SAFE without exploration and without the exploration's soundness downgrades. --no-property-precheck disables it. Co-Authored-By: Claude Opus 5.5 --- symbolic-explorer/SymbolicExplorer.py | 1 + symbolic-explorer/driver/SVCompDriver.py | 39 ++++++++-- symbolic-explorer/svcomp/PropertyPreCheck.py | 81 ++++++++++++++++++++ symbolic-explorer/svcomp/TestcaseStats.py | 9 ++- 4 files changed, 120 insertions(+), 10 deletions(-) create mode 100644 symbolic-explorer/svcomp/PropertyPreCheck.py 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: From c41571f9a1b22ed26a94b4fde371361c2927e5db Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:04:33 +0000 Subject: [PATCH 3/7] Test the property pre-check and the verdict it gives Co-Authored-By: Claude Opus 5.5 --- .../tests/test_property_precheck.py | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 symbolic-explorer/tests/test_property_precheck.py 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() From 3445d6473c9e082ebc4980ac70ac06d02da25f71 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:07:57 +0000 Subject: [PATCH 4/7] Check only the static initializers that may run A static initializer can only run if reachable code initializes its class (new, getstatic, putstatic, invokestatic, or a subclass being initialized), so unrelated classes on the classpath no longer make the check fail. Co-Authored-By: Claude Opus 5.5 --- .../staticcheck/ExceptionFreedomCheck.java | 36 +++++++++++++++---- 1 file changed, 29 insertions(+), 7 deletions(-) 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 index db31ba74..0fd2e86e 100644 --- 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 @@ -15,7 +15,7 @@ * 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 any static initializer: + * proves that no RuntimeException can escape {@code main} or a static initializer that may run: * *

    *
  • Every instruction that the JVM specification lets throw a RuntimeException (array access @@ -136,10 +136,7 @@ Result run() throws AnalyzerException { List roots = new ArrayList<>(); roots.add(entry); - for (ClassNode c : program.appClasses()) { - Program.Method clinit = program.method(c.name, "", "()V"); - if (clinit != null) roots.add(clinit); - } + 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. @@ -152,7 +149,12 @@ Result run() throws AnalyzerException { 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"; - for (Program.Method r : roots) { + // 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", @@ -186,7 +188,9 @@ else if (insns[i].getOpcode() == INVOKESPECIAL && ((MethodInsnNode) insns[i]).na * 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. + * 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); @@ -200,6 +204,10 @@ private String openWorldCall(List roots, Set rea if (f[i] == null) continue; if (insns[i] instanceof InvokeDynamicInsnNode && !isStringConcat((InvokeDynamicInsnNode) insns[i])) return m.key + ": line " + line(insns[i]) + ": invokedynamic"; + 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]); @@ -211,6 +219,20 @@ private String openWorldCall(List roots, Set rea 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(); From d0d735798f72dc6fecfd87302b27ad7e1a1cf0eb Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:32:40 +0000 Subject: [PATCH 5/7] Close soundness gaps in the exception-freedom check - Virtual dispatch over-approximates JVM selection: every non-private instance method of the superclass chain and every default method of the superinterfaces counts (package-private overriding, private and maximally-specific default methods were resolved wrongly). - The receiver-escape rule uses a may-alias flag that survives joins. - Main.main's parameter also joins the arguments of calls to main. - ConstantValue only initializes static fields. - ldc of method handles and dynamic constants counts as unknown code. - Classes in java/ are never application classes. - String.concat/toLowerCase/toUpperCase and new StringBuilder(String) are no longer modelled: on JDK 8 they overflow for huge strings. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/staticcheck/AbsValue.java | 28 ++++++++-- .../staticcheck/ExceptionFreedomCheck.java | 26 ++++++--- .../de/uzl/its/swat/staticcheck/JdkModel.java | 8 +-- .../de/uzl/its/swat/staticcheck/Program.java | 56 +++++++++++-------- .../ExceptionFreedomCheckSpec.groovy | 6 ++ 5 files changed, 83 insertions(+), 41 deletions(-) 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 index d54ebbb7..5fb9b97f 100644 --- 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 @@ -41,6 +41,8 @@ enum Kind { 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). @@ -59,6 +61,12 @@ enum Kind { 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; @@ -110,16 +118,16 @@ static AbsValue caught(String type, int handler) { /** The same value without the facts that only hold where it was computed (receiver, handler). */ AbsValue escaped() { - if (!isThis && caughtBy < 0) return this; + 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); + 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); + return new AbsValue(kind, size, constant, length, enumType, ordinalOf, exactType, staticType, isThis, caughtBy, mayBeThis); } boolean isBottom() { @@ -146,6 +154,15 @@ public int getSize() { /** 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; @@ -180,7 +197,7 @@ 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 && caughtBy == v.caughtBy + 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) @@ -189,7 +206,7 @@ public boolean equals(Object o) { @Override public int hashCode() { - return Objects.hash(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, caughtBy); + return Objects.hash(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, mayBeThis, caughtBy); } @Override @@ -202,6 +219,7 @@ public String toString() { 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 index 0fd2e86e..5ecb6359 100644 --- 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 @@ -2,6 +2,8 @@ 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.*; @@ -101,7 +103,8 @@ Result run() throws AnalyzerException { fieldFacts.put(key, AbsValue.prim(t.getSize())); continue; } - if (f.value instanceof String) fieldFacts.put(key, AbsValue.exact("java/lang/String")); + // 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); } } @@ -204,6 +207,9 @@ private String openWorldCall(List roots, Set rea 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)); @@ -332,8 +338,12 @@ public AbsValue field(FieldInsnNode insn) { @Override public AbsValue parameter(Program.Method method, int index, Type type) { - if (method == entry) return AbsValue.array(MAIN_DESC.substring(1, MAIN_DESC.indexOf(')')), null, null); 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]; } @@ -519,7 +529,7 @@ private boolean instanceFieldInitializedFirst(ClassNode c, FieldNode f) throws A 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).isThis) { + && !top(frame, 0).mayBeThis) { assigned = true; break; } @@ -545,19 +555,19 @@ private boolean assigns(FieldInsnNode fi, ClassNode c, FieldNode f) { 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).isThis; + 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).isThis) return true; + 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).isThis) return true; - if (op == INVOKESTATIC || !top(frame, n).isThis) return false; - if (op != INVOKESPECIAL || !mi.name.equals("")) return true; + 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); 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 index 8a4197e2..a05475a9 100644 --- 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 @@ -185,7 +185,7 @@ private static void addExact(String owner, Condition c, Returns r, String... met "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;", "toLowerCase()Ljava/lang/String;", "toUpperCase()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"); @@ -194,15 +194,15 @@ private static void addExact(String owner, Condition c, Returns r, String... met "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"); - add("java/lang/String", nonNull, fresh, "concat(Ljava/lang/String;)Ljava/lang/String;", - "valueOf([C)Ljava/lang/String;"); + // 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, nonNull, decl, "(Ljava/lang/String;)V"); 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); 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 index d88b4ea9..a35826c1 100644 --- 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 @@ -97,8 +97,9 @@ static final class Targets { 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; + // The first definition on the classpath wins, as for the JVM's class loader. Classes in + // java/ are always the platform's own. + if (classes.containsKey(c.name) || c.name.startsWith("java/")) return; classes.put(c.name, c); if (c.name.startsWith(VERIFIER_PACKAGE)) return; for (MethodNode m : c.methods) { @@ -221,21 +222,27 @@ Method resolveInChain(String owner, String name, String desc, String[] libraryOw return null; } - /** A default method for name+desc in the application interfaces of a class (null if none). */ - private Method resolveDefault(String clazz, String name, String desc) { + /** 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()) return m; + if (m != null && m.hasCode() && !m.isStatic() && (m.node.access & Opcodes.ACC_PRIVATE) == 0) out.add(m); } - return null; + return out; } /** - * The targets of an invokevirtual/invokeinterface on an application owner type: the method each - * concrete application subtype of the owner resolves to. Returns null if some subtype resolves - * to a library method that is not one of the known methods of java/lang/Object or java/lang/Enum. + * 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 whose methods are unknown + * might provide it. */ Targets virtualTargets(String owner, String name, String desc) { Targets t = new Targets(); @@ -249,23 +256,24 @@ Targets virtualTargets(String owner, String name, String desc) { for (String sub : appSubtypes(owner)) { ClassNode c = classes.get(sub); if ((c.access & (Opcodes.ACC_ABSTRACT | Opcodes.ACC_INTERFACE)) != 0) continue; - String[] lib = new String[1]; - Method m = resolveInChain(sub, name, desc, lib); - if (m != null) { + 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); - else if ((m.node.access & Opcodes.ACC_NATIVE) != 0) return null; - // abstract in a concrete class cannot happen for verified classes - continue; - } - String declaring = lib[0] == null ? null : JdkModel.declaringClass(lib[0], name, desc); - if (declaring != null) { - t.libraryMethods.add(declaring + "." + name + desc); - continue; + if ((m.node.access & (Opcodes.ACC_PUBLIC | Opcodes.ACC_PROTECTED)) != 0) overridesLibrary = true; } - if (lib[0] != null && !JdkModel.knowsMethodsOf(lib[0])) return null; - Method d = resolveDefault(sub, name, desc); - if (d != null) t.methods.add(d); - // else: AbstractMethodError, an Error + t.methods.addAll(defaults(sub, name, desc)); + if (lib == null || overridesLibrary) 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; } 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 index 573b7de9..21ffa1e7 100644 --- 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 @@ -92,6 +92,12 @@ public interface ObjectFactory { T createObject(); } '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()); } }' } @Unroll From 16754245c2d633a7004c487ffbdc25586e6d6860 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:47:19 +0000 Subject: [PATCH 6/7] Treat calls that a library default method may serve as unknown A concrete class that implements a library interface may inherit one of its default methods (Iterator.remove, Iterable.forEach, CharSequence.isEmpty), which can throw or call back into the application. Such calls now have unknown targets, unless the interface is known to have no default methods. Platform packages (javax/, jdk/, sun/) are never application classes. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/staticcheck/JdkModel.java | 10 +++++++++- .../de/uzl/its/swat/staticcheck/Program.java | 20 +++++++++++++++---- .../ExceptionFreedomCheckSpec.groovy | 3 +++ 3 files changed, 28 insertions(+), 5 deletions(-) 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 index a05475a9..79f64a51 100644 --- 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 @@ -93,7 +93,7 @@ private static void addExact(String owner, Condition c, Returns r, String... met 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")); + "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")); @@ -267,6 +267,14 @@ 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 index a35826c1..e9a3cdc5 100644 --- 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 @@ -99,7 +99,7 @@ private void add(InputStream in) throws IOException { new ClassReader(in).accept(c, ClassReader.SKIP_FRAMES); // The first definition on the classpath wins, as for the JVM's class loader. Classes in // java/ are always the platform's own. - if (classes.containsKey(c.name) || c.name.startsWith("java/")) return; + if (classes.containsKey(c.name) || isPlatformPackage(c.name)) return; classes.put(c.name, c); if (c.name.startsWith(VERIFIER_PACKAGE)) return; for (MethodNode m : c.methods) { @@ -108,6 +108,11 @@ private void add(InputStream in) throws IOException { } } + /** Packages the JVM always loads from the platform, never from the classpath. */ + private static boolean isPlatformPackage(String name) { + return name.startsWith("java/") || name.startsWith("javax/") || name.startsWith("jdk/") || name.startsWith("sun/"); + } + /** 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); @@ -241,8 +246,8 @@ private List defaults(String clazz, String name, String desc) { * 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 whose methods are unknown - * might provide it. + * 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(); @@ -270,7 +275,14 @@ Targets virtualTargets(String owner, String name, String desc) { if ((m.node.access & (Opcodes.ACC_PUBLIC | Opcodes.ACC_PROTECTED)) != 0) overridesLibrary = true; } t.methods.addAll(defaults(sub, name, desc)); - if (lib == null || overridesLibrary) continue; + 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; 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 index 21ffa1e7..322f56cd 100644 --- 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 @@ -98,6 +98,9 @@ public interface ObjectFactory { T createObject(); } '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(); } }' } @Unroll From 9cd00a6dd31a8cee5e0a83d1a8477db7ddc3907f Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:17:19 +0000 Subject: [PATCH 7/7] Fail the check when the JVM would not load the classpath as modelled A class on the classpath in a platform package (java/, javax/, jdk/, sun/, and the JDK 8 packages org/xml/, org/w3c/, org/omg/, org/ietf/, org/jcp/, com/sun/), in a package of the JDK's boot modules, or in the Verifier package other than Verifier and ObjectFactory, is refused or shadowed by the JVM, or would run its static initializer unanalysed. Such programs are no longer proven. Co-Authored-By: Claude Opus 5.5 --- .../staticcheck/ExceptionFreedomCheck.java | 1 + .../de/uzl/its/swat/staticcheck/Program.java | 49 ++++++++++++++++--- .../ExceptionFreedomCheckSpec.groovy | 27 +++++++++- 3 files changed, 70 insertions(+), 7 deletions(-) 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 index 5ecb6359..bf750356 100644 --- 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 @@ -91,6 +91,7 @@ public static Result check(List classpath) { } 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"); 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 index e9a3cdc5..b99e2b8d 100644 --- 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 @@ -97,9 +97,9 @@ static final class Targets { 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. Classes in - // java/ are always the platform's own. - if (classes.containsKey(c.name) || isPlatformPackage(c.name)) return; + // 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) { @@ -108,9 +108,46 @@ private void add(InputStream in) throws IOException { } } - /** Packages the JVM always loads from the platform, never from the classpath. */ - private static boolean isPlatformPackage(String name) { - return name.startsWith("java/") || name.startsWith("javax/") || name.startsWith("jdk/") || name.startsWith("sun/"); + /** + * 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). */ 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 index 322f56cd..038e9251 100644 --- 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 @@ -35,13 +35,17 @@ public interface ObjectFactory { T createObject(); } @TempDir Path dir - ExceptionFreedomCheck.Result check(String main, String release = '8') { + 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, @@ -103,6 +107,27 @@ public interface ObjectFactory { T createObject(); } '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: