From 8835e1003efae2f266243833e79db259280f5f37 Mon Sep 17 00:00:00 2001
From: whitequark <whitequark@whitequark.org>
Date: Sat, 1 Feb 2020 01:55:23 +0000
Subject: [PATCH] hdl.ast: warn on unused property statements (Assert, Assume,
 etc).

A property statement that is created but not added to a module is
virtually always a serious bug, since it can make formal verification
pass when it should not. Therefore, add a warning to it, similar to
UnusedElaboratable.

Doing this to all statements is possible, but many temporary ones are
created internally by nMigen, and the extensive changes required to
remove false positives are likely not worth the true positives.
We can revisit this in the future.

Fixes #303.
---
 nmigen/hdl/ast.py  | 19 +++++++++++++------
 nmigen/hdl/dsl.py  | 12 +++++++-----
 nmigen/hdl/ir.py   |  4 +++-
 nmigen/hdl/xfrm.py |  2 ++
 4 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/nmigen/hdl/ast.py b/nmigen/hdl/ast.py
index d26c3c3..efaeb0f 100644
--- a/nmigen/hdl/ast.py
+++ b/nmigen/hdl/ast.py
@@ -8,6 +8,7 @@ from enum import Enum
 
 from .. import tracer
 from .._utils import *
+from .._unused import *
 
 
 __all__ = [
@@ -17,9 +18,9 @@ __all__ = [
     "Signal", "ClockSignal", "ResetSignal",
     "UserValue",
     "Sample", "Past", "Stable", "Rose", "Fell", "Initial",
-    "Statement", "Assign", "Assert", "Assume", "Cover", "Switch",
-    "ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict",
-    "SignalSet",
+    "Statement", "Switch",
+    "Property", "Assign", "Assert", "Assume", "Cover",
+    "ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict", "SignalSet",
 ]
 
 
@@ -493,13 +494,13 @@ class AnyValue(Value, DUID):
 @final
 class AnyConst(AnyValue):
     def __repr__(self):
-        return "(anyconst {}'{})".format(self.nbits, "s" if self.signed else "")
+        return "(anyconst {}'{})".format(self.width, "s" if self.signed else "")
 
 
 @final
 class AnySeq(AnyValue):
     def __repr__(self):
-        return "(anyseq {}'{})".format(self.nbits, "s" if self.signed else "")
+        return "(anyseq {}'{})".format(self.width, "s" if self.signed else "")
 
 
 @final
@@ -1221,7 +1222,13 @@ class Assign(Statement):
         return "(eq {!r} {!r})".format(self.lhs, self.rhs)
 
 
-class Property(Statement):
+class UnusedProperty(UnusedMustUse):
+    pass
+
+
+class Property(Statement, MustUse):
+    _MustUse__warning = UnusedProperty
+
     def __init__(self, test, *, _check=None, _en=None, src_loc_at=0):
         super().__init__(src_loc_at=src_loc_at)
         self.test   = Value.cast(test)
diff --git a/nmigen/hdl/dsl.py b/nmigen/hdl/dsl.py
index b8f7692..986ecc0 100644
--- a/nmigen/hdl/dsl.py
+++ b/nmigen/hdl/dsl.py
@@ -462,14 +462,16 @@ class Module(_ModuleBuilderRoot, Elaboratable):
         while len(self._ctrl_stack) > self.domain._depth:
             self._pop_ctrl()
 
-        for assign in Statement.cast(assigns):
-            if not compat_mode and not isinstance(assign, (Assign, Assert, Assume, Cover)):
+        for stmt in Statement.cast(assigns):
+            if not compat_mode and not isinstance(stmt, (Assign, Assert, Assume, Cover)):
                 raise SyntaxError(
                     "Only assignments and property checks may be appended to d.{}"
                     .format(domain_name(domain)))
 
-            assign = SampleDomainInjector(domain)(assign)
-            for signal in assign._lhs_signals():
+            stmt._MustUse__used = True
+            stmt = SampleDomainInjector(domain)(stmt)
+
+            for signal in stmt._lhs_signals():
                 if signal not in self._driving:
                     self._driving[signal] = domain
                 elif self._driving[signal] != domain:
@@ -479,7 +481,7 @@ class Module(_ModuleBuilderRoot, Elaboratable):
                         "already driven from d.{}"
                         .format(signal, domain_name(domain), domain_name(cd_curr)))
 
-            self._statements.append(assign)
+            self._statements.append(stmt)
 
     def _add_submodule(self, submodule, name=None):
         if not hasattr(submodule, "elaborate"):
diff --git a/nmigen/hdl/ir.py b/nmigen/hdl/ir.py
index 5d4a1c5..cea9b40 100644
--- a/nmigen/hdl/ir.py
+++ b/nmigen/hdl/ir.py
@@ -121,7 +121,9 @@ class Fragment:
         yield from self.domains
 
     def add_statements(self, *stmts):
-        self.statements += Statement.cast(stmts)
+        for stmt in Statement.cast(stmts):
+            stmt._MustUse__used = True
+            self.statements.append(stmt)
 
     def add_subfragment(self, subfragment, name=None):
         assert isinstance(subfragment, Fragment)
diff --git a/nmigen/hdl/xfrm.py b/nmigen/hdl/xfrm.py
index 75f85ba..fb4dad9 100644
--- a/nmigen/hdl/xfrm.py
+++ b/nmigen/hdl/xfrm.py
@@ -234,6 +234,8 @@ class StatementVisitor(metaclass=ABCMeta):
             new_stmt.src_loc = stmt.src_loc
             if isinstance(new_stmt, Switch) and isinstance(stmt, Switch):
                 new_stmt.case_src_locs = stmt.case_src_locs
+        if isinstance(new_stmt, Property):
+            new_stmt._MustUse__used = True
         return new_stmt
 
     def __call__(self, stmt):
-- 
2.30.2