Repository navigation
fix(codegen,smt): declare sysml_parse_rec in generated C; order a witnessed sensitivity's values - #2170
Closed
devin-ai-integration[bot] wants to merge 1 commit into
Closed
fix(codegen,smt): declare sysml_parse_rec in generated C; order a witnessed sensitivity's values#2170devin-ai-integration[bot] wants to merge 1 commit into
devin-ai-integration[bot] wants to merge 1 commit into
Conversation
…nessed sensitivity's values The collection runtime instantiated over records calls sysml_parse_rec, which nothing declared: gcc 14 rejects the implicit declaration where gcc 13 warned. Declare it as the record counterpart of sysml_parse_fn and ask every C compiler to reject implicit declarations, so the gate catches the next one on any image. The SMT engine spelt a divergence's two values in the order the solver's model put the copies, which differs between z3 4.8 and 4.13. Order them as the check engine does, swapping the two runs with the values so witness A stays the run that ends with the first. The open-bound optimum test accepted only the z3 4.8 rendering (nothing reported); it now accepts the approached bound 4.13 reports and rejects the bound as a value under either. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
Contributor
Author
![devin-ai-integration[bot]](https://avatars.githubusercontent.com/in/811515?s=60&v=4){kind=small}
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
When
ubuntu-latestmoved to ubuntu-26.04 (gcc 15, z3 4.13.3) the merge queue went red on three tests that pass on 24.04 (gcc 13, z3 4.8.12). #2165 pins the image back; this fixes the two latent bugs and the one solver-specific assertion the newer image exposed, so the suite is correct on either.internal/translate/codegen/emit_fn.go): the collection runtime instantiated over records (cRecSeqRuntime) callssysml_parse_rec, which nothing declared. gcc ≤ 13 warned and dropped the unused parser; gcc 14+ makes the implicit declaration an error, failingTestCompiledCalcsAgreeWithInterpreter/candTestCompiledStepBudgetMatchesInterpreteronRec::InSeq. It is now declared as the record counterpart ofsysml_parse_fn.CFlagsgains-Werror=implicit-function-declarationso every compiler rejects the next one.internal/exec/smt/twocopy.go):DecodePairspelt the output's two values in the order the solver's model put the two copies, sox ends as 1 or 2becamex ends as 2 or 1under z3 4.13 (TestEngineSMTDecidesSensitivity). The pair is now ordered as the check engine orders aDivergence(lexically), swapping the runs with the values so witness A is still the run ending with the first value.internal/frontend/repl/optimize_test.go): asserted the z3 4.8 rendering only (no optimum reported). z3 4.13 names the bound it approaches, whichoptimumLinesalready renders asno greatest value, approaching 10.5 without attaining it. The test now accepts either rendering and asserts the contract in the test's name: the bound is never reported as a value (`margin`: 10.5rejected).How it was verified
-Werror=implicit-function-declarationfirst, without the fix:go test ./tests/codegen -run 'TestCompiledCalcsAgreeWithInterpreter/c$'reproduces the CI error on local gcc 11 (implicit declaration of function ‘sysml_parse_rec’). With the fix the package passes.go test -count=1 ./internal/translate/codegen ./internal/exec/smt ./internal/frontend/repl ./tests/codegenandgo test ./cmd/sysml -run 'SMT|Sensitiv': pass (local z3 4.8.12, so the 4.8 branch of the optimum test; the 4.13 branch is the string CI printed).go build ./...,go vet,gofmt -l, staticcheck on the three packages: clean.Checklist
make testandmake lintpass locally (affected packages; staticcheck clean)docs/project/native-compilation.mdflag list)changes/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (none moved)F4,K5) in the body, docs, or changelogLink to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/a22ac6bb49a04224941818e07d42bed9
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/a22ac6bb49a04224941818e07d42bed9?variant=devin
Requested by: @HuiJun
🟢 Devin Review found nothing to fix · View findings · Follow Devin's work