From bf439bd711ab4fad46489bfa5ee3fbeee8bf67d1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 17 Nov 2021 16:24:50 +0000
Subject: [PATCH 1/2] C front-end: Use is_constantt to recognise further
 compile-time constants

Arrays and structs (and any nesting thereof) could also be compile-time
constants.
---
 src/ansi-c/c_typecheck_expr.cpp | 38 +++++++++++++++++++++++++++++----
 src/util/expr_util.cpp          |  1 +
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index fb597a90f72..455b83ccc49 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3925,6 +3925,38 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
   throw 0;
 }
 
+class is_compile_time_constantt : public is_constantt
+{
+public:
+  explicit is_compile_time_constantt(const namespacet &ns) : ns(ns)
+  {
+  }
+
+protected:
+  const namespacet &ns;
+
+  bool is_constant(const exprt &e) const override
+  {
+    if(e.id() == ID_infinity)
+      return true;
+    else
+      return is_constantt::is_constant(e);
+  }
+
+  bool is_constant_address_of(const exprt &e) const override
+  {
+    if(e.id() == ID_symbol)
+    {
+      return e.type().id() == ID_code ||
+             ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
+    }
+    else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
+      return true;
+    else
+      return is_constantt::is_constant_address_of(e);
+  }
+};
+
 void c_typecheck_baset::make_constant(exprt &expr)
 {
   // Floating-point expressions may require a rounding mode.
@@ -3936,8 +3968,7 @@ void c_typecheck_baset::make_constant(exprt &expr)
 
   simplify(expr, *this);
 
-  if(!expr.is_constant() &&
-     expr.id()!=ID_infinity)
+  if(!is_compile_time_constantt(*this)(expr))
   {
     error().source_location=expr.find_source_location();
     error() << "expected constant expression, but got '" << to_string(expr)
@@ -3952,8 +3983,7 @@ void c_typecheck_baset::make_constant_index(exprt &expr)
   make_index_type(expr);
   simplify(expr, *this);
 
-  if(!expr.is_constant() &&
-     expr.id()!=ID_infinity)
+  if(!is_compile_time_constantt(*this)(expr))
   {
     error().source_location=expr.find_source_location();
     error() << "conversion to integer constant failed" << eom;
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index d88065fa280..2e3e4a58939 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -236,6 +236,7 @@ bool is_constantt::is_constant(const exprt &expr) const
     expr.id() == ID_typecast || expr.id() == ID_array_of ||
     expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
     expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
+    expr.id() == ID_empty_union ||
     // byte_update works, byte_extract may be out-of-bounds
     expr.id() == ID_byte_update_big_endian ||
     expr.id() == ID_byte_update_little_endian)

From 1a86739a3e123e420f0336fd5824c08c75a4e5c3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 17 Nov 2021 13:49:29 +0000
Subject: [PATCH 2/2] Static-lifetime symbols require compile-time constant
 initialisers

We previously silently accepted initialisers that weren't compile-time
constants, resulting in surprising behaviour: the assertion in the
enclosed regression test would fail, because x ended up being
initialised before y.
---
 regression/ansi-c/static4/main.c    |  7 +++++++
 regression/ansi-c/static4/test.desc |  9 +++++++++
 src/ansi-c/c_typecheck_code.cpp     | 13 ++++++++++---
 3 files changed, 26 insertions(+), 3 deletions(-)
 create mode 100644 regression/ansi-c/static4/main.c
 create mode 100644 regression/ansi-c/static4/test.desc

diff --git a/regression/ansi-c/static4/main.c b/regression/ansi-c/static4/main.c
new file mode 100644
index 00000000000..450d99c2803
--- /dev/null
+++ b/regression/ansi-c/static4/main.c
@@ -0,0 +1,7 @@
+int main()
+{
+  int y = 42;
+  static int x = y;
+
+  __CPROVER_assert(x == 42, "local static");
+}
diff --git a/regression/ansi-c/static4/test.desc b/regression/ansi-c/static4/test.desc
new file mode 100644
index 00000000000..146bde3172a
--- /dev/null
+++ b/regression/ansi-c/static4/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+expected constant expression
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 7e46443a18f..6fd492371ce 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -308,12 +308,19 @@ void c_typecheck_baset::typecheck_decl(codet &code)
     // see if it's a typedef
     // or a function
     // or static
-    if(symbol.is_type ||
-       symbol.type.id()==ID_code ||
-       symbol.is_static_lifetime)
+    if(symbol.is_type || symbol.type.id() == ID_code)
     {
       // we ignore
     }
+    else if(symbol.is_static_lifetime)
+    {
+      // make sure the initialization value is a compile-time constant
+      if(symbol.value.is_not_nil())
+      {
+        exprt init_value = symbol.value;
+        make_constant(init_value);
+      }
+    }
     else
     {
       code_frontend_declt decl(symbol.symbol_expr());