feat: Translate PySpec preconditions to Laurel assertions for bug finding#615
feat: Translate PySpec preconditions to Laurel assertions for bug finding#615MikaelMayer wants to merge 29 commits intomainfrom
Conversation
…ding Translate SpecExpr preconditions into Assert statements in generated Laurel procedures. Wire up type alias resolution so Python type annotations resolve to pyspec composite types, and emit StaticCall for known pyspec methods. Add procedure inlining to pyAnalyzeLaurel so assertions are checked at call sites with concrete arguments.
Two test cases: - test_precondition_pass: valid args satisfy all preconditions (3 always true) - test_precondition_fail: empty body violates len >= 1 (1 always false detected)
Check Core program structure via string inspection instead of running the solver, avoiding sorry dependencies from ProcedureInlining.
The hasModel check was too broad — it matched composite type names, causing method calls like Resource.get_value to be emitted as StaticCall instead of InstanceCall. Now only checks preludeProcedures.
Inlining all procedures changes verification output for existing tests. Inlining should be opt-in or conditional on pyspec usage.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
The precondition translation is well-structured: specExprToLaurel cleanly maps each SpecExpr constructor to Laurel, buildSpecBody assembles the procedure body, and the type alias plumbing through the pipeline is consistent across all three files. The augmented assignment support is a nice bonus. Two comments, one of which is a bug.
The PR description mentions StrataMain.lean changes (procedure inlining in pyAnalyzeLaurel) but those are no longer in the diff — presumably already merged to main. The description also doesn't mention the augmented assignment feature (AugAssign support, test_augmented_assign, sarif skip). Worth updating the description to match the actual diff.
| @@ -301,7 +413,18 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl) | |||
| | .TVoid => [] | |||
| | _ => [{ name := "result", type := retType }] | |||
| if func.preconditions.size > 0 || func.postconditions.size > 0 then | |||
There was a problem hiding this comment.
This condition fires even when only preconditions are present (no postconditions), emitting a misleading "Postconditions not yet supported" warning for functions that only have preconditions — which are now supported. Should be:
| if func.preconditions.size > 0 || func.postconditions.size > 0 then | |
| if func.postconditions.size > 0 then |
There was a problem hiding this comment.
Fixed — now only warns when postconditions are present.
|
|
||
| /-- Build a procedure body that asserts preconditions and havocs outputs. -/ | ||
| def buildSpecBody (preconditions : Array Assertion) (outputs : List Parameter) | ||
| : ToLaurelM (Body × Nat) := do |
There was a problem hiding this comment.
Nit: translatedCount is returned but always discarded by the caller (let (body, _) ← buildSpecBody ...). Consider either dropping it from the return type or using it for a diagnostic (e.g., logging how many preconditions were successfully translated vs. emitted as assert true).
There was a problem hiding this comment.
Dropped — buildSpecBody now returns just Body.
- Only warn about postconditions when they are actually present - Drop unused translatedCount from buildSpecBody return type - Resolve merge conflict with main (Hole fallback for InstanceCall)
|
Both review comments addressed in commit 00c9e11:
|
Only inject procedure aliases, not composite type names. The composite type resolution for pyspec classes happens via resolveTypeName in refineFunctionCallExpr instead.
Restrict StaticCall emission to methods where the caller type has a pyspec type alias, preventing dispatch-resolved types from being incorrectly converted from Hole to StaticCall.
1 participant
Translate PySpec preconditions into Laurel assertions for bug-finding verification.
When a PySpec function has
assertpreconditions (e.g.assert len(kwargs["name"]) >= 1),the generated Laurel procedure now contains
Assertstatements instead of an opaque body.After inlining at call sites, the solver can prove whether preconditions are satisfied
or always violated — detecting real bugs statically.
Changes:
Specs/ToLaurel.lean: TranslateSpecExprto LaurelStmtExprusing Core preludefunctions (
Str.Length,Any..as_string!,Any..as_int!,from_int,DictStrAny_contains). Untranslatable preconditions emitassert truewith adiagnostic.
kwargs["field"]references resolve to expanded parameter names.PySpecPipeline.lean: Thread type aliases (unprefixed → prefixed class names) soPython type annotations resolve to pyspec composite types.
PythonToLaurel.lean: Resolve type aliases for composite type creation and methoddispatch. Emit
StaticCallinstead ofInstanceCallwhen the method resolves to aknown pyspec procedure.
StrataMain.lean: Add procedure inlining topyAnalyzeLaurelso pyspec assertionsare checked at call sites with concrete arguments.
Regex preconditions (
string_to_regex,regex_matches) and quantifier preconditions(
forallList,forallDict) are not yet translated (emitassert true).