Guards: Add support for wrappers that may throw exceptions.

This commit is contained in:
Anders Schack-Mulligen
2025-07-23 15:31:34 +02:00
parent b156bd5ce2
commit f90b6ab005
4 changed files with 33 additions and 0 deletions

View File

@@ -146,6 +146,8 @@ private module GuardsInput implements SharedGuards::InputSig<Location> {
class ControlFlowNode = J::ControlFlowNode;
class NormalExitNode = ControlFlow::NormalExitNode;
class BasicBlock = J::BasicBlock;
predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }

View File

@@ -202,4 +202,14 @@ public class Guards {
break;
}
}
static void ensureNotNull(Object o) throws Exception {
if (o == null) throw new Exception();
}
void testExceptionWrapper(String s) throws Exception {
chk(); // nothing guards here
ensureNotNull(s);
chk(); // $ guarded='ensureNotNull(...):no exception' guarded='s:not null'
}
}

View File

@@ -112,3 +112,5 @@
| Guards.java:201:9:201:13 | chk(...) | 'testEnumWrapper(...):FAILURE' |
| Guards.java:201:9:201:13 | chk(...) | 'testEnumWrapper(...):match FAILURE' |
| Guards.java:201:9:201:13 | chk(...) | g(1):false |
| Guards.java:213:5:213:9 | chk(...) | 'ensureNotNull(...):no exception' |
| Guards.java:213:5:213:9 | chk(...) | 's:not null' |

View File

@@ -79,6 +79,9 @@ signature module InputSig<LocationSig Location> {
Location getLocation();
}
/** A control flow node indicating normal termination of a callable. */
class NormalExitNode extends ControlFlowNode;
/**
* A basic block, that is, a maximal straight-line sequence of control flow nodes
* without branches or joins.
@@ -520,6 +523,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
)
}
private predicate normalExitBlock(BasicBlock bb) { bb.getNode(_) instanceof NormalExitNode }
signature module LogicInputSig {
class SsaDefinition {
/** Gets the basic block to which this SSA definition belongs. */
@@ -1047,6 +1052,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
)
}
private predicate guardDirectlyControlsExit(Guard guard, GuardValue val) {
exists(BasicBlock bb |
guard.directlyValueControls(bb, val) and
normalExitBlock(bb)
)
}
/**
* Gets a non-overridable method that performs a check on the `ppos`th
* parameter. A return value equal to `retval` allows us to conclude
@@ -1064,6 +1076,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
|
validReturnInCustomGuard(ret, ppos, retval, val)
)
or
exists(SsaDefinition param, Guard g0, GuardValue v0 |
parameterDefinition(result.getParameter(ppos), param) and
guardDirectlyControlsExit(g0, v0) and
retval = TException(false) and
BranchImplies::ssaControls(param, val, g0, v0)
)
}
/**