From 9b559d015120a694014e1055a3d4395bcd225719 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 12 Nov 2026 06:17:44 +0000 Subject: [PATCH] fix(codegen,smt): declare sysml_parse_rec in generated C; order a witnessed 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 --- .../codegen-rec-parse-declaration.fixed.md | 1 + .../unreleased/smt-sensitivity-value-order.fixed.md | 1 + docs/project/native-compilation.md | 2 +- internal/exec/smt/twocopy.go | 5 +++++ internal/frontend/repl/optimize_test.go | 12 +++++++++--- internal/translate/codegen/build.go | 2 +- internal/translate/codegen/emit_fn.go | 1 + 7 files changed, 19 insertions(+), 5 deletions(-) create mode 100644 changes/unreleased/codegen-rec-parse-declaration.fixed.md create mode 100644 changes/unreleased/smt-sensitivity-value-order.fixed.md diff --git a/changes/unreleased/codegen-rec-parse-declaration.fixed.md b/changes/unreleased/codegen-rec-parse-declaration.fixed.md new file mode 100644 index 0000000000..72edf108af --- /dev/null +++ b/changes/unreleased/codegen-rec-parse-declaration.fixed.md @@ -0,0 +1 @@ +- The generated C of a function whose program holds records declares `sysml_parse_rec`, so the collection runtime it instantiates over records compiles under a C compiler that rejects implicit declarations (gcc 14 and later); the compiler is now asked to reject them everywhere (`-Werror=implicit-function-declaration`). diff --git a/changes/unreleased/smt-sensitivity-value-order.fixed.md b/changes/unreleased/smt-sensitivity-value-order.fixed.md new file mode 100644 index 0000000000..28de97c607 --- /dev/null +++ b/changes/unreleased/smt-sensitivity-value-order.fixed.md @@ -0,0 +1 @@ +- A sensitivity the SMT engine witnesses spells the output's two values in the check engine's order (`x ends as 1 or 2`), with witness A the run that ends with the first, whichever copy the solver's model put first. diff --git a/docs/project/native-compilation.md b/docs/project/native-compilation.md index 076b92f13f..80571a5879 100644 --- a/docs/project/native-compilation.md +++ b/docs/project/native-compilation.md @@ -407,7 +407,7 @@ lower.CalcBody (statements) ──┘ checked-arithmetic prelude, the calcs as functions, a `sysml_run` entry that turns an error into a status, and a `main`. - `build.go` — `Source`, `Build`, `Targets`; C is compiled with - `-O3 -flto -std=gnu11 -Wall -Wextra`, Go in a throwaway module. + `-O3 -flto -std=gnu11 -Werror=implicit-function-declaration -Wall -Wextra`, Go in a throwaway module. ### Function values diff --git a/internal/exec/smt/twocopy.go b/internal/exec/smt/twocopy.go index d1ea0e72dd..22d956b115 100644 --- a/internal/exec/smt/twocopy.go +++ b/internal/exec/smt/twocopy.go @@ -198,6 +198,11 @@ func (e *Encoding) DecodePair(result *solve.Result, out Output) (*Diverging, err if d.Values[0] == d.Values[1] { return nil, &WitnessError{Var: out.Var.Name, Reason: fmt.Sprintf("both copies end with %s", d.Values[0])} } + // The check engine orders a divergence's values; which copy the solver put first is noise. + if d.Values[1] < d.Values[0] { + d.Runs[0], d.Runs[1] = d.Runs[1], d.Runs[0] + d.Values[0], d.Values[1] = d.Values[1], d.Values[0] + } return d, nil } diff --git a/internal/frontend/repl/optimize_test.go b/internal/frontend/repl/optimize_test.go index 5a07659106..4b4d09f2bb 100644 --- a/internal/frontend/repl/optimize_test.go +++ b/internal/frontend/repl/optimize_test.go @@ -222,7 +222,9 @@ func TestOptimizeReportsObjectivesInDeclarationOrder(t *testing.T) { } // A bound no assignment attains is never reported as a value: the report says -// there is no optimum and offers only the feasible value found. +// there is no optimum and offers only the feasible value found. Whether the +// solver names the bound it approaches (z3 4.13) or reports nothing (z3 4.8) +// depends on its version; what it must never do is report the bound as a value. func TestOptimizeReportsABoundThatIsNotAttained(t *testing.T) { requireOptimizingSolver(t) s := checkSession(t, optimizeModel) @@ -231,8 +233,12 @@ func TestOptimizeReportsABoundThatIsNotAttained(t *testing.T) { t.Fatalf("status is %s, want no-optimum: %s", report.Status, strings.Join(report.Lines, "\n")) } wants(t, got, "! Analysis OpenBound is satisfiable, but its optimum was not established", - "maximize widest = `margin`: no optimum reported") - rejects(t, got, "is optimized") + "maximize widest = `margin`: no ") + if !strings.Contains(got, "`margin`: no optimum reported") && + !strings.Contains(got, "`margin`: no greatest value, approaching 10.5 without attaining it") { + t.Errorf("the open bound is neither unreported nor reported as approached:\n%s", got) + } + rejects(t, got, "is optimized", "`margin`: 10.5") } // Refusals need no solver: they are settled while translating. diff --git a/internal/translate/codegen/build.go b/internal/translate/codegen/build.go index 603547ccaa..17e1d7c28d 100644 --- a/internal/translate/codegen/build.go +++ b/internal/translate/codegen/build.go @@ -52,7 +52,7 @@ func goCommand(name string) (string, error) { // CFlags are the C compiler options; the prelude's explicit checks keep -O3 safe, // and no contraction keeps every Real operation rounded as the interpreter rounds it. -var CFlags = []string{"-O3", "-flto", "-ffp-contract=off", "-std=gnu11", "-Wall", "-Wextra", "-Wno-unused-function", "-Wno-unused-parameter"} +var CFlags = []string{"-O3", "-flto", "-ffp-contract=off", "-std=gnu11", "-Werror=implicit-function-declaration", "-Wall", "-Wextra", "-Wno-unused-function", "-Wno-unused-parameter"} // Source renders program for target, as a complete program with a main. func Source(p *Program, target Target) ([]byte, error) { diff --git a/internal/translate/codegen/emit_fn.go b/internal/translate/codegen/emit_fn.go index 33488d072f..1674294020 100644 --- a/internal/translate/codegen/emit_fn.go +++ b/internal/translate/codegen/emit_fn.go @@ -304,6 +304,7 @@ static const char *sysml_show_rec(sysml_rec *r) { sysml_format_rec(r, text, sizeof text); return text; } +static sysml_rec *sysml_parse_rec(const char *s, const char *name) { fprintf(stderr, "argument %s: %s is not an object value\n", name, s); exit(2); } ` + r.Replace(cSeqTemplate) }