From a0e8b3d9bebc88cb9156b6c13d5a4cd94af7dfec Mon Sep 17 00:00:00 2001 From: David Deng Date: Fri, 8 May 2026 11:45:49 -0700 Subject: [PATCH 01/21] Fix namespace collision and SMACK assert encoding in BoogieToStrata 1. Namespace collision (issue 1 in #1148): Constants that share a name with a procedure are now prefixed with __const_ in the Strata output. The rename is applied consistently in declarations and references. 2. Recursive synonym resolution (Fixes issue 2 in #1148): DealiasTypeExpr now recurses on its result, resolving synonym chains like ref := i64 := int fully to the base type. Previously it resolved only one level, causing panics on comparison/arithmetic operators applied to multi-level type synonyms. 3. SMACK assert encoding (issue 3 in #1148): Procedures named assert_.* now get a requires (arg != 0) precondition emitted. Call elimination generates VCs at each call site, making SMACK assertions verifiable. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../Core/DDMTransform/Translate.lean | 4 +- .../BoogieToStrata/Source/StrataGenerator.cs | 60 ++++++++++++++++++- .../Tests/NamespaceCollision.bpl | 25 ++++++++ 3 files changed, 84 insertions(+), 5 deletions(-) create mode 100644 Tools/BoogieToStrata/Tests/NamespaceCollision.bpl diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index aa088ca54f..6361a9fdeb 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -453,8 +453,8 @@ partial def dealiasTypeExpr (p : Program) (te : TypeExpr) : TypeExpr := match te with | (.fvar _ idx #[]) => match p.globalContext.kindOf! idx with - | .expr te => te - | .type [] (.some te) => te + | .expr te => dealiasTypeExpr p te + | .type [] (.some te) => dealiasTypeExpr p te | _ => te | _ => te diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 368e6e7b5f..4f7f5a6668 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -52,6 +52,12 @@ public class StrataGenerator : ReadOnlyVisitor { // Global variables collected from the program, used to convert them // into inout/input parameters on procedure headers and call sites. private List _globalVariables = []; + // Maps sanitized constant names to their renamed versions when they + // collide with procedure names. In Boogie, constants and procedures + // live in separate namespaces, but Strata Core has a single namespace. + private readonly Dictionary _constantRenames = new(); + // Set of all sanitized procedure names, used to detect collisions. + private readonly HashSet _procedureNames = new(); private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program) { _options = options; @@ -74,6 +80,22 @@ public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTex generator.FindSpecialTypes(); + // Collect all procedure names (sanitized) to detect namespace collisions. + foreach (var proc in p.Procedures) { + generator._procedureNames.Add(SanitizeNameForStrata(proc.Name)); + } + foreach (var impl in p.Implementations) { + generator._procedureNames.Add(SanitizeNameForStrata(impl.Name)); + } + + // Build rename map for constants that collide with procedure names. + foreach (var c in liveDeclarations.OfType()) { + var sanitized = SanitizeNameForStrata(c.TypedIdent.Name); + if (generator._procedureNames.Contains(sanitized)) { + generator._constantRenames[c.TypedIdent.Name] = $"__const_{sanitized}"; + } + } + var typeConstructors = p.TopLevelDeclarations.OfType().ToList(); if (typeConstructors.Count != 0) { generator.WriteLine("// Type constructors"); @@ -299,6 +321,17 @@ private string Name(string name) { return SanitizeNameForStrata(name); } + /// + /// Returns the (possibly renamed) name for a constant, handling namespace + /// collisions with procedures. + /// + private string ConstantName(string originalName) { + if (_constantRenames.TryGetValue(originalName, out var renamed)) { + return renamed; + } + return SanitizeNameForStrata(originalName); + } + private void WriteLine(string text) { _writer.WriteLine(text); } @@ -310,7 +343,11 @@ private void EmitOldExpr(Expr expr) { switch (expr) { case IdentifierExpr identExpr: WriteText("old "); - WriteText(Name(identExpr.Name)); + if (identExpr.Decl is Constant && _constantRenames.ContainsKey(identExpr.Name)) { + WriteText(ConstantName(identExpr.Name)); + } else { + WriteText(Name(identExpr.Name)); + } break; case NAryExpr { Fun: MapSelect } mapSelect: WriteText("("); @@ -546,7 +583,11 @@ public override Expr VisitExpr(Expr node) { case LiteralExpr literalExpr: throw new StrataConversionException(node.tok, $"Unsupported literal type: {literalExpr}"); case IdentifierExpr identifierExpr: - WriteText(Name(identifierExpr.Name)); + if (identifierExpr.Decl is Constant && _constantRenames.ContainsKey(identifierExpr.Name)) { + WriteText(ConstantName(identifierExpr.Name)); + } else { + WriteText(Name(identifierExpr.Name)); + } break; case NAryExpr nAryExpr: { var fun = nAryExpr.Fun; @@ -1510,7 +1551,7 @@ public override Block VisitBlock(Block node) { public override Constant VisitConstant(Constant node) { var ti = node.TypedIdent; - var name = Name(ti.Name); + var name = ConstantName(ti.Name); WriteText($"const {name} : "); VisitType(ti.Type); if (node.Unique) { @@ -1773,6 +1814,19 @@ private void WriteProcedureHeader(Procedure proc) { public override Procedure VisitProcedure(Procedure node) { if (!_program.Implementations.Any(i => i.Name.Equals(node.Name))) { WriteProcedureHeader(node); + // SMACK encodes C assert(expr) as a call to assert_.*(cond). + // Emit a requires precondition so the call-elimination pass + // generates a VC checking the condition is non-zero. + if (node.Name.StartsWith("assert_") && node.InParams.Count > 0 + && node.Requires.Count == 0) { + var firstParam = Name(node.InParams[0].TypedIdent.Name); + WriteLine("spec {"); + IncIndent(); + Indent(); + WriteLine($"requires ({firstParam} != 0);"); + DecIndent(); + WriteText("}"); + } WriteLine(";"); WriteLine(); } diff --git a/Tools/BoogieToStrata/Tests/NamespaceCollision.bpl b/Tools/BoogieToStrata/Tests/NamespaceCollision.bpl new file mode 100644 index 0000000000..caedc2c08a --- /dev/null +++ b/Tools/BoogieToStrata/Tests/NamespaceCollision.bpl @@ -0,0 +1,25 @@ +// Minimal reproduction: namespace collision bug in BoogieToStrata. +// Boogie allows a constant and procedure to share the same name +// because they live in separate namespaces. BoogieToStrata emits +// both into Strata Core's single namespace, causing: +// "a declaration of this name already exists" + +type ref = int; + +const main: ref; +axiom (main == 1000); + +var x: int; + +procedure main() + modifies x; +{ + var y: int; + x := 42; + assert x == 42; + // Use the constant in an expression that doesn't require the axiom to verify + y := 0; + if (main == 1000) { y := 1; } + // This assertion is trivially true regardless of the axiom + assert y == 0 || y == 1; +} From ceb164cf7931c8d643f3e016fda700942c7088fd Mon Sep 17 00:00:00 2001 From: David Deng Date: Fri, 8 May 2026 14:02:52 -0700 Subject: [PATCH 02/21] Refactor name collision fix: use global name set with entity-type prefix Replace the separate _constantRenames/_procedureNames approach with a unified _renames dictionary populated by scanning all declarations upfront. Procedures are claimed first; constants, functions, and globals that collide get prefixed with their kind (__const_, __func_, __var_). Also restores InferModifies and Prune options in BoogieToStrata.cs. Co-Authored-By: Claude Opus 4.6 (1M context) --- Tools/BoogieToStrata/Source/BoogieToStrata.cs | 4 +- .../BoogieToStrata/Source/StrataGenerator.cs | 61 ++++++++++--------- Tools/BoogieToStrata/Tests/SmackAssert.bpl | 21 +++++++ 3 files changed, 56 insertions(+), 30 deletions(-) create mode 100644 Tools/BoogieToStrata/Tests/SmackAssert.bpl diff --git a/Tools/BoogieToStrata/Source/BoogieToStrata.cs b/Tools/BoogieToStrata/Source/BoogieToStrata.cs index 1816f6a1fc..f0dc7d2cb1 100644 --- a/Tools/BoogieToStrata/Source/BoogieToStrata.cs +++ b/Tools/BoogieToStrata/Source/BoogieToStrata.cs @@ -18,7 +18,9 @@ public static int Main(string[] args) { var options = new CommandLineOptions(Console.Out, new ConsolePrinter()) { Verify = false, - TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates + TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates, + InferModifies = true, + Prune = true }; var boogieEngine = ExecutionEngine.CreateWithoutSharedCache(options); diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 4f7f5a6668..7a76ad475a 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -52,12 +52,11 @@ public class StrataGenerator : ReadOnlyVisitor { // Global variables collected from the program, used to convert them // into inout/input parameters on procedure headers and call sites. private List _globalVariables = []; - // Maps sanitized constant names to their renamed versions when they - // collide with procedure names. In Boogie, constants and procedures - // live in separate namespaces, but Strata Core has a single namespace. - private readonly Dictionary _constantRenames = new(); - // Set of all sanitized procedure names, used to detect collisions. - private readonly HashSet _procedureNames = new(); + // Renames for declarations whose sanitized name collides with another + // declaration. Boogie has separate namespaces for constants, procedures, + // etc., but Strata Core has a single namespace. First-seen wins; later + // entities get prefixed with their kind (__const_, __func_, __var_). + private readonly Dictionary _renames = new(); private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program) { _options = options; @@ -80,20 +79,28 @@ public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTex generator.FindSpecialTypes(); - // Collect all procedure names (sanitized) to detect namespace collisions. - foreach (var proc in p.Procedures) { - generator._procedureNames.Add(SanitizeNameForStrata(proc.Name)); - } - foreach (var impl in p.Implementations) { - generator._procedureNames.Add(SanitizeNameForStrata(impl.Name)); - } - - // Build rename map for constants that collide with procedure names. + // Build rename map for declarations with colliding sanitized names. + // Procedures/implementations are claimed first; constants, functions, + // and globals that collide get prefixed with their entity kind. + var claimed = new HashSet(); + foreach (var proc in p.Procedures) + claimed.Add(SanitizeNameForStrata(proc.Name)); + foreach (var impl in p.Implementations) + claimed.Add(SanitizeNameForStrata(impl.Name)); foreach (var c in liveDeclarations.OfType()) { var sanitized = SanitizeNameForStrata(c.TypedIdent.Name); - if (generator._procedureNames.Contains(sanitized)) { - generator._constantRenames[c.TypedIdent.Name] = $"__const_{sanitized}"; - } + if (!claimed.Add(sanitized)) + generator._renames[c.TypedIdent.Name] = $"__const_{sanitized}"; + } + foreach (var f in liveDeclarations.OfType()) { + var sanitized = SanitizeNameForStrata(f.Name); + if (!claimed.Add(sanitized)) + generator._renames[f.Name] = $"__func_{sanitized}"; + } + foreach (var g in p.GlobalVariables) { + var sanitized = SanitizeNameForStrata(g.Name); + if (!claimed.Add(sanitized)) + generator._renames[g.Name] = $"__var_{sanitized}"; } var typeConstructors = p.TopLevelDeclarations.OfType().ToList(); @@ -322,13 +329,9 @@ private string Name(string name) { } /// - /// Returns the (possibly renamed) name for a constant, handling namespace - /// collisions with procedures. - /// - private string ConstantName(string originalName) { - if (_constantRenames.TryGetValue(originalName, out var renamed)) { + private string ResolveName(string originalName) { + if (_renames.TryGetValue(originalName, out var renamed)) return renamed; - } return SanitizeNameForStrata(originalName); } @@ -343,8 +346,8 @@ private void EmitOldExpr(Expr expr) { switch (expr) { case IdentifierExpr identExpr: WriteText("old "); - if (identExpr.Decl is Constant && _constantRenames.ContainsKey(identExpr.Name)) { - WriteText(ConstantName(identExpr.Name)); + if (_renames.ContainsKey(identExpr.Name)) { + WriteText(ResolveName(identExpr.Name)); } else { WriteText(Name(identExpr.Name)); } @@ -583,8 +586,8 @@ public override Expr VisitExpr(Expr node) { case LiteralExpr literalExpr: throw new StrataConversionException(node.tok, $"Unsupported literal type: {literalExpr}"); case IdentifierExpr identifierExpr: - if (identifierExpr.Decl is Constant && _constantRenames.ContainsKey(identifierExpr.Name)) { - WriteText(ConstantName(identifierExpr.Name)); + if (_renames.ContainsKey(identifierExpr.Name)) { + WriteText(ResolveName(identifierExpr.Name)); } else { WriteText(Name(identifierExpr.Name)); } @@ -1551,7 +1554,7 @@ public override Block VisitBlock(Block node) { public override Constant VisitConstant(Constant node) { var ti = node.TypedIdent; - var name = ConstantName(ti.Name); + var name = ResolveName(ti.Name); WriteText($"const {name} : "); VisitType(ti.Type); if (node.Unique) { diff --git a/Tools/BoogieToStrata/Tests/SmackAssert.bpl b/Tools/BoogieToStrata/Tests/SmackAssert.bpl new file mode 100644 index 0000000000..01ae42e412 --- /dev/null +++ b/Tools/BoogieToStrata/Tests/SmackAssert.bpl @@ -0,0 +1,21 @@ +// Minimal test case for SMACK assert_ pattern recognition. +// SMACK encodes C assert(expr) as a call to assert_.i32(cond). +// BoogieToStrata should recognize this pattern and emit: +// assert (cond != 0); +// instead of an opaque procedure call. +// +// This test passes 0 (false) to assert — it should be a verification +// failure, but currently produces "All 0 goals passed" because the +// call is treated as opaque. + +type i32 = int; + +procedure assert_.i32(p.0: i32) returns ($r: i32); + +procedure main() returns ($r: i32) +{ + // assert(false) — should fail verification + call $r := assert_.i32(0); + $r := 0; + return; +} From fa62cea4536f06e87f5e3ea32f8ad7fb2032f7c5 Mon Sep 17 00:00:00 2001 From: David Deng Date: Fri, 8 May 2026 16:01:28 -0700 Subject: [PATCH 03/21] Remove Prune option to fix CI integration test failures Prune=true caused Boogie to remove declarations needed by axioms and quantifiers, shifting line numbers and breaking verification for tests like BooleanQuantification, Axioms, TypeSynonyms2, Quantifiers, and Lambda. InferModifies is retained as it's needed for SMACK support. Co-Authored-By: Claude Opus 4.6 (1M context) --- Tools/BoogieToStrata/Source/BoogieToStrata.cs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Tools/BoogieToStrata/Source/BoogieToStrata.cs b/Tools/BoogieToStrata/Source/BoogieToStrata.cs index f0dc7d2cb1..3ee6cc63c2 100644 --- a/Tools/BoogieToStrata/Source/BoogieToStrata.cs +++ b/Tools/BoogieToStrata/Source/BoogieToStrata.cs @@ -19,8 +19,7 @@ public static int Main(string[] args) { var options = new CommandLineOptions(Console.Out, new ConsolePrinter()) { Verify = false, TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates, - InferModifies = true, - Prune = true + InferModifies = true }; var boogieEngine = ExecutionEngine.CreateWithoutSharedCache(options); From 96913e028b3b9e9682472bab808a9c91b5800527 Mon Sep 17 00:00:00 2001 From: David Deng Date: Fri, 8 May 2026 16:40:30 -0700 Subject: [PATCH 04/21] Fix #1152 --- .../BoogieToStrata/Source/StrataGenerator.cs | 82 +++++++++---------- .../Tests/SanitizationCollision.bpl | 25 ++++++ 2 files changed, 66 insertions(+), 41 deletions(-) create mode 100644 Tools/BoogieToStrata/Tests/SanitizationCollision.bpl diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 7a76ad475a..cd085c2da7 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -53,10 +53,10 @@ public class StrataGenerator : ReadOnlyVisitor { // into inout/input parameters on procedure headers and call sites. private List _globalVariables = []; // Renames for declarations whose sanitized name collides with another - // declaration. Boogie has separate namespaces for constants, procedures, - // etc., but Strata Core has a single namespace. First-seen wins; later - // entities get prefixed with their kind (__const_, __func_, __var_). - private readonly Dictionary _renames = new(); + // declaration. Keyed by Boogie Declaration object to avoid ambiguity + // when two entities share the same original name (e.g., const main and + // procedure main). First-seen wins; later entities get prefixed. + private readonly Dictionary _renames = new(); private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program) { _options = options; @@ -80,28 +80,37 @@ public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTex generator.FindSpecialTypes(); // Build rename map for declarations with colliding sanitized names. - // Procedures/implementations are claimed first; constants, functions, - // and globals that collide get prefixed with their entity kind. + // Two kinds of collision are handled: + // 1. Cross-namespace: constant vs procedure sharing the same name + // 2. Sanitization: distinct names that map to the same string + // (e.g., $add.i32 and $add_i32 both become _add_i32) + // First-seen wins; colliding entities get a suffix (_2, _3, ...). var claimed = new HashSet(); - foreach (var proc in p.Procedures) - claimed.Add(SanitizeNameForStrata(proc.Name)); - foreach (var impl in p.Implementations) - claimed.Add(SanitizeNameForStrata(impl.Name)); - foreach (var c in liveDeclarations.OfType()) { - var sanitized = SanitizeNameForStrata(c.TypedIdent.Name); - if (!claimed.Add(sanitized)) - generator._renames[c.TypedIdent.Name] = $"__const_{sanitized}"; - } - foreach (var f in liveDeclarations.OfType()) { - var sanitized = SanitizeNameForStrata(f.Name); - if (!claimed.Add(sanitized)) - generator._renames[f.Name] = $"__func_{sanitized}"; + + void ClaimOrRename(Declaration decl, string originalName, string prefix) { + var sanitized = SanitizeNameForStrata(originalName); + if (claimed.Add(sanitized)) return; + var candidate = $"{prefix}{sanitized}"; + if (!claimed.Add(candidate)) { + var i = 2; + while (!claimed.Add($"{candidate}_{i}")) i++; + candidate = $"{candidate}_{i}"; + } + generator._renames[decl] = candidate; } - foreach (var g in p.GlobalVariables) { - var sanitized = SanitizeNameForStrata(g.Name); - if (!claimed.Add(sanitized)) - generator._renames[g.Name] = $"__var_{sanitized}"; + + foreach (var proc in p.Procedures) + ClaimOrRename(proc, proc.Name, "__proc_"); + foreach (var impl in p.Implementations) { + var sanitized = SanitizeNameForStrata(impl.Name); + claimed.Add(sanitized); } + foreach (var c in liveDeclarations.OfType()) + ClaimOrRename(c, c.TypedIdent.Name, "__const_"); + foreach (var f in liveDeclarations.OfType()) + ClaimOrRename(f, f.Name, "__func_"); + foreach (var g in p.GlobalVariables) + ClaimOrRename(g, g.Name, "__var_"); var typeConstructors = p.TopLevelDeclarations.OfType().ToList(); if (typeConstructors.Count != 0) { @@ -328,9 +337,8 @@ private string Name(string name) { return SanitizeNameForStrata(name); } - /// - private string ResolveName(string originalName) { - if (_renames.TryGetValue(originalName, out var renamed)) + private string NameOf(Declaration decl, string originalName) { + if (_renames.TryGetValue(decl, out var renamed)) return renamed; return SanitizeNameForStrata(originalName); } @@ -346,11 +354,7 @@ private void EmitOldExpr(Expr expr) { switch (expr) { case IdentifierExpr identExpr: WriteText("old "); - if (_renames.ContainsKey(identExpr.Name)) { - WriteText(ResolveName(identExpr.Name)); - } else { - WriteText(Name(identExpr.Name)); - } + WriteText(identExpr.Decl != null ? NameOf(identExpr.Decl, identExpr.Name) : Name(identExpr.Name)); break; case NAryExpr { Fun: MapSelect } mapSelect: WriteText("("); @@ -586,11 +590,7 @@ public override Expr VisitExpr(Expr node) { case LiteralExpr literalExpr: throw new StrataConversionException(node.tok, $"Unsupported literal type: {literalExpr}"); case IdentifierExpr identifierExpr: - if (_renames.ContainsKey(identifierExpr.Name)) { - WriteText(ResolveName(identifierExpr.Name)); - } else { - WriteText(Name(identifierExpr.Name)); - } + WriteText(identifierExpr.Decl != null ? NameOf(identifierExpr.Decl, identifierExpr.Name) : Name(identifierExpr.Name)); break; case NAryExpr nAryExpr: { var fun = nAryExpr.Fun; @@ -678,7 +678,7 @@ public override Expr VisitExpr(Expr node) { break; case FunctionCall functionCall: { - WriteText($"{Name(functionCall.FunctionName)}("); + WriteText($"{NameOf(functionCall.Func, functionCall.FunctionName)}("); EmitSeparated(args, e => VisitExpr(e), ", "); WriteText(")"); break; @@ -997,7 +997,7 @@ public override Cmd VisitCallCmd(CallCmd node) { var modifiesNames = new HashSet(callee.Modifies.Select(m => m.Name)); Indent("call "); - WriteText($"{Name(callee.Name)}("); + WriteText($"{NameOf(callee, callee.Name)}("); // Emit: inout globals, then read-only globals, then original args, then out outputs. var needComma = false; foreach (var g in _globalVariables.Where(g => modifiesNames.Contains(g.Name))) { @@ -1554,7 +1554,7 @@ public override Block VisitBlock(Block node) { public override Constant VisitConstant(Constant node) { var ti = node.TypedIdent; - var name = ResolveName(ti.Name); + var name = NameOf(node, ti.Name); WriteText($"const {name} : "); VisitType(ti.Type); if (node.Unique) { @@ -1725,7 +1725,7 @@ private void MaybeEmitBuiltinBody(Function function) { } public override Function VisitFunction(Function node) { - WriteText($"function {Name(node.Name)}"); + WriteText($"function {NameOf(node, node.Name)}"); EmitTypeParameters(node.TypeParameters); WriteText("("); WriteFormals(node.InParams); @@ -1767,7 +1767,7 @@ private void WriteProcedureHeader(Procedure proc) { var modifiesGlobals = _globalVariables.Where(g => modifiesNames.Contains(g.Name)).ToList(); var readOnlyGlobals = _globalVariables.Where(g => !modifiesNames.Contains(g.Name)).ToList(); - WriteText($"procedure {Name(proc.Name)}"); + WriteText($"procedure {NameOf(proc, proc.Name)}"); EmitTypeParameters(proc.TypeParameters); WriteText("("); // Emit: inout globals, then read-only globals, then original inputs, then out outputs. diff --git a/Tools/BoogieToStrata/Tests/SanitizationCollision.bpl b/Tools/BoogieToStrata/Tests/SanitizationCollision.bpl new file mode 100644 index 0000000000..7a4f339a01 --- /dev/null +++ b/Tools/BoogieToStrata/Tests/SanitizationCollision.bpl @@ -0,0 +1,25 @@ +// Test case: sanitization collision in BoogieToStrata. +// +// SanitizeNameForStrata replaces '.', '$', '@', '#', '^' with '_'. +// This means distinct Boogie identifiers can map to the same Strata name: +// $add.i32 → _add_i32 +// $add_i32 → _add_i32 (collision!) +// +// The rename mechanism should detect this and disambiguate. + +type i32 = int; + +function {:inline} $add.i32(i1: i32, i2: i32) returns (i32) { i1 + i2 } +function {:inline} $add_i32(i1: i32, i2: i32) returns (i32) { i1 + i2 } + +procedure main() returns (r: i32) +ensures r == 5; +{ + var a: i32; + var b: i32; + a := $add.i32(2, 3); + b := $add_i32(2, 3); + assert a == 5; + assert b == 5; + r := a; +} From 46fde0d72490f1ee7ce4684e314fec6f363c1867 Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 11 May 2026 09:54:07 -0700 Subject: [PATCH 05/21] Fix rename consistency, tighten SMACK pattern, and add regression tests 1. Rename mechanism: use NameOf(decl, ...) instead of Name(...) at all sites that emit variable names (EmitSimpleAssign, VisitCallCmd, VisitHavocCmd, VisitGlobalVariable, WriteFormals) so that renamed globals are referenced consistently throughout the output. 2. SMACK assert pattern: tighten StartsWith("assert_") to StartsWith("assert_.") to match only SMACK's actual encoding (assert_.i32, assert_.i64) and avoid false positives on user procedures like assert_helper. 3. Regression tests: add .expect files for SmackAssert, NamespaceCollision, SanitizationCollision (fixing the test harness gap where --check mode skipped verification), plus new test cases for TypeSynonymChain, GlobalVarRenameCollision, and AssertPrefixFalsePositive. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../BoogieToStrata/Source/StrataGenerator.cs | 14 ++++++------- .../Tests/AssertPrefixFalsePositive.bpl | 11 ++++++++++ .../Tests/AssertPrefixFalsePositive.expect | 2 ++ .../Tests/GlobalVarRenameCollision.bpl | 9 +++++++++ .../Tests/GlobalVarRenameCollision.expect | 2 ++ .../Tests/NamespaceCollision.expect | 4 ++++ .../Tests/SanitizationCollision.expect | 5 +++++ Tools/BoogieToStrata/Tests/SmackAssert.expect | 3 +++ .../BoogieToStrata/Tests/TypeSynonymChain.bpl | 20 +++++++++++++++++++ .../Tests/TypeSynonymChain.expect | 5 +++++ 10 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl create mode 100644 Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect create mode 100644 Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl create mode 100644 Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect create mode 100644 Tools/BoogieToStrata/Tests/NamespaceCollision.expect create mode 100644 Tools/BoogieToStrata/Tests/SanitizationCollision.expect create mode 100644 Tools/BoogieToStrata/Tests/SmackAssert.expect create mode 100644 Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl create mode 100644 Tools/BoogieToStrata/Tests/TypeSynonymChain.expect diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index cd085c2da7..1e395afd09 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -962,7 +962,7 @@ public override GotoCmd VisitGotoCmd(GotoCmd node) { private void EmitSimpleAssign(SimpleAssignLhs lhs, Expr rhs) { Indent(); - WriteText($"{Name(lhs.AssignedVariable.Name)} := "); + WriteText($"{NameOf(lhs.AssignedVariable.Decl, lhs.AssignedVariable.Name)} := "); VisitExpr(rhs); WriteLine(";"); } @@ -1002,12 +1002,12 @@ public override Cmd VisitCallCmd(CallCmd node) { var needComma = false; foreach (var g in _globalVariables.Where(g => modifiesNames.Contains(g.Name))) { if (needComma) WriteText(", "); - WriteText($"inout {Name(g.Name)}"); + WriteText($"inout {NameOf(g, g.Name)}"); needComma = true; } foreach (var g in _globalVariables.Where(g => !modifiesNames.Contains(g.Name))) { if (needComma) WriteText(", "); - WriteText(Name(g.Name)); + WriteText(NameOf(g, g.Name)); needComma = true; } foreach (var arg in node.Ins) { @@ -1027,7 +1027,7 @@ public override Cmd VisitCallCmd(CallCmd node) { public override Cmd VisitHavocCmd(HavocCmd node) { foreach (var x in node.Vars) { - IndentLine($"havoc {Name(x.Name)};"); + IndentLine($"havoc {NameOf(x.Decl, x.Name)};"); } // All assumptions come after all havocs! This allows where clauses @@ -1567,7 +1567,7 @@ public override Constant VisitConstant(Constant node) { public override GlobalVariable VisitGlobalVariable(GlobalVariable node) { var ti = node.TypedIdent; - WriteText($"var {Name(ti.Name)} : "); + WriteText($"var {NameOf(node, ti.Name)} : "); VisitType(ti.Type); WriteLine(";"); return node; @@ -1820,7 +1820,7 @@ public override Procedure VisitProcedure(Procedure node) { // SMACK encodes C assert(expr) as a call to assert_.*(cond). // Emit a requires precondition so the call-elimination pass // generates a VC checking the condition is non-zero. - if (node.Name.StartsWith("assert_") && node.InParams.Count > 0 + if (node.Name.StartsWith("assert_.") && node.InParams.Count > 0 && node.Requires.Count == 0) { var firstParam = Name(node.InParams[0].TypedIdent.Name); WriteLine("spec {"); @@ -1844,7 +1844,7 @@ private void WriteFormals(IEnumerable variables, ref bool needComma, if (needComma) WriteText(", "); var name = v.TypedIdent.Name ?? ""; if (name == "") name = $"x{n++}"; - WriteText($"{prefix}{Name(name)} : "); + WriteText($"{prefix}{NameOf(v, name)} : "); VisitType(v.TypedIdent.Type); needComma = true; } diff --git a/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl new file mode 100644 index 0000000000..36ab20b483 --- /dev/null +++ b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl @@ -0,0 +1,11 @@ +// Regression test: procedures starting with "assert_" but NOT matching +// SMACK's assert_.TYPE pattern should NOT get a synthetic requires. +// Only assert_. (literal dot) is the SMACK pattern. + +procedure assert_helper(p: int) returns (r: int); + +procedure main() returns (r: int) +{ + // assert_helper is a normal procedure, passing 0 should be fine + call r := assert_helper(0); +} diff --git a/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect new file mode 100644 index 0000000000..e9e8e85d9e --- /dev/null +++ b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect @@ -0,0 +1,2 @@ +Successfully parsed. +All 0 goals passed. diff --git a/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl new file mode 100644 index 0000000000..5a1275cbff --- /dev/null +++ b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl @@ -0,0 +1,9 @@ +const $a.b: int; axiom $a.b > 0; +var $a_b: int; // both sanitize to _a_b +procedure main() returns (r: int) + modifies $a_b; +{ + $a_b := 1; + havoc $a_b; + r := $a.b + $a_b; +} diff --git a/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect new file mode 100644 index 0000000000..e9e8e85d9e --- /dev/null +++ b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect @@ -0,0 +1,2 @@ +Successfully parsed. +All 0 goals passed. diff --git a/Tools/BoogieToStrata/Tests/NamespaceCollision.expect b/Tools/BoogieToStrata/Tests/NamespaceCollision.expect new file mode 100644 index 0000000000..c2c458ba8c --- /dev/null +++ b/Tools/BoogieToStrata/Tests/NamespaceCollision.expect @@ -0,0 +1,4 @@ +Successfully parsed. +NamespaceCollision.core.st(23, 4) [assert_0]: ✅ pass +NamespaceCollision.core.st(33, 4) [assert_1]: ✅ pass +All 2 goals passed. diff --git a/Tools/BoogieToStrata/Tests/SanitizationCollision.expect b/Tools/BoogieToStrata/Tests/SanitizationCollision.expect new file mode 100644 index 0000000000..d7e99638ef --- /dev/null +++ b/Tools/BoogieToStrata/Tests/SanitizationCollision.expect @@ -0,0 +1,5 @@ +Successfully parsed. +SanitizationCollision.core.st(29, 4) [assert_0]: ✅ pass +SanitizationCollision.core.st(30, 4) [assert_1]: ✅ pass +SanitizationCollision.core.st(21, 2) [main_ensures_0]: ✅ pass +All 3 goals passed. diff --git a/Tools/BoogieToStrata/Tests/SmackAssert.expect b/Tools/BoogieToStrata/Tests/SmackAssert.expect new file mode 100644 index 0000000000..8af84c0bbc --- /dev/null +++ b/Tools/BoogieToStrata/Tests/SmackAssert.expect @@ -0,0 +1,3 @@ +Successfully parsed. +SmackAssert.core.st(21, 6) [callElimAssert_assert__i32_requires_0_2]: ❌ fail +Finished with 0 goals passed, 1 failed. diff --git a/Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl b/Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl new file mode 100644 index 0000000000..cc5811b580 --- /dev/null +++ b/Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl @@ -0,0 +1,20 @@ +// Regression test for multi-level type synonym resolution. +// dealiasTypeExpr must recurse through: ref → i64 → int +// Without recursive resolution, comparison and arithmetic on `ref` +// trigger a panic because the type stays as a synonym instead of +// resolving to the base `int` type. + +type i64 = int; +type ref = i64; + +procedure main() returns (r: ref) +ensures r >= 0; +{ + var a: ref; + var b: ref; + a := 3; + b := a + 4; + assert b == 7; + assert a <= b; + r := b; +} diff --git a/Tools/BoogieToStrata/Tests/TypeSynonymChain.expect b/Tools/BoogieToStrata/Tests/TypeSynonymChain.expect new file mode 100644 index 0000000000..197fd783cb --- /dev/null +++ b/Tools/BoogieToStrata/Tests/TypeSynonymChain.expect @@ -0,0 +1,5 @@ +Successfully parsed. +TypeSynonymChain.core.st(22, 4) [assert_0]: ✅ pass +TypeSynonymChain.core.st(23, 4) [assert_1]: ✅ pass +TypeSynonymChain.core.st(14, 2) [main_ensures_0]: ✅ pass +All 3 goals passed. From 0880ae33d7dc202d3806e020ca87dfb386df83cf Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 11 May 2026 10:24:45 -0700 Subject: [PATCH 06/21] fix: eliminate duplicate spec block for SMACK assert_ procedures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Problem: When an assert_. procedure had existing ensures (or requires) clauses, the generated Strata output contained two separate spec {} blocks — one from WriteProcedureHeader (for existing specs) and a second from VisitProcedure (for the synthetic requires). This produced invalid output like: `spec { ensures ...; }spec { requires ...; }`. Root Cause: VisitProcedure emitted the synthetic `requires (param != 0)` as a standalone spec block after calling WriteProcedureHeader, instead of injecting it into the procedure's Requires list so WriteProcedureHeader could emit everything in a single unified spec block. Fix: Build a synthetic Requires AST node (param != 0) and add it to node.Requires before calling WriteProcedureHeader, then remove it afterward to avoid permanently mutating the shared Boogie AST. This lets WriteProcedureHeader's existing spec-emission loop handle both the synthetic requires and any pre-existing specs in one block. Test: Added SmackAssertDuplicateSpec.bpl (assert_ procedure with an existing ensures clause) and SmackAssertWithEnsuresProducesSingleSpecBlock test that counts spec block occurrences and asserts exactly one is emitted. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../BoogieToStrataIntegrationTests.cs | 32 +++++++++++++++++++ .../BoogieToStrata/Source/StrataGenerator.cs | 28 ++++++++++------ .../Tests/SmackAssertDuplicateSpec.bpl | 16 ++++++++++ 3 files changed, 66 insertions(+), 10 deletions(-) create mode 100644 Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs index 05e16b9b9f..8679454511 100644 --- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs +++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs @@ -149,6 +149,38 @@ public void VerifyTestFile(string fileName, string filePath) { Assert.Equal(expectedExitCode, proc.ExitCode); } + /// + /// Regression test: an assert_. procedure with an existing ensures clause + /// should emit a single spec block containing both the synthetic requires and the + /// original ensures — not two separate spec blocks. + /// + [Fact] + public void SmackAssertWithEnsuresProducesSingleSpecBlock() { + var filePath = Path.Combine(TestsDirectory, "SmackAssertDuplicateSpec.bpl"); + Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}"); + + var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath); + Assert.Equal(0, exitCode); + + // Count occurrences of "spec {" in the output. + // There should be exactly one spec block for the assert_ procedure. + var specCount = 0; + var searchFrom = 0; + while (true) { + var idx = standardOutput.IndexOf("spec {", searchFrom, StringComparison.Ordinal); + if (idx < 0) break; + specCount++; + searchFrom = idx + 1; + } + + output.WriteLine($"Output:\n{standardOutput}"); + Assert.Equal(1, specCount); + + // The single spec block should contain both requires and ensures + Assert.Contains("requires", standardOutput); + Assert.Contains("ensures", standardOutput); + } + [Fact] public void ErrorCodeWithNoArguments() { var result = BoogieToStrata.Main(Array.Empty()); diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 1e395afd09..3d7bca5e6f 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -1816,22 +1816,30 @@ private void WriteProcedureHeader(Procedure proc) { public override Procedure VisitProcedure(Procedure node) { if (!_program.Implementations.Any(i => i.Name.Equals(node.Name))) { - WriteProcedureHeader(node); // SMACK encodes C assert(expr) as a call to assert_.*(cond). - // Emit a requires precondition so the call-elimination pass - // generates a VC checking the condition is non-zero. + // Inject a synthetic requires precondition so the call-elimination + // pass generates a VC checking the condition is non-zero. + // We add it to node.Requires so WriteProcedureHeader emits it + // inside a single spec block alongside any existing specs. + Requires? syntheticReq = null; if (node.Name.StartsWith("assert_.") && node.InParams.Count > 0 && node.Requires.Count == 0) { - var firstParam = Name(node.InParams[0].TypedIdent.Name); - WriteLine("spec {"); - IncIndent(); - Indent(); - WriteLine($"requires ({firstParam} != 0);"); - DecIndent(); - WriteText("}"); + var param = node.InParams[0]; + var paramExpr = new IdentifierExpr(param.tok, param); + var zero = new LiteralExpr(param.tok, Microsoft.BaseTypes.BigNum.FromInt(0)); + var neqExpr = Expr.Neq(paramExpr, zero); + syntheticReq = new Requires(false, neqExpr); + node.Requires.Add(syntheticReq); } + + WriteProcedureHeader(node); WriteLine(";"); WriteLine(); + + // Remove the synthetic requires to avoid mutating the shared AST. + if (syntheticReq != null) { + node.Requires.Remove(syntheticReq); + } } return node; diff --git a/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl b/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl new file mode 100644 index 0000000000..05da4154ba --- /dev/null +++ b/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl @@ -0,0 +1,16 @@ +// Regression test: assert_. procedure with an existing ensures clause +// should produce a single merged spec block, not two separate spec blocks. +// Bug: VisitProcedure emitted a second spec { requires ... } block in addition +// to the one already emitted by WriteProcedureHeader for existing ensures. + +type i32 = int; + +procedure assert_.i32(p.0: i32) returns ($r: i32); + ensures ($r == 0); + +procedure main() returns ($r: i32) +{ + // assert(true) -- should pass because p.0 != 0 holds for 1 + call $r := assert_.i32(1); + return; +} From 7cf444c2fb58c2d6bdfeeb7b21fa9dd6330da482 Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 11 May 2026 10:31:02 -0700 Subject: [PATCH 07/21] fix: replace silent IdentifierExpr.Decl null fallback with exception Two IdentifierExpr emission sites (EmitOldExpr and VisitExpr) used a ternary fallback: Decl != null ? NameOf(...) : Name(...). When Decl was null, this silently fell back to Name(), emitting the raw sanitized name without consulting the rename map -- wrong in name-collision scenarios. Post-Boogie-resolution, Decl is always non-null. Replace both fallbacks with explicit null checks that throw StrataConversionException, then always use NameOf(). Added OldExprRenameCollision.bpl and OldExprUsesRenamedNameOnCollision integration test verifying old() uses the renamed name on collision. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../BoogieToStrataIntegrationTests.cs | 32 +++++++++++++++++++ .../BoogieToStrata/Source/StrataGenerator.cs | 10 ++++-- .../Tests/OldExprRenameCollision.bpl | 17 ++++++++++ 3 files changed, 57 insertions(+), 2 deletions(-) create mode 100644 Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs index 8679454511..fcbea5e86f 100644 --- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs +++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs @@ -181,6 +181,38 @@ public void SmackAssertWithEnsuresProducesSingleSpecBlock() { Assert.Contains("ensures", standardOutput); } + /// + /// Regression test: old() expressions must use the renamed name when a + /// variable has a name collision (e.g., global var `main` vs procedure `main`). + /// Previously, IdentifierExpr with Decl != null used NameOf() correctly, but + /// had a silent fallback to Name() when Decl was null — which would emit the + /// unrenamed (wrong) name in the collision case. Post-resolution, Decl should + /// always be non-null; the fallback masked potential bugs. + /// + [Fact] + public void OldExprUsesRenamedNameOnCollision() { + var filePath = Path.Combine(TestsDirectory, "OldExprRenameCollision.bpl"); + Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}"); + + var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath); + + output.WriteLine($"Output:\n{standardOutput}"); + if (!string.IsNullOrEmpty(errorOutput)) { + output.WriteLine($"Error output: {errorOutput}"); + } + + Assert.Equal(0, exitCode); + + // The output should contain an `old` expression referencing the *renamed* + // variable (e.g., __var_main), not the raw name `main` which is the procedure. + // Look for the pattern "old __var_main" or similar renamed form. + Assert.Contains("old __var_main", standardOutput); + + // Also ensure the output does NOT contain "old main" (unrenamed fallback). + // This would indicate the fallback to Name() was used instead of NameOf(). + Assert.DoesNotContain("old main", standardOutput); + } + [Fact] public void ErrorCodeWithNoArguments() { var result = BoogieToStrata.Main(Array.Empty()); diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 3d7bca5e6f..9d20638e82 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -354,7 +354,10 @@ private void EmitOldExpr(Expr expr) { switch (expr) { case IdentifierExpr identExpr: WriteText("old "); - WriteText(identExpr.Decl != null ? NameOf(identExpr.Decl, identExpr.Name) : Name(identExpr.Name)); + if (identExpr.Decl == null) + throw new StrataConversionException(identExpr.tok, + $"IdentifierExpr '{identExpr.Name}' has null Decl (expected non-null post-resolution)"); + WriteText(NameOf(identExpr.Decl, identExpr.Name)); break; case NAryExpr { Fun: MapSelect } mapSelect: WriteText("("); @@ -590,7 +593,10 @@ public override Expr VisitExpr(Expr node) { case LiteralExpr literalExpr: throw new StrataConversionException(node.tok, $"Unsupported literal type: {literalExpr}"); case IdentifierExpr identifierExpr: - WriteText(identifierExpr.Decl != null ? NameOf(identifierExpr.Decl, identifierExpr.Name) : Name(identifierExpr.Name)); + if (identifierExpr.Decl == null) + throw new StrataConversionException(identifierExpr.tok, + $"IdentifierExpr '{identifierExpr.Name}' has null Decl (expected non-null post-resolution)"); + WriteText(NameOf(identifierExpr.Decl, identifierExpr.Name)); break; case NAryExpr nAryExpr: { var fun = nAryExpr.Fun; diff --git a/Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl new file mode 100644 index 0000000000..7494acd002 --- /dev/null +++ b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl @@ -0,0 +1,17 @@ +// Regression test: old() expression with a renamed (colliding) variable. +// +// The global variable `main` collides with procedure `main` after +// sanitization (cross-namespace collision). The variable must be +// renamed when emitted. An old() expression referencing that variable +// must use the *renamed* name, not the raw sanitized name. +// If the code silently falls back to Name() instead of NameOf(), the +// old() expression will reference the wrong (procedure) name. + +var main: int; + +procedure main() + modifies main; + ensures main == old(main) + 1; +{ + main := main + 1; +} From f568f65fbcde35ef9e4dafde2f8fe7bab677b49c Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 11 May 2026 10:36:39 -0700 Subject: [PATCH 08/21] test: add regression test for InferModifies=true on Boogie without modifies clauses SMACK-generated Boogie can omit explicit modifies clauses. InferModifies=true causes Boogie's ModSetCollector to infer them, so the translator correctly emits globals as inout parameters. This test catches regressions if Boogie ever stops inferring or the option is accidentally disabled. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../BoogieToStrataIntegrationTests.cs | 33 +++++++++++++++++++ .../Tests/InferModifiesGlobal.bpl | 16 +++++++++ 2 files changed, 49 insertions(+) create mode 100644 Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs index fcbea5e86f..1aeacb601e 100644 --- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs +++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs @@ -213,6 +213,39 @@ public void OldExprUsesRenamedNameOnCollision() { Assert.DoesNotContain("old main", standardOutput); } + /// + /// Regression test for InferModifies = true. + /// + /// SMACK-generated Boogie can omit explicit modifies clauses on procedures. + /// With InferModifies = true, Boogie's ModSetCollector infers them so that + /// the translator correctly emits globals as `inout` parameters (modified) + /// rather than read-only parameters. + /// + /// This test uses a .bpl file where procedure p() assigns to global g but + /// has no `modifies g;` clause. If InferModifies is working, the output + /// should contain `inout g` for procedure p. + /// + [Fact] + public void InferModifiesEmitsInoutForMutatedGlobal() { + var filePath = Path.Combine(TestsDirectory, "InferModifiesGlobal.bpl"); + Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}"); + + var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath); + + output.WriteLine($"Output:\n{standardOutput}"); + if (!string.IsNullOrEmpty(errorOutput)) { + output.WriteLine($"Error output: {errorOutput}"); + } + + // Translation must succeed — if InferModifies is broken, Boogie would + // reject the program because g is assigned without a modifies clause. + Assert.Equal(0, exitCode); + + // The inferred modifies clause should cause the translator to emit + // `inout g` on procedure p's parameter list. + Assert.Contains("inout g", standardOutput); + } + [Fact] public void ErrorCodeWithNoArguments() { var result = BoogieToStrata.Main(Array.Empty()); diff --git a/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl new file mode 100644 index 0000000000..5a92c580b5 --- /dev/null +++ b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl @@ -0,0 +1,16 @@ +// Regression test for InferModifies = true. +// +// This procedure mutates the global variable `g` but has NO explicit +// `modifies g;` clause. With InferModifies = true, Boogie's +// ModSetCollector should infer the modifies clause so that the +// BoogieToStrata translator emits `inout g` for procedure p. +// If InferModifies is ever disabled or broken, this file will fail +// to translate correctly (g would be treated as read-only instead +// of inout). + +var g: int; + +procedure p() +{ + g := 1; +} From 3a7fb9099720df9eec8e0cc654a8813799bfe376 Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 11 May 2026 10:45:26 -0700 Subject: [PATCH 09/21] refactor: extract ClaimOrRename into static method and document InferModifies Extract the ClaimOrRename local closure from EmitProgramAsStrata into a private static method on StrataGenerator, passing the claimed set and renames dictionary as explicit parameters. Documentation additions: - Expand _renames field comment to describe the registration order (procs first, then impls defensively, then consts/funcs/globals) - Add comment on implementation loop explaining it is defensive - Document InferModifies=true motivation in BoogieToStrata.cs Co-Authored-By: Claude Opus 4.6 (1M context) --- Tools/BoogieToStrata/Source/BoogieToStrata.cs | 4 ++ .../BoogieToStrata/Source/StrataGenerator.cs | 54 +++++++++++++------ 2 files changed, 42 insertions(+), 16 deletions(-) diff --git a/Tools/BoogieToStrata/Source/BoogieToStrata.cs b/Tools/BoogieToStrata/Source/BoogieToStrata.cs index 3ee6cc63c2..a2b1d04b14 100644 --- a/Tools/BoogieToStrata/Source/BoogieToStrata.cs +++ b/Tools/BoogieToStrata/Source/BoogieToStrata.cs @@ -19,6 +19,10 @@ public static int Main(string[] args) { var options = new CommandLineOptions(Console.Out, new ConsolePrinter()) { Verify = false, TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates, + // SMACK-generated Boogie often omits explicit `modifies` clauses on procedures that mutate globals. + // InferModifies runs ModSetCollector.CollectModifies to populate empty modifies clauses and + // suppresses modifies-clause typechecking (via CheckModifies), so that ResolveAndTypecheck + // does not reject SMACK programs missing modifies clauses. InferModifies = true }; diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 9d20638e82..724396f6f9 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -56,6 +56,13 @@ public class StrataGenerator : ReadOnlyVisitor { // declaration. Keyed by Boogie Declaration object to avoid ambiguity // when two entities share the same original name (e.g., const main and // procedure main). First-seen wins; later entities get prefixed. + // + // Registration order determines who wins a collision: + // 1. Procedures — registered first, always keep their name. + // 2. Implementations — claimed defensively (they share names with + // their procedures, but claiming guards against edge cases). + // 3. Constants, Functions, Globals — registered last; in a + // proc-vs-const collision the constant is always renamed. private readonly Dictionary _renames = new(); private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program) { @@ -87,30 +94,22 @@ public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTex // First-seen wins; colliding entities get a suffix (_2, _3, ...). var claimed = new HashSet(); - void ClaimOrRename(Declaration decl, string originalName, string prefix) { - var sanitized = SanitizeNameForStrata(originalName); - if (claimed.Add(sanitized)) return; - var candidate = $"{prefix}{sanitized}"; - if (!claimed.Add(candidate)) { - var i = 2; - while (!claimed.Add($"{candidate}_{i}")) i++; - candidate = $"{candidate}_{i}"; - } - generator._renames[decl] = candidate; - } - foreach (var proc in p.Procedures) - ClaimOrRename(proc, proc.Name, "__proc_"); + ClaimOrRename(proc, proc.Name, "__proc_", claimed, generator._renames); + // Defensive: implementations share names with their corresponding + // procedures, so they would normally never collide. Claiming them + // here guards against edge cases (e.g., an implementation whose + // procedure was pruned or renamed upstream). foreach (var impl in p.Implementations) { var sanitized = SanitizeNameForStrata(impl.Name); claimed.Add(sanitized); } foreach (var c in liveDeclarations.OfType()) - ClaimOrRename(c, c.TypedIdent.Name, "__const_"); + ClaimOrRename(c, c.TypedIdent.Name, "__const_", claimed, generator._renames); foreach (var f in liveDeclarations.OfType()) - ClaimOrRename(f, f.Name, "__func_"); + ClaimOrRename(f, f.Name, "__func_", claimed, generator._renames); foreach (var g in p.GlobalVariables) - ClaimOrRename(g, g.Name, "__var_"); + ClaimOrRename(g, g.Name, "__var_", claimed, generator._renames); var typeConstructors = p.TopLevelDeclarations.OfType().ToList(); if (typeConstructors.Count != 0) { @@ -243,6 +242,29 @@ private static string SanitizeNameForStrata(string name) { .Replace("$", "_"); } + /// + /// Claim a sanitized name for , or rename it if the + /// name is already taken. The first declaration to claim a name wins; + /// subsequent colliders get a prefixed (and possibly suffixed) name recorded + /// in . + /// + private static void ClaimOrRename( + Declaration decl, + string originalName, + string prefix, + HashSet claimed, + Dictionary renames) { + var sanitized = SanitizeNameForStrata(originalName); + if (claimed.Add(sanitized)) return; + var candidate = $"{prefix}{sanitized}"; + if (!claimed.Add(candidate)) { + var i = 2; + while (!claimed.Add($"{candidate}_{i}")) i++; + candidate = $"{candidate}_{i}"; + } + renames[decl] = candidate; + } + private void AddUniqueConst(Type t, string name) { if (!_uniqueConstants.TryGetValue(t, out var value)) { value = new HashSet(); From c3d59772cee4d02815fe1fc54b075a8727312b33 Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 18 May 2026 10:44:21 -0700 Subject: [PATCH 10/21] fix: wrap synthetic Requires mutation in try/finally The VisitProcedure assert_. handler adds a synthetic Requires to node.Requires before calling WriteProcedureHeader and removes it after. The unconditional removal at the end of the if-block leaks the synthetic Requires onto the shared Boogie AST if WriteProcedureHeader (or anything it transitively calls) throws. Wrap the WriteProcedureHeader call in try/finally so the synthetic Requires is always removed, matching the invariant the surrounding comment promises. --- Tools/BoogieToStrata/Source/StrataGenerator.cs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 724396f6f9..dc8c960cda 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -1860,13 +1860,16 @@ public override Procedure VisitProcedure(Procedure node) { node.Requires.Add(syntheticReq); } - WriteProcedureHeader(node); - WriteLine(";"); - WriteLine(); - - // Remove the synthetic requires to avoid mutating the shared AST. - if (syntheticReq != null) { - node.Requires.Remove(syntheticReq); + try { + WriteProcedureHeader(node); + WriteLine(";"); + WriteLine(); + } finally { + // Remove the synthetic requires to avoid mutating the shared + // AST, even if WriteProcedureHeader threw. + if (syntheticReq != null) { + node.Requires.Remove(syntheticReq); + } } } From 2f2f649dc1584988690026097a7913ee0f0a1372 Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 18 May 2026 10:44:27 -0700 Subject: [PATCH 11/21] test: add .expect for OldExprRenameCollision Without a .expect file, VerifyTestFile runs the .core.st through the verifier with --check (parse-only), which gives no end-to-end coverage that the renamed name in old() actually translates to a sound VC. Add a .expect with the expected single ensures-goal pass so the verification path runs and asserts an exact-match result, matching the standard the other regression tests in this PR follow. --- Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect diff --git a/Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect new file mode 100644 index 0000000000..98a3632dbf --- /dev/null +++ b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect @@ -0,0 +1,3 @@ +Successfully parsed. +OldExprRenameCollision.core.st(10, 2) [main_ensures_0]: ✅ pass +All 1 goals passed. From 040482e40538b29eeebd7d61ac43ca3e341762b6 Mon Sep 17 00:00:00 2001 From: David Deng Date: Mon, 18 May 2026 10:44:54 -0700 Subject: [PATCH 12/21] test: add .expect for InferModifiesGlobal MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Without a .expect file, VerifyTestFile runs with --check (parse-only). Add a .expect (`All 0 goals passed.` — the procedure has no specs or asserts) so the verifier actually consumes the .core.st output and the test exercises the full end-to-end path, matching the standard the other regression tests in this PR follow. --- Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect diff --git a/Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect new file mode 100644 index 0000000000..e9e8e85d9e --- /dev/null +++ b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect @@ -0,0 +1,2 @@ +Successfully parsed. +All 0 goals passed. From 1edc5994be92667828d6a4975e9a60e957f9b8df Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 14:58:12 -0700 Subject: [PATCH 13/21] refactor: thread smack parameter into StrataGenerator No behavior change. Plumbs a new bool smack param through EmitProgramAsStrata into the generator constructor, hardcoded to true at the single call site. Subsequent commits gate SMACK-specific behavior on this flag and wire it to a CLI option. --- Tools/BoogieToStrata/Source/BoogieToStrata.cs | 4 +++- Tools/BoogieToStrata/Source/StrataGenerator.cs | 12 +++++++++--- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/Tools/BoogieToStrata/Source/BoogieToStrata.cs b/Tools/BoogieToStrata/Source/BoogieToStrata.cs index a2b1d04b14..09f81bce18 100644 --- a/Tools/BoogieToStrata/Source/BoogieToStrata.cs +++ b/Tools/BoogieToStrata/Source/BoogieToStrata.cs @@ -5,7 +5,9 @@ namespace BoogieToStrata; public static class BoogieToStrata { private static void PrintResolvedProgram(ExecutionEngineOptions options, ProcessedProgram prog) { var writer = new TokenTextWriter(Console.Out, options); - StrataGenerator.EmitProgramAsStrata(options, prog.Program, writer); + // smack: true here preserves pre-task behavior; Task 3 wires the real value + // from the parsed CLI flag. + StrataGenerator.EmitProgramAsStrata(options, prog.Program, writer, smack: true); } public static int Main(string[] args) { diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index dc8c960cda..dad5f59cad 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -64,15 +64,21 @@ public class StrataGenerator : ReadOnlyVisitor { // 3. Constants, Functions, Globals — registered last; in a // proc-vs-const collision the constant is always renamed. private readonly Dictionary _renames = new(); + // True when the input is SMACK-generated Boogie. Gates SMACK-specific + // accommodations (synthetic `requires (p != 0)` on assert_. procedures). + // The companion `InferModifies = true` knob is set on the Boogie options + // by the BoogieToStrata.Main entrypoint, also gated on this flag. + private readonly bool _smack; - private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program) { + private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program, bool smack) { _options = options; _writer = writer; _program = program; + _smack = smack; } - public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTextWriter writer) { - var generator = new StrataGenerator(options, writer, p); + public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTextWriter writer, bool smack) { + var generator = new StrataGenerator(options, writer, p, smack); var fieldTypeCollector = new FieldTypeCollector(); fieldTypeCollector.Visit(p); From 6fb6f9c1959b9b70d006572e07971f9fe0e9d04a Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:02:51 -0700 Subject: [PATCH 14/21] feat: gate assert_. requires injection on smack flag VisitProcedure now consults the _smack field set by the constructor. The Requires.Count == 0 guard is removed: when the assert_. pattern matches under --smack, the synthetic `requires (p != 0)` is injected unconditionally, alongside any pre-existing requires/ensures. WriteProcedureHeader still emits a single merged spec block. Addresses MikaelMayer's review comment on PR #1149: the previous guard silently dropped the SMACK invariant when a pre-existing requires was present. --- Tools/BoogieToStrata/Source/StrataGenerator.cs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index dad5f59cad..ad269fc77a 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -1850,14 +1850,17 @@ private void WriteProcedureHeader(Procedure proc) { public override Procedure VisitProcedure(Procedure node) { if (!_program.Implementations.Any(i => i.Name.Equals(node.Name))) { - // SMACK encodes C assert(expr) as a call to assert_.*(cond). - // Inject a synthetic requires precondition so the call-elimination - // pass generates a VC checking the condition is non-zero. - // We add it to node.Requires so WriteProcedureHeader emits it - // inside a single spec block alongside any existing specs. + // Under --smack, SMACK encodes C assert(expr) as a call to + // assert_.*(cond). Inject a synthetic requires precondition so the + // call-elimination pass generates a VC checking the condition is + // non-zero. We add it to node.Requires so WriteProcedureHeader + // emits it inside a single spec block alongside any existing + // specs. The injection always fires when the name pattern matches + // (no Requires.Count == 0 guard) — if the procedure already has a + // hand-written requires, both clauses appear in the merged spec + // block, preserving the SMACK invariant unconditionally. Requires? syntheticReq = null; - if (node.Name.StartsWith("assert_.") && node.InParams.Count > 0 - && node.Requires.Count == 0) { + if (_smack && node.Name.StartsWith("assert_.") && node.InParams.Count > 0) { var param = node.InParams[0]; var paramExpr = new IdentifierExpr(param.tok, param); var zero = new LiteralExpr(param.tok, Microsoft.BaseTypes.BigNum.FromInt(0)); From 7950fc2600c8e1928c9dba3965efca2d0f273cee Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:14:25 -0700 Subject: [PATCH 15/21] feat: add --smack CLI flag to BoogieToStrata --smack enables two SMACK-specific accommodations: InferModifies=true (plus ModSetCollector mutation and CheckModifies suppression for missing modifies clauses) and the synthetic `requires (p != 0)` injection on assert_. procedures. Without the flag, the translator runs in strict Boogie mode. Manual arg parsing (no new package dep). The flag may appear before or after the positional filename. Unknown flags or wrong arg count print the usage banner and exit 1. --- Tools/BoogieToStrata/Source/BoogieToStrata.cs | 54 ++++++++++++++----- 1 file changed, 42 insertions(+), 12 deletions(-) diff --git a/Tools/BoogieToStrata/Source/BoogieToStrata.cs b/Tools/BoogieToStrata/Source/BoogieToStrata.cs index 09f81bce18..de97643552 100644 --- a/Tools/BoogieToStrata/Source/BoogieToStrata.cs +++ b/Tools/BoogieToStrata/Source/BoogieToStrata.cs @@ -3,29 +3,59 @@ namespace BoogieToStrata; public static class BoogieToStrata { + private const string Usage = "Usage: BoogieToStrata [--smack] "; + + private static bool _smack; + private static void PrintResolvedProgram(ExecutionEngineOptions options, ProcessedProgram prog) { var writer = new TokenTextWriter(Console.Out, options); - // smack: true here preserves pre-task behavior; Task 3 wires the real value - // from the parsed CLI flag. - StrataGenerator.EmitProgramAsStrata(options, prog.Program, writer, smack: true); + StrataGenerator.EmitProgramAsStrata(options, prog.Program, writer, _smack); + } + + /// + /// Parse args into (smack, filename). Returns false on any malformed + /// invocation (zero or two-plus positional args, unknown flags); the + /// caller should print Usage and return exit code 1. + /// + private static bool TryParseArgs(string[] args, out bool smack, out string filename) { + smack = false; + filename = ""; + string? positional = null; + foreach (var arg in args) { + if (arg == "--smack") { + smack = true; + } else if (arg.StartsWith("--")) { + return false; // unknown flag + } else if (positional == null) { + positional = arg; + } else { + return false; // two positional args + } + } + if (positional == null) return false; // no positional arg + filename = positional; + return true; } public static int Main(string[] args) { - if (args.Length != 1) { - Console.Error.WriteLine("Usage: BoogieToStrata "); + if (!TryParseArgs(args, out var smack, out var filename)) { + Console.Error.WriteLine(Usage); return 1; } - - var filename = args[0]; + _smack = smack; var options = new CommandLineOptions(Console.Out, new ConsolePrinter()) { Verify = false, TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates, - // SMACK-generated Boogie often omits explicit `modifies` clauses on procedures that mutate globals. - // InferModifies runs ModSetCollector.CollectModifies to populate empty modifies clauses and - // suppresses modifies-clause typechecking (via CheckModifies), so that ResolveAndTypecheck + // Under --smack, SMACK-generated Boogie often omits explicit + // `modifies` clauses on procedures that mutate globals. + // InferModifies runs ModSetCollector.CollectModifies to populate + // empty modifies clauses and suppresses modifies-clause + // typechecking (via CheckModifies), so that ResolveAndTypecheck // does not reject SMACK programs missing modifies clauses. - InferModifies = true + // For strict Boogie input (no --smack), this stays false and + // missing modifies clauses are reported as typecheck errors. + InferModifies = smack }; var boogieEngine = ExecutionEngine.CreateWithoutSharedCache(options); @@ -51,4 +81,4 @@ public static int Main(string[] args) { return 0; } -} \ No newline at end of file +} From c62d5299f7b6da7521c99864d47c88cacfd5945e Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:19:51 -0700 Subject: [PATCH 16/21] test: make integration runner marker-aware for --smack RunTranslation(filePath) now reads the first 5 lines of the .bpl and passes --smack when the literal token {:smack} is present. The new RunTranslation(filePath, bool smack) overload is the explicit form, used by tests that pin down the off-by-default behavior. --- .../BoogieToStrataIntegrationTests.cs | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs index 1aeacb601e..076d190031 100644 --- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs +++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs @@ -51,7 +51,28 @@ public static IEnumerable GetBoogieTestFiles() { } } + /// + /// Returns true if the first 5 lines of contain + /// the literal token "{:smack}". Files carrying this marker opt into the + /// --smack CLI flag, which gates the assert_. synthetic-requires + /// injection and InferModifies=true. + /// + private static bool HasSmackMarker(string filePath) { + if (!File.Exists(filePath)) return false; + using var reader = new StreamReader(filePath); + for (var i = 0; i < 5; i++) { + var line = reader.ReadLine(); + if (line == null) break; + if (line.Contains("{:smack}", StringComparison.Ordinal)) return true; + } + return false; + } + private (int, string, string) RunTranslation(string filePath) { + return RunTranslation(filePath, HasSmackMarker(filePath)); + } + + private (int, string, string) RunTranslation(string filePath, bool smack) { // Capture console output using var consoleOutput = new StringWriter(); using var consoleError = new StringWriter(); @@ -62,7 +83,8 @@ public static IEnumerable GetBoogieTestFiles() { try { Console.SetOut(consoleOutput); Console.SetError(consoleError); - exitCode = BoogieToStrata.Main([filePath]); + var args = smack ? new[] { "--smack", filePath } : new[] { filePath }; + exitCode = BoogieToStrata.Main(args); } catch (Exception) { exitCode = 1; } finally { From 5297e8dbfd80d756b8b99b1381b2fde55b8acad4 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:24:51 -0700 Subject: [PATCH 17/21] test: add {:smack} marker and remove stale comment in SmackAssert.bpl MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the per-file {:smack} marker so the integration runner passes --smack. Also removes the stale paragraph at lines 7-9 that described pre-fix behavior ("currently produces 'All 0 goals passed'") — after the assert_. fix landed, the test now produces a verification failure as captured in SmackAssert.expect. Addresses MikaelMayer's review comment on PR #1149. --- Tools/BoogieToStrata/Tests/SmackAssert.bpl | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Tools/BoogieToStrata/Tests/SmackAssert.bpl b/Tools/BoogieToStrata/Tests/SmackAssert.bpl index 01ae42e412..5094a86704 100644 --- a/Tools/BoogieToStrata/Tests/SmackAssert.bpl +++ b/Tools/BoogieToStrata/Tests/SmackAssert.bpl @@ -1,12 +1,9 @@ +// {:smack} // Minimal test case for SMACK assert_ pattern recognition. // SMACK encodes C assert(expr) as a call to assert_.i32(cond). // BoogieToStrata should recognize this pattern and emit: // assert (cond != 0); // instead of an opaque procedure call. -// -// This test passes 0 (false) to assert — it should be a verification -// failure, but currently produces "All 0 goals passed" because the -// call is treated as opaque. type i32 = int; From 5a1beaaf991f7e00b07b2773f483a6ce77d55a7b Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:29:08 -0700 Subject: [PATCH 18/21] test: extend SmackAssertDuplicateSpec for requires-already-present case Adds a second assert_. procedure (assert_.i32_with_req) with a hand-written `requires (p.0 > -1)` and asserts that the output spec block contains BOTH the synthetic `requires (p.0 != 0)` and the user-written one. This pins down the post-fix behavior of dropping the Requires.Count == 0 guard: the SMACK invariant is preserved unconditionally, alongside any pre-existing requires. Renames the test method to SmackAssertProducesSingleMergedSpecBlock to reflect the broader coverage. Adds {:smack} marker to the .bpl. Note: name sanitization rewrites `p.0` -> `p_0` and the unary literal `-1` is emitted as `-(1)`, so the assertions match `p_0 != 0` and `p_0 > -(1)` against the actual output. Addresses MikaelMayer's review comment on PR #1149. --- .../BoogieToStrataIntegrationTests.cs | 41 +++++++++++++++---- .../Tests/SmackAssertDuplicateSpec.bpl | 22 ++++++++-- 2 files changed, 51 insertions(+), 12 deletions(-) diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs index 076d190031..fb16dc13a5 100644 --- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs +++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs @@ -172,20 +172,24 @@ public void VerifyTestFile(string fileName, string filePath) { } /// - /// Regression test: an assert_. procedure with an existing ensures clause - /// should emit a single spec block containing both the synthetic requires and the - /// original ensures — not two separate spec blocks. + /// Regression test: assert_. procedures must produce a single + /// merged spec block, not duplicates, regardless of whether the input + /// already has user-written specs. Two cases: + /// 1. existing ensures only — synthetic requires merges in. + /// 2. existing requires — synthetic requires is added alongside, + /// not silently dropped. /// [Fact] - public void SmackAssertWithEnsuresProducesSingleSpecBlock() { + public void SmackAssertProducesSingleMergedSpecBlock() { var filePath = Path.Combine(TestsDirectory, "SmackAssertDuplicateSpec.bpl"); Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}"); var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath); Assert.Equal(0, exitCode); - // Count occurrences of "spec {" in the output. - // There should be exactly one spec block for the assert_ procedure. + // Three procedures (assert_.i32, assert_.i32_with_req, main); the two + // assert_. ones each produce one spec block; main has none. + // Count occurrences of "spec {" in the output: must be exactly 2. var specCount = 0; var searchFrom = 0; while (true) { @@ -196,11 +200,32 @@ public void SmackAssertWithEnsuresProducesSingleSpecBlock() { } output.WriteLine($"Output:\n{standardOutput}"); - Assert.Equal(1, specCount); + Assert.Equal(2, specCount); - // The single spec block should contain both requires and ensures + // Overall sanity: the output contains at least one of each clause kind. + // (assert_.i32 has an `ensures`, both procedures have at least one + // `requires`.) Assert.Contains("requires", standardOutput); Assert.Contains("ensures", standardOutput); + + // The critical regression check: BOTH clauses must appear in the + // SECOND procedure's spec block (assert_.i32_with_req) — i.e., the + // requires-already-present case must not silently drop the synthetic + // clause. Procedures emit in source order, so the second `spec {` is + // assert_.i32_with_req's. + var firstSpec = standardOutput.IndexOf("spec {", StringComparison.Ordinal); + Assert.True(firstSpec >= 0, "Expected at least one spec block"); + var secondSpecStart = standardOutput.IndexOf("spec {", firstSpec + 1, StringComparison.Ordinal); + Assert.True(secondSpecStart >= 0, "Expected a second spec block for assert_.i32_with_req"); + var secondSpecEnd = standardOutput.IndexOf("}", secondSpecStart, StringComparison.Ordinal); + Assert.True(secondSpecEnd > secondSpecStart, "Second spec block missing closing brace"); + var secondSpec = standardOutput.Substring(secondSpecStart, secondSpecEnd - secondSpecStart); + + // The user-written `requires (p.0 > -1)` (sanitized to `p_0 > -(1)`) + // and the synthetic `requires (p.0 != 0)` (sanitized to `p_0 != 0`) + // must both be present in this single spec block. + Assert.Contains("p_0 > -(1)", secondSpec); + Assert.Contains("p_0 != 0", secondSpec); } /// diff --git a/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl b/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl index 05da4154ba..3f3d49bce3 100644 --- a/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl +++ b/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl @@ -1,16 +1,30 @@ -// Regression test: assert_. procedure with an existing ensures clause -// should produce a single merged spec block, not two separate spec blocks. -// Bug: VisitProcedure emitted a second spec { requires ... } block in addition -// to the one already emitted by WriteProcedureHeader for existing ensures. +// {:smack} +// Regression test: assert_. procedures must produce a single +// merged spec block, not duplicates, regardless of whether the input +// already has user-written specs. +// +// Two procedures exercise the two cases: +// 1. assert_.i32 has only an existing `ensures` — output must merge +// the synthetic `requires (p.0 != 0)` with the existing ensures +// into one spec block. +// 2. assert_.i32_with_req has an existing `requires (p.0 > -1)` — +// output must contain BOTH requires clauses (the synthetic one +// and the user-written one) in a single spec block, not drop the +// synthetic one. type i32 = int; procedure assert_.i32(p.0: i32) returns ($r: i32); ensures ($r == 0); +procedure assert_.i32_with_req(p.0: i32) returns ($r: i32); + requires (p.0 > -1); + procedure main() returns ($r: i32) { // assert(true) -- should pass because p.0 != 0 holds for 1 call $r := assert_.i32(1); + // call assert_.i32_with_req(1) — both `1 != 0` and `1 > -1` hold + call $r := assert_.i32_with_req(1); return; } From b71dce3eda8317b165dace4fc1cf42ecc3814c69 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:41:30 -0700 Subject: [PATCH 19/21] test: add {:smack} marker to AssertPrefixFalsePositive.bpl This regression test proves that even under --smack, names like assert_helper (no literal dot) do NOT receive the synthetic requires. The marker is required for the test to actually exercise the --smack-on path; without it, the test would only prove the gate is closed when --smack is off, which is uninteresting. --- Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl | 1 + 1 file changed, 1 insertion(+) diff --git a/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl index 36ab20b483..50bdf5579f 100644 --- a/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl +++ b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl @@ -1,3 +1,4 @@ +// {:smack} // Regression test: procedures starting with "assert_" but NOT matching // SMACK's assert_.TYPE pattern should NOT get a synthetic requires. // Only assert_. (literal dot) is the SMACK pattern. From 1010757061ff74bf0f5d16679ed0f146f8ef4552 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:41:37 -0700 Subject: [PATCH 20/21] test: add {:smack} marker to InferModifiesGlobal.bpl This file relies on InferModifies = true, which is now gated on the --smack flag. The marker tells the integration runner to pass --smack when translating this file. Without the flag, the file deliberately fails Boogie typechecking (no explicit `modifies g;` clause); a companion test in the next task pins down that strict-mode failure. --- Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl | 1 + 1 file changed, 1 insertion(+) diff --git a/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl index 5a92c580b5..0767f22518 100644 --- a/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl +++ b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl @@ -1,3 +1,4 @@ +// {:smack} // Regression test for InferModifies = true. // // This procedure mutates the global variable `g` but has NO explicit From 48ba8a3b223f5fba3ed41f23ee263c40fbdcda84 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:52:04 -0700 Subject: [PATCH 21/21] test: pin down --smack off-by-default behavior MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two new facts assert that the SMACK-specific accommodations are gated behind --smack: 1. SmackAssertWithoutFlagDoesNotInjectRequires — translates SmackAssert.bpl without --smack and asserts the output has no `requires` clause (the assert_. pattern is treated as opaque). 2. InferModifiesOffWithoutSmackFlag — translates InferModifiesGlobal.bpl without --smack and asserts the run exits non-zero (Boogie rejects the program for the missing `modifies g;` clause). --- .../BoogieToStrataIntegrationTests.cs | 54 +++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs index fb16dc13a5..2f921c041b 100644 --- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs +++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs @@ -293,6 +293,60 @@ public void InferModifiesEmitsInoutForMutatedGlobal() { Assert.Contains("inout g", standardOutput); } + /// + /// Pin down the --smack gate: without the flag, the assert_. + /// pattern is treated as an opaque procedure (no synthetic requires + /// injected). Translation succeeds; the output does not contain a + /// requires clause for the assert_ procedure. + /// + [Fact] + public void SmackAssertWithoutFlagDoesNotInjectRequires() { + var filePath = Path.Combine(TestsDirectory, "SmackAssert.bpl"); + Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}"); + + var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath, smack: false); + + output.WriteLine($"Output:\n{standardOutput}"); + if (!string.IsNullOrEmpty(errorOutput)) { + output.WriteLine($"Error output: {errorOutput}"); + } + + Assert.Equal(0, exitCode); + + // Without --smack, no synthetic requires is added, so no `requires` + // clause should appear anywhere in the translation of this file + // (the .bpl has no user-written requires either). + Assert.DoesNotContain("requires", standardOutput); + } + + /// + /// Pin down the --smack gate: without the flag, InferModifies is off. + /// A program that omits an explicit `modifies` clause on a procedure + /// that mutates a global is rejected at typecheck. + /// + [Fact] + public void InferModifiesOffWithoutSmackFlag() { + var filePath = Path.Combine(TestsDirectory, "InferModifiesGlobal.bpl"); + Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}"); + + var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath, smack: false); + + output.WriteLine($"Exit code: {exitCode}"); + output.WriteLine($"Output:\n{standardOutput}"); + if (!string.IsNullOrEmpty(errorOutput)) { + output.WriteLine($"Error output: {errorOutput}"); + } + + // Without --smack, ResolveAndTypecheck rejects the program because + // procedure p mutates global g without an explicit `modifies g;` + // clause. BoogieToStrata.Main writes a "Failed to typecheck" line + // to stderr and returns exit code 1. Pin both signals so a future + // regression that fails for an unrelated reason (parse error, + // arg-handling change) doesn't silently pass this test. + Assert.Equal(1, exitCode); + Assert.Contains("Failed to typecheck", errorOutput); + } + [Fact] public void ErrorCodeWithNoArguments() { var result = BoogieToStrata.Main(Array.Empty());