Repository navigation
Soundness: try/catch is checked as if the catch block always runs #364
Description
Impact: a real bug passes verification (false negative).
Description
The verifier checks try and catch blocks one after the other, so after a try/catch a variable keeps whatever the catch block last assigned. The path where the try finishes normally is lost. An if/else instead merges both branches after the join, and try/catch should be merged the same way.
Also, an exception can be thrown at any point in the try. The catch block should therefore not assume the try ran to completion, or that it never ran at all.
Minimal reproducer
import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;
@ExternalRefinementsFor("java.lang.Throwable")
@StateSet({"withThrowable", "noThrowable"})
interface ThrowableRefinements {
@StateRefinement(to = "noThrowable(this)")
void Throwable(String message);
@StateRefinement(to = "withThrowable(this)")
void Throwable(String message, Throwable cause);
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
Throwable initCause(Throwable cause);
}
public class Repro {
static void load() throws Exception { throw new Exception("x"); }
static void m() {
Throwable t = new Throwable("start");
try {
load();
t = new Throwable("try", new RuntimeException()); // withThrowable
} catch (Exception e) {
t = new Throwable("catch"); // noThrowable
}
t.initCause(new RuntimeException()); // not reported, but t is withThrowable if load() returns
}
}Expected: a State Refinement Error on t.initCause(...), because t may be withThrowable.
Actual: Correct! Passed Verification.
Same bug with value refinements
static void m() {
int y = 0;
try {
load();
y = -5;
} catch (Exception e) {
y = 7;
}
@Refinement("_ > 0")
int z = y; // not reported, but y == -5 if load() returns
}Actual: Correct! Passed Verification. If the values are swapped (5 in the try, -5 in the catch), the error is reported, but as z == -5 is not a subtype of z > 0: only the catch path is considered.
Activity
Combine try, catch and finally blocks soundly (#364)
Combine try, catch and finally blocks soundly (#364)
Combine try, catch and finally blocks soundly (#366)