Enable fatal warnings and fix compiler warnings throughout codebase - #590
Enable fatal warnings and fix compiler warnings throughout codebase#590jcp19 wants to merge 3 commits into
Conversation
Enable -Xfatal-warnings for the Carbon project (Silver is left unchanged, since it is a separate repository) and fix every warning it reports, without changing the behaviour of the program: - Remove unused imports. - Give public implicit definitions explicit result types. - Replace unused pattern variables and lambda/binder names with `_`. - Annotate intentionally unused parameters, private members and locals with `@unused` instead of deleting them, so that no initialisation side effects (e.g. fresh identifier/namespace allocation, `env.define`) are lost. - Drop default arguments of private methods that no call site relies on. - Turn `var`s that are never reassigned into `val`s. - `reset` / `sumOfStatesAxiomRequired`: align the empty parameter lists with the ones declared in the overridden methods. - Replace deprecated usages: the implicit `Array`-to-`Seq` conversion in `Carbon.main`, mutable `Map.+`, and procedure syntax in the tests. - Mark the deliberately partial `match`es on access predicates as `@unchecked`; they keep throwing a `MatchError` for unhandled inputs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01W9SJYwJrGzRj71r7Kg1yvD
The previous commit annotated every unused binding with `@unused`. That is the right call only when the initialiser has side effects; where it does not, the annotation just silences the compiler on code that should be removed. Delete the bindings whose initialisers are provably pure: - `specialRef`/`specialRefName`, `mask1`, `mask2`, `oldVersion` (FuncPred) - `qpHeap`/`qpHeapName` (Heap) - `permAddName`, `permSubName`, `permDivName`, `translatedLocal`, `permVar` and the unused private `maskUpdate` overload (QuantifiedPerm) - `nofractionsStmt` (Wand) - `currentMethodIsAbstract` and its two write-only assignments (Loop) Two are rewritten to keep the side effect without the discarded result: `getCopyState` uses a plain `for` instead of a `for`/`yield` whose list was thrown away, and the `env.define` loop uses `foreach` instead of `map`. The remaining `@unused` value bindings are deliberately kept, because evaluating them has effects the program depends on: - `obj2`, `field2`, `predField` (Heap preamble) call `axiomNamespace`, which is a `def` delegating to `Verifier.freshNamespace` and therefore increments a global counter. `Identifier` identity is `(name, namespace)`, so dropping these calls would renumber every later namespace and rename identifiers across the generated Boogie. - `hypName` consumes a name from the shared `BoogieNameGenerator`. - `defineLHS` registers the wand's lhs label state in the state repository.
| override def preamble = { | ||
| val obj = LocalVarDecl(Identifier("o")(axiomNamespace), refType) | ||
| val obj2 = LocalVarDecl(Identifier("o2")(axiomNamespace), refType) | ||
| @unused val obj2 = LocalVarDecl(Identifier("o2")(axiomNamespace), refType) |
There was a problem hiding this comment.
why don't we drop this var?
There was a problem hiding this comment.
We can, but not for free — this one is a trap, which is why I kept it rather than deleting it with the other dead bindings in 19f1a9c.
obj2 looks like pure AST construction, but the implicit argument is axiomNamespace, and in this class that is a def, not a val:
def axiomNamespace = verifier.freshNamespace("heap.axiom") // DefaultHeapModule.scala:40CarbonVerifier.freshNamespace increments a global counter (CarbonVerifier.scala:45-48), and Identifier identity is (name, namespace) (boogie.scala:112-131) — the namespace id is what disambiguates same-named identifiers in the output. So evaluating obj2 bumps that counter, and deleting it renumbers every namespace allocated afterwards, which can rename identifiers across the generated Boogie. (Note QuantifiedPermModule.axiomNamespace is a val, so the distinction really is per-site.)
The output would still be semantically equivalent, and I'd expect the suite to pass since the tests key on Viper-level errors rather than Boogie names — but it's a wider blast radius than "delete an unused val" suggests. Happy to drop obj2, field2 and predField and let CI confirm, if you're fine with the renumbering. Just say the word.
Generated by Claude Code
| @unused val field2 = LocalVarDecl(Identifier("f2")(axiomNamespace), NamedType(fieldTypeName, Seq(TypeVar("A2"), TypeVar("B2")))) | ||
| @unused val predField = LocalVarDecl(Identifier("pm_f")(axiomNamespace), |
There was a problem hiding this comment.
why don't we drop this var decl?
There was a problem hiding this comment.
Same reason as obj2 above — predField (and field2 on the line before) also take axiomNamespace, which is a def that bumps the global namespace counter, so deleting them renumbers namespaces downstream. Grouped with that thread; whatever you decide there applies to all three.
Generated by Claude Code
|
|
||
| //inhale left hand side to initialize hypothetical state | ||
| val hypName = names.createUniqueIdentifier("Ops") | ||
| @unused val hypName = names.createUniqueIdentifier("Ops") |
There was a problem hiding this comment.
any reason we do not drop this decl?
There was a problem hiding this comment.
Same class of reason as the DefaultHeapModule ones, and here it's concrete enough to state exactly what would change.
names.createUniqueIdentifier mutates the shared BoogieNameGenerator, and createAndSetState on the very next line calls names.createUniqueIdentifier(usedString) internally (line 507) with usedString = "Ops". So this line pre-consumes the name "Ops", which forces the state created on line 216 to be named Ops1 instead of Ops.
Deleting it is therefore not a no-op: every hypothetical-state variable in the generated Boogie gets renamed. Semantically equivalent, textually different.
Whether that's worth keeping is your call — if it's incidental rather than deliberate, I'm happy to drop it and let CI confirm nothing depends on the naming.
Generated by Claude Code
| */ | ||
| val lhsID = wandModule.getNewLhsID() // identifier for the lhs of the wand to be referred to later when 'old(lhs)' is used | ||
| val defineLHS = stmtModule.translateStmt(sil.Label("lhs"+lhsID, Nil)(w.pos, w.info)) | ||
| @unused val defineLHS = stmtModule.translateStmt(sil.Label("lhs"+lhsID, Nil)(w.pos, w.info)) |
There was a problem hiding this comment.
is it a bug we do not do anything with the result?
There was a problem hiding this comment.
This is the one I flagged to myself and could not settle — I'd value your judgement.
Why it looks like a bug. There are three sites that translate an lhs label, and this is the only one that throws the result away:
| site | result |
|---|---|
DefaultWandModule:223 (package) |
used |
DefaultExpModule:493 (checkDefinednessWand) |
used, in the NondetIf |
DefaultWandModule:711 (applyWand) |
discarded |
The discarded value is not nothing: translateStmt(sil.Label(...)) returns Label(...) ++ stateModule.initToCurrentStmt(labelState) ++ ..., and initToCurrentStmt is precisely the assignments that copy the current state into the label's state variables. Only the side effect survives — the snapshot gets registered in the state repository via LabelHelper.getLabelState, but its variables are never assigned. That would make old[lhs](…) in an applied wand's RHS read uninitialised Boogie variables.
Why I don't think that's what's happening. wands/new_syntax/Old.vpr is not Carbon-ignored, and test3 is exactly this scenario:
package acc(x.f) --* acc(x.f) && x.f == old[lhs](x.f)
x.f := 0
apply acc(x.f) --* acc(x.f) && x.f == old[lhs](x.f)
// ensures x.f == 0
If the label state were arbitrary, x.f == old[lhs](x.f) would leave x.f unconstrained and the postcondition couldn't be proved — so that test would be failing, and as far as I know it isn't. Something must initialise it by a path I didn't find, or the value genuinely is redundant here.
I couldn't resolve it by reading alone and can't run the suite locally (no Boogie/Z3 in my environment), so I left it as-is rather than "fixing" something that isn't broken. If you know which path covers it, I'm happy to either drop the binding or wire the result into ret.
Generated by Claude Code
| * Can a location on a given receiver be read? | ||
| */ | ||
| private def hasDirectPerm(mask: Exp, obj: Exp, loc: Exp): Exp = | ||
| private def hasDirectPerm(@unused mask: Exp, obj: Exp, loc: Exp): Exp = |
There was a problem hiding this comment.
why don't we drop the first param?
There was a problem hiding this comment.
Good catch — dropping it would have cemented a latent bug, so I've made the function honour it instead (01df198).
The two call sites currently agree only by accident. hasDirectPerm(obj, loc) passes maskExp, so it was already consistent. But staticPermissionPositive (line 1521) passes staticMask(0).l, which is LocalVar(Identifier("Mask")), whereas maskExp yields GlobalVar(Identifier("Mask")). PrettyPrinter.scala:408-409 renders both as plain Mask, and the only caller is DefaultHeapModule.preamble, which runs while mask == originalMask — so the emitted Boogie is byte-identical today and this commit changes no output.
It would stop being identical the moment staticPermissionPositive were called with mask reassigned to a temporary/old state, or under usingPureState (where maskExp becomes zeroMask): the axiom would silently reference the wrong mask with nothing to flag it.
Generated by Claude Code
`hasDirectPerm` took a `mask` argument and then ignored it, emitting `maskExp`
instead. The two call sites currently agree only by accident: the one that
passes something different, `staticPermissionPositive`, passes
`LocalVar(Identifier("Mask"))` while `maskExp` yields
`GlobalVar(Identifier("Mask"))`, and the pretty printer renders both as plain
`Mask`. The generated Boogie is therefore unchanged by this commit, but the
function now honours its argument instead of silently substituting the current
mask, which would diverge as soon as it were called with `mask` reassigned to
a temporary state or under `usingPureState`.
`loopToInvs` and `labelLoopInfoMap` are `scala.collection.mutable.Map`s, so the
deprecated `+` they used expanded to clone-and-add, which the previous commit
preserved literally. Both are private, are never passed to or returned from
anything, and are only read through `get`, so nothing can observe the copy:
update them in place instead.
2 participants
Summary
This PR enables Scala compiler fatal warnings (
-Xfatal-warnings) and systematically fixes all resulting compiler warnings across the codebase to ensure code quality and prevent future regressions.Key Changes
Compiler Configuration
-Xfatal-warningsscalac option inbuild.sbtto treat all warnings as compilation errorsUnused Variable/Parameter Annotations
@unusedannotations to 40+ variables and parameters that are intentionally not used:permAddName,permSubName,permDivName)translatedLocal,vsFreshBoogie)Pattern Matching Improvements
_) where the binding is unused:case (x, _) if ...→case (_, _) if ...case fa@sil.Forall(v, cond, expr)→case fa@sil.Forall(_, _, _)case sil.FieldAccess(recv, f)→case sil.FieldAccess(recv, _)Type Annotations
implicit val namespace = ...→implicit val namespace: Namespace = ...heapNamespace,fpNamespace,stateNamespace,namespacein multiple modulesMethod Signature Fixes
def permissionPositiveInternal(permission: Exp, silPerm: Option[sil.Exp] = None, ...)→ removed= Nonedefaultdef transformFuncAppsToLimitedOrTriggerForm(exp: Exp, heightToSkip : Int = -1, triggerForm: Boolean = false)→ removed defaultsdef heapUpdateLoc(..., isPMask: Boolean = false)→ removed defaultdef transferAcc(..., havocHeap: Boolean = true)→ removed defaultReturn Type Annotations
Unitreturn types to methods:override def reset = { }→override def reset(): Unit = { }override def beforeAll()→override def beforeAll(): Unitoverride def afterAll()→override def afterAll(): UnitPattern Matching with Type Ascriptions
@uncheckedannotations to pattern matches that are exhaustive but not recognized as such:val (formals, args) = accPred match { ... }→val (formals, args) = (accPred: @unchecked) match { ... }Variable Mutability Fixes
vartovalwhere variables are assigned once:var containsVars = ...→val containsVars = ...var err = ...→val err = ...var oldW = ...→val oldW = ...Unused Import Removals
DefaultHeapModule: removedInhaleComponent,PartialVerificationErrorCarbonQuantifierWeightTests: removedExists,PrettyPrinter,EnvironmentDefaultMainModule: removedexpModuleimportDefaultExhaleModule: removedpermModuleimportDefaultLoopModule: removedViperStrategyimportExhaleModule: removedDefinednessStateimportHeapModule: removedPolyMapDesugarHelperimportLabelHelper: removedStateModuleimportImplicit Conversion Return Types
https://claude.ai/code/session_01W9SJYwJrGzRj71r7Kg1yvD