Skip to content

Commit 25c0e7f

Browse files
mtdowlingmtdowling
committed
Add BddVerifier
1 parent 3c690a5 commit 25c0e7f

File tree

2 files changed

+355
-0
lines changed

2 files changed

+355
-0
lines changed

‎smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/language/syntax/parameters/Parameters.java

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
package software.amazon.smithy.rulesengine.language.syntax.parameters;
66

77
import java.util.ArrayList;
8+
import java.util.Collections;
89
import java.util.Iterator;
910
import java.util.List;
1011
import java.util.Map;
@@ -76,6 +77,15 @@ public void writeToScope(Scope<Type> scope) {
7677
}
7778
}
7879

80+
/**
81+
* Convert the Parameters container to a list.
82+
*
83+
* @return the parameters list.
84+
*/
85+
public List<Parameter> toList() {
86+
return Collections.unmodifiableList(parameters);
87+
}
88+
7989
@Override
8090
public SourceLocation getSourceLocation() {
8191
return sourceLocation;

‎smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/logic/bdd/BddEquivalenceChecker.java

Lines changed: 345 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,345 @@
1+
package software.amazon.smithy.rulesengine.logic.bdd;
2+
3+
import java.time.Duration;
4+
import java.util.ArrayList;
5+
import java.util.HashMap;
6+
import java.util.HashSet;
7+
import java.util.List;
8+
import java.util.Map;
9+
import java.util.Set;
10+
import java.util.logging.Logger;
11+
import software.amazon.smithy.rulesengine.language.syntax.parameters.Parameter;
12+
import software.amazon.smithy.rulesengine.language.syntax.rule.Condition;
13+
import software.amazon.smithy.rulesengine.language.syntax.rule.NoMatchRule;
14+
import software.amazon.smithy.rulesengine.language.syntax.rule.Rule;
15+
import software.amazon.smithy.rulesengine.logic.ConditionEvaluator;
16+
import software.amazon.smithy.rulesengine.logic.cfg.Cfg;
17+
import software.amazon.smithy.rulesengine.logic.cfg.CfgNode;
18+
import software.amazon.smithy.rulesengine.logic.cfg.ConditionNode;
19+
import software.amazon.smithy.rulesengine.logic.cfg.ResultNode;
20+
21+
/**
22+
* Verifies functional equivalence between a CFG and its BDD representation.
23+
*
24+
* <p>This verifier uses structural equivalence checking to ensure that for every possible
25+
* combination of condition evaluations, both representations produce the same result.
26+
*/
27+
public final class BddEquivalenceChecker {
28+
29+
private static final Logger LOGGER = Logger.getLogger(BddEquivalenceChecker.class.getName());
30+
31+
private static final int EXHAUSTIVE_THRESHOLD = 20;
32+
private static final int DEFAULT_MAX_SAMPLES = 1_000_000;
33+
private static final Duration DEFAULT_TIMEOUT = Duration.ofMinutes(1);
34+
35+
private final Cfg cfg;
36+
private final Bdd bdd;
37+
private final List<Parameter> parameters;
38+
private final Map<Condition, Integer> conditionToIndex = new HashMap<>();
39+
40+
private int maxSamples = DEFAULT_MAX_SAMPLES;
41+
private Duration timeout = DEFAULT_TIMEOUT;
42+
43+
private int testsRun = 0;
44+
private long startTime;
45+
46+
public static BddEquivalenceChecker of(Cfg cfg, Bdd bdd) {
47+
return new BddEquivalenceChecker(cfg, bdd);
48+
}
49+
50+
private BddEquivalenceChecker(Cfg cfg, Bdd bdd) {
51+
this.cfg = cfg;
52+
this.bdd = bdd;
53+
this.parameters = new ArrayList<>(cfg.getRuleSet().getParameters().toList());
54+
55+
for (int i = 0; i < bdd.getConditions().size(); i++) {
56+
conditionToIndex.put(bdd.getConditions().get(i), i);
57+
}
58+
}
59+
60+
/**
61+
* Sets the maximum number of samples to test for large condition sets.
62+
*
63+
* <p>Defaults to a max of 1M samples. Set to <= 0 to disable the max.
64+
*
65+
* @param maxSamples the maximum number of samples
66+
* @return this verifier for method chaining
67+
*/
68+
public BddEquivalenceChecker setMaxSamples(int maxSamples) {
69+
if (maxSamples < 1) {
70+
maxSamples = Integer.MAX_VALUE;
71+
}
72+
this.maxSamples = maxSamples;
73+
return this;
74+
}
75+
76+
/**
77+
* Sets the maximum amount of time to take for the verification (runs until timeout or max samples met).
78+
*
79+
* <p>Defaults to a 1-minute timeout if not overridden.
80+
*
81+
* @param timeout the timeout duration
82+
* @return this verifier for method chaining
83+
*/
84+
public BddEquivalenceChecker setMaxDuration(Duration timeout) {
85+
this.timeout = timeout;
86+
return this;
87+
}
88+
89+
/**
90+
* Verifies that the BDD produces identical results to the CFG.
91+
*
92+
* @throws VerificationException if any discrepancy is found
93+
*/
94+
public void verify() {
95+
startTime = System.currentTimeMillis();
96+
verifyResults();
97+
testsRun = 0;
98+
99+
LOGGER.info(() -> String.format("Verifying BDD with %d conditions (max samples: %d, timeout: %s)",
100+
bdd.getConditionCount(), maxSamples, timeout));
101+
102+
if (bdd.getConditionCount() <= EXHAUSTIVE_THRESHOLD) {
103+
verifyExhaustive();
104+
} else {
105+
verifyWithLimits();
106+
}
107+
108+
LOGGER.info(String.format("BDD verification passed: %d tests in %s", testsRun, getElapsedDuration()));
109+
}
110+
111+
private void verifyResults() {
112+
Set<Rule> cfgResults = new HashSet<>();
113+
for (CfgNode node : cfg) {
114+
if (node instanceof ResultNode) {
115+
Rule result = ((ResultNode) node).getResult();
116+
if (result != null) {
117+
cfgResults.add(result);
118+
}
119+
}
120+
}
121+
122+
// Remove the NoMatchRule that's added by default. It's not in the CFG.
123+
Set<Rule> bddResults = new HashSet<>(bdd.getResults());
124+
bddResults.removeIf(v -> v == NoMatchRule.INSTANCE);
125+
126+
if (!cfgResults.equals(bddResults)) {
127+
Set<Rule> inCfgOnly = new HashSet<>(cfgResults);
128+
inCfgOnly.removeAll(bddResults);
129+
Set<Rule> inBddOnly = new HashSet<>(bddResults);
130+
inBddOnly.removeAll(cfgResults);
131+
throw new IllegalStateException(String.format(
132+
"Result mismatch: CFG has %d results, BDD has %d results (excluding NoMatchRule).\n" +
133+
"In CFG only: %s\n" +
134+
"In BDD only: %s",
135+
cfgResults.size(), bddResults.size(), inCfgOnly, inBddOnly
136+
));
137+
}
138+
}
139+
140+
/**
141+
* Exhaustively tests all possible condition combinations.
142+
*/
143+
private void verifyExhaustive() {
144+
long totalCombinations = 1L << bdd.getConditionCount();
145+
LOGGER.info(() -> "Running exhaustive verification with " + totalCombinations + " combinations");
146+
for (long mask = 0; mask < totalCombinations; mask++) {
147+
verifyCase(mask);
148+
if (hasEitherLimitBeenExceeded()) {
149+
LOGGER.info(String.format("Exhaustive verification stopped after %d tests "
150+
+ "(limit: %d samples or %s timeout)", testsRun, maxSamples, timeout));
151+
break;
152+
}
153+
}
154+
}
155+
156+
/**
157+
* Verifies with configured limits (samples and timeout).
158+
* Continues until EITHER limit is reached: maxSamples reached OR timeout exceeded.
159+
*/
160+
private void verifyWithLimits() {
161+
LOGGER.info(() -> String.format("Running limited verification (will stop at %d samples OR %s timeout)",
162+
maxSamples, timeout));
163+
verifyCriticalCases();
164+
165+
while (!hasEitherLimitBeenExceeded()) {
166+
long mask = randomMask();
167+
verifyCase(mask);
168+
if (testsRun % 10000 == 0 && testsRun > 0) {
169+
LOGGER.fine(() -> String.format("Progress: %d tests run, %s elapsed", testsRun, getElapsedDuration()));
170+
}
171+
}
172+
173+
LOGGER.info(() -> String.format("Verification complete: %d tests run in %s", testsRun, getElapsedDuration()));
174+
}
175+
176+
/**
177+
* Tests critical edge cases that are likely to expose bugs.
178+
*/
179+
private void verifyCriticalCases() {
180+
LOGGER.fine("Testing critical edge cases");
181+
182+
// All conditions false
183+
verifyCase(0);
184+
185+
// All conditions true
186+
verifyCase((1L << bdd.getConditionCount()) - 1);
187+
188+
// Each condition true individually
189+
for (int i = 0; i < bdd.getConditionCount() && !hasEitherLimitBeenExceeded(); i++) {
190+
verifyCase(1L << i);
191+
}
192+
193+
// Each condition false individually (all others true)
194+
long allTrue = (1L << bdd.getConditionCount()) - 1;
195+
for (int i = 0; i < bdd.getConditionCount() && !hasEitherLimitBeenExceeded(); i++) {
196+
verifyCase(allTrue ^ (1L << i));
197+
}
198+
199+
// Alternating patterns
200+
if (!hasEitherLimitBeenExceeded()) {
201+
verifyCase(0x5555555555555555L & ((1L << bdd.getConditionCount()) - 1));
202+
}
203+
204+
if (!hasEitherLimitBeenExceeded()) {
205+
verifyCase(0xAAAAAAAAAAAAAAAAL & ((1L << bdd.getConditionCount()) - 1));
206+
}
207+
}
208+
209+
private boolean hasEitherLimitBeenExceeded() {
210+
return testsRun >= maxSamples || isTimedOut();
211+
}
212+
213+
private boolean isTimedOut() {
214+
return getElapsedDuration().compareTo(timeout) >= 0;
215+
}
216+
217+
private Duration getElapsedDuration() {
218+
return Duration.ofMillis(System.currentTimeMillis() - startTime);
219+
}
220+
221+
private void verifyCase(long mask) {
222+
testsRun++;
223+
224+
// Create evaluators that will return fixed values for conditions
225+
FixedMaskEvaluator maskEvaluator = new FixedMaskEvaluator(mask);
226+
Rule cfgResult = evaluateCfgWithMask(maskEvaluator);
227+
Rule bddResult = evaluateBdd(mask);
228+
229+
if (!resultsEqual(cfgResult, bddResult)) {
230+
StringBuilder errorMsg = new StringBuilder();
231+
errorMsg.append("BDD verification mismatch found!\n");
232+
errorMsg.append("Test case #").append(testsRun).append("\n");
233+
errorMsg.append("Condition mask: ").append(Long.toBinaryString(mask)).append("\n");
234+
errorMsg.append("\nCondition details:\n");
235+
for (int i = 0; i < bdd.getConditions().size(); i++) {
236+
Condition condition = bdd.getConditions().get(i);
237+
boolean value = (mask & (1L << i)) != 0;
238+
errorMsg.append(" Condition ").append(i).append(" [").append(value).append("]: ")
239+
.append(condition).append("\n");
240+
}
241+
errorMsg.append("\nResults:\n");
242+
errorMsg.append(" CFG result: ").append(describeResult(cfgResult)).append("\n");
243+
errorMsg.append(" BDD result: ").append(describeResult(bddResult));
244+
throw new VerificationException(errorMsg.toString());
245+
}
246+
}
247+
248+
private Rule evaluateCfgWithMask(ConditionEvaluator maskEvaluator) {
249+
CfgNode result = evaluateCfgNode(cfg.getRoot(), conditionToIndex, maskEvaluator);
250+
if (result instanceof ResultNode) {
251+
return ((ResultNode) result).getResult();
252+
}
253+
254+
return null;
255+
}
256+
257+
// Recursively evaluates a CFG node.
258+
private CfgNode evaluateCfgNode(CfgNode node, Map<Condition, Integer> conditionToIndex,
259+
ConditionEvaluator maskEvaluator) {
260+
if (node instanceof ResultNode) {
261+
return node;
262+
}
263+
264+
if (node instanceof ConditionNode) {
265+
ConditionNode condNode = (ConditionNode) node;
266+
Condition condition = condNode.getCondition().getCondition();
267+
268+
Integer index = conditionToIndex.get(condition);
269+
if (index == null) {
270+
throw new IllegalStateException("Condition not found in BDD: " + condition);
271+
}
272+
273+
boolean conditionResult = maskEvaluator.test(index);
274+
275+
// Handle negation if the condition reference is negated
276+
if (condNode.getCondition().isNegated()) {
277+
conditionResult = !conditionResult;
278+
}
279+
280+
// Follow the appropriate branch
281+
if (conditionResult) {
282+
return evaluateCfgNode(condNode.getTrueBranch(), conditionToIndex, maskEvaluator);
283+
} else {
284+
return evaluateCfgNode(condNode.getFalseBranch(), conditionToIndex, maskEvaluator);
285+
}
286+
}
287+
288+
throw new IllegalStateException("Unknown CFG node type: " + node);
289+
}
290+
291+
private Rule evaluateBdd(long mask) {
292+
FixedMaskEvaluator evaluator = new FixedMaskEvaluator(mask);
293+
BddEvaluator bddEvaluator = BddEvaluator.from(bdd);
294+
int resultIndex = bddEvaluator.evaluate(evaluator);
295+
return resultIndex < 0 ? null : bdd.getResults().get(resultIndex);
296+
}
297+
298+
private boolean resultsEqual(Rule r1, Rule r2) {
299+
if (r1 == r2) {
300+
return true;
301+
} else if (r1 == null || r2 == null) {
302+
return false;
303+
} else {
304+
return r1.withoutConditions().equals(r2.withoutConditions());
305+
}
306+
}
307+
308+
// Generates a random bit mask for sampling.
309+
private long randomMask() {
310+
long mask = 0;
311+
for (int i = 0; i < bdd.getConditionCount(); i++) {
312+
if (Math.random() < 0.5) {
313+
mask |= (1L << i);
314+
}
315+
}
316+
return mask;
317+
}
318+
319+
private String describeResult(Rule rule) {
320+
return rule == null ? "null (no match)" : rule.toString();
321+
}
322+
323+
// A condition evaluator that returns values based on a fixed bit mask.
324+
private static class FixedMaskEvaluator implements ConditionEvaluator {
325+
private final long mask;
326+
327+
FixedMaskEvaluator(long mask) {
328+
this.mask = mask;
329+
}
330+
331+
@Override
332+
public boolean test(int conditionIndex) {
333+
return (mask & (1L << conditionIndex)) != 0;
334+
}
335+
}
336+
337+
/**
338+
* Exception thrown when verification fails.
339+
*/
340+
public static class VerificationException extends RuntimeException {
341+
public VerificationException(String message) {
342+
super(message);
343+
}
344+
}
345+
}

0 commit comments

Comments
 (0)