[Strata] Better isolation of non-determinism in Core#617
[Strata] Better isolation of non-determinism in Core#617MikaelMayer wants to merge 6 commits intomainfrom
Conversation
Introduce ExprOrNondet type to unify deterministic and non-deterministic expressions in Imperative commands. Merge Cmd.havoc into Cmd.set with ExprOrNondet.nondet, and change Cmd.init to use ExprOrNondet instead of Option. Update all downstream consumers including backends, transforms, languages, and tests.
Add ExprOrNondet.map helper function and use it in places that manually match on .det/.nondet to transform the inner expression.
| | .cover _ _ md => | ||
| throw s!"{Imperative.MetaData.formatFileRangeD md}\ | ||
| cover unimplemented" | ||
| | .havoc _ md => |
There was a problem hiding this comment.
Let's make sure we keep .havoc as a definition accepting the name and metadata so that the .set ... .nondet can be built and deconstructed with .havoc .... for better hypothetical compatibility, but everything rewritten in this PR should prefer .set so don't undo your changes.
There was a problem hiding this comment.
The .havoc abbreviation is preserved at both the Cmd level (via the HasHavoc class which builds .set name .nondet md) and the Statement level (via Statement.havoc which is a @[match_pattern] abbreviation). All rewritten code in this PR uses .set ... .nondet directly, but .havoc remains available for construction and pattern matching.
| -- variable name mapping. | ||
| IdMap.updateVars map [(n1.name,n2.name)] | ||
| | .cmd (.set n1 e1 _), .cmd (.set n2 e2 _) => | ||
| | .cmd (.set n1 (.det e1) _), .cmd (.set n2 (.det e2) _) => |
There was a problem hiding this comment.
Ok I looked at the entire PR it's good. I would also like to see in Stmt that the condition of an if as well as the condition of the while loop also use ExprOrNondet.
And since these two are new, we need a syntax in Core to parse them, I suggest using a single star in the DDM to indicate nondeterminism like if * { } else { } and while * { ... }
And I want to see tests that make sure that these last two constructs are tested until verification. In the partial evaluator, for the if * we would introduce a fresh boolean. For the loop elimination phase, we would introduce a fresh boolean with a nondet RHS and set it at the end of the loop with a nondet RHS for now, until we have better.
There was a problem hiding this comment.
Addressed all three points:
-
ExprOrNondet in Stmt.ite/Stmt.loop: Done - both
iteandloopconditions inStmtnow useExprOrNondet Pinstead ofP.Expr. All downstream code (semantics, transforms, backends, tests) updated. -
DDM syntax
if (*)andwhile (*): Addedbstarexpression (*) to the Core grammar. The DDM translator recognizesif (*) { } else { }andwhile (*) { ... }and producesExprOrNondet.nondet. The ASTtoCST round-trips usingbstaras well. AddedExamples/NondetCond.core.stdemonstrating the syntax. -
Fresh boolean in partial evaluator: Updated
processIteBranchesNondetto introduce a fresh boolean variable ($__nondet_cond_N) with a nondet RHS (init ... .nondet), then use it as the condition for the ite in the output. Path conditions are set up using this fresh variable for proper path splitting.
Extend the non-determinism isolation from Cmd (init/set) to Stmt (ite/loop) by changing their condition/guard fields from P.Expr to ExprOrNondet P. This allows if-then-else and while-loop constructs to have non-deterministic conditions, where the branch or loop iteration is chosen arbitrarily. Changes: - Stmt.ite condition: P.Expr → ExprOrNondet P - Stmt.loop guard: P.Expr → ExprOrNondet P - Added ite_nondet_true_sem/ite_nondet_false_sem to big-step semantics - Added step_ite_nondet_true/false and step_loop_nondet_enter/exit to small-step semantics - Updated DetToNondet transform to handle nondet conditions - Updated LoopElim transform to handle nondet guards - Updated all language frontends (Core, C_Simp, Boole, Laurel, Python) to wrap deterministic conditions with .det - Updated all backends (CBMC, GOTO) to handle ExprOrNondet - Updated correctness proofs (DetToNondetCorrect, StatementSemanticsProps) - Updated all affected tests Closes #612
| [ | ||
| .init "x" t[int] (.det eb[#0]) .empty, | ||
| .ite eb[x == #3] | ||
| .ite (.det eb[x == #3]) |
There was a problem hiding this comment.
I see no test with .ite (.nondet) and .loop(.nondet). Also, where is the concrete syntax represented for nondet if and nondet loop ? I couldn't find where the new syntax was defined.
Add 'bstar' (*) expression to Core grammar for non-deterministic conditions in if/while statements. The DDM translator recognizes if (*) and while (*) and produces ExprOrNondet.nondet. Update the partial evaluator to introduce a fresh boolean variable for non-deterministic if conditions, enabling proper path splitting with path conditions. Add NondetCond.core.st example demonstrating the syntax.
1 participant
Summary
Completes the isolation of non-determinism in the Strata Core dialect by extending
ExprOrNondetfrom commands (init/set) to statement-level constructs (ite/loop).Problem
The previous commits on this branch replaced
Option/havocwithExprOrNondetinCmd, butStmt.iteandStmt.loopstill usedP.Exprfor their conditions/guards. This meant non-deterministic branching and looping could only be expressed indirectly.Solution
Changed
Stmt.iteandStmt.loopto useExprOrNondet Pfor their condition/guard fields. When the condition is.nondet, the branch or loop iteration is chosen arbitrarily.Key changes:
Stmt.itecondition andStmt.loopguard now acceptExprOrNondet Pite_nondet_true_sem/ite_nondet_false_semconstructorsDetToNondettransform handles nondet conditions (no assume needed)LoopElimtransform handles nondet guards (no guard negation needed).detExprOrNondetin condition positionsTesting
All existing tests pass (except a pre-existing failure in
StrataTest/DDM/Integration/Java/TestGen.leandue to asorryinStatementWF.leanon main).Fixes #612