Corrected test for whether a program loses const-correctness

Previously the check for loss of const-correctness was to look at each
assignment and check whether in either the left/right hand sides of the
assignment or somewhere in the right hand side expression tree the
following condition was met:

Any type or any of its subtypes lost const-ness

This condition is now replaced by a more subtle condition:

if they are both pointers then:
there subtypes should not directly lose const-ness
if the subtype is a pointer, we recursively apply this check on the
subtypes
if they are not pointers:
we don't care about const-qualification loss at this level since it is
a copy

This fixes diffblue/cbmc-toyota#127 where an `const int` being assigned
to an
`int` would trigger disabling the function pointer removal.

Pulled out the private access class into a util file

Updating

New implementation of  is_type_at_least_as_const_as only checks one
depth so we
don't need to pass in naked pointers. Updated the comment to reflect
methods new
purpose. Added unit tests to document exactly what the method is testing

Added tests to demonstrate the does_type_preserve_const_correctness

This is useful documentation of how it is different to the
is_type_at_least_as_const_as.

Added more examples of spurious const loss

Author: thk123

regression/goto-analyzer/precise-const-fp-supurious-const-loss/main.c

@@ -23,6 +23,13 @@ void func()
   // Here we 'lose' const-ness except it is a copy so we shouldn't care
   int non_const_number=const_number;
   const void_fp fp = f2;
+
+
+  // Here also we lose const-ness except it is a copy of pointer so we
+  // shouldn't care
+  const void_fp * const p2fp = &f2;
+  const void_fp * p2fp_non_const = &p2fp;
+
   fp();
 }
 

regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$

src/analyses/does_remove_const.cpp

@@ -47,7 +47,7 @@ bool does_remove_constt::operator()() const
 
     // Compare the types recursively for a point where the rhs is more
     // const that the lhs
-    if(!is_type_at_least_as_const_as(&lhs_type, &rhs_type))
+    if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
     {
       return true;
     }
@@ -78,7 +78,7 @@ bool does_remove_constt::does_expr_lose_const(const exprt &expr) const
     if(base_type_eq(op_type, root_type, ns))
     {
       // Is this child more const-qualified than the root
-      if(!is_type_at_least_as_const_as(&root_type, &op_type))
+      if(!does_type_preserve_const_correctness(&root_type, &op_type))
       {
         return true;
       }
@@ -93,37 +93,78 @@ bool does_remove_constt::does_expr_lose_const(const exprt &expr) const
   return false;
 }
 
-/// A recursive check to check the type_more_const is at least as const as type
-/// compare.
+/// A recursive check that handles when assigning a source value to a target, is
+/// the assignment a loss of const-correctness.
 ///
-///          type_more_const | type_compare || result
-///          ----------------------------------------
-///          const int *     | const int *  -> true
-///          int *           | const int *  -> false
-///          const int *     | int *        -> true
-///          int *           | int * const  -> false
+/// For primitive types, it always returns true since these are copied
+///
+/// For pointers we requires that if in the source it's value couldn't
+/// be modified, then it still can't be modified in the target
+///
+/// target_type     | source_type  || result
+/// ----------------------------------------
+/// const int       | int          -> true
+/// int             | const int    -> true
+/// const int       | const int    -> true
+/// int             | int          -> true
+///
+/// int *           | int * const  -> true
+/// int *           | const int *  -> false
+/// const int *     | int *        -> true
+/// const int *     | const int *  -> true
+/// int * const     | int *        -> true
+///
+/// See unit/analyses/does_type_preserve_const_correcness for
+/// comprehensive list
+/// \param target_type: the resulting type
+/// \param source_type: the starting type
+/// \return Returns true if a value of type source_type could be assigned into a
+///   a value of target_type without losing const-correctness
+bool does_remove_constt::does_type_preserve_const_correctness(
+  const typet *target_type, const typet *source_type) const
+{
+  while(target_type->id()==ID_pointer)
+  {
+    bool direct_subtypes_at_least_as_const=
+      is_type_at_least_as_const_as(
+        target_type->subtype(), source_type->subtype());
+    // We have a pointer to something, but the thing it is pointing to can't be
+    // modified normally, but can through this pointer
+    if(!direct_subtypes_at_least_as_const)
+      return false;
+    // Check the subtypes if they are pointers
+    target_type=&target_type->subtype();
+    source_type=&source_type->subtype();
+  }
+  return true;
+}
+
+/// A simple check to check the type_more_const is at least as const as type
+/// compare. This only checks the exact type, use
+/// `is_pointer_at_least_as_constant_as` for dealing with nested types
+///
+/// type_more_const | type_compare || result
+/// ----------------------------------------
+/// const int       | int          -> true
+/// int             | const int    -> false
+/// const int       | const int    -> true
+/// int             | int          -> true
+/// int *           | int * const  -> false
+/// int *           | const int *  -> true
+/// const int *     | int *        -> true
+/// int * const     | int *        -> true
+///
+/// See unit/analyses/is_type_as_least_as_const_as for comprehensive list
 /// \param type_more_const: the type we are expecting to be at least as const
 ///   qualified
 /// \param type_compare: the type we are comparing against which may be less
 ///   const qualified
 /// \return Returns true if type_more_const is at least as const as type_compare
 bool does_remove_constt::is_type_at_least_as_const_as(
-  const typet *type_more_const, const typet *type_compare) const
+  const typet &type_more_const, const typet &type_compare) const
 {
-  while(type_compare->id()!=ID_nil && type_more_const->id()!=ID_nil)
-  {
-    const c_qualifierst rhs_qualifiers(*type_compare);
-    const c_qualifierst lhs_qualifiers(*type_more_const);
-    if(rhs_qualifiers.is_constant && !lhs_qualifiers.is_constant)
-    {
-      return false;
-    }
-
-    type_compare=&type_compare->subtype();
-    type_more_const=&type_more_const->subtype();
-  }
-
-  // Both the types should have the same number of subtypes
-  assert(type_compare->id()==ID_nil && type_more_const->id()==ID_nil);
-  return true;
+  const c_qualifierst type_compare_qualifiers(type_compare);
+  const c_qualifierst more_constant_qualifiers(type_more_const);
+  return !type_compare_qualifiers.is_constant ||
+    more_constant_qualifiers.is_constant;
 }

src/analyses/does_remove_const.h

@@ -26,7 +26,10 @@ class does_remove_constt
   bool does_expr_lose_const(const exprt &expr) const;
 
   bool is_type_at_least_as_const_as(
-    const typet *type_more_const, const typet *type_compare) const;
+    const typet &type_more_const, const typet &type_compare) const;
+
+  bool does_type_preserve_const_correctness(
+    const typet *target_type, const typet *source_type) const;
 
   const goto_programt &goto_program;
   const namespacet &ns;

unit/Makefile

@@ -2,6 +2,8 @@
 
 SRC = unit_tests.cpp \
       analyses/does_remove_const/does_expr_lose_const.cpp \
+      analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
+      analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
       catch_example.cpp \
       # Empty last line
 

unit/analyses/does_remove_const/does_expr_lose_const.cpp

@@ -16,24 +16,8 @@
 #include <util/std_types.h>
 #include <ansi-c/c_qualifiers.h>
 #include <goto-programs/goto_program.h>
+#include <analyses/does_remove_const/does_remove_const_util.h>
 
-// This class provides access to private members and functions of
-// does_remove_const
-class does_remove_const_testt
-{
-public:
-  does_remove_const_testt(does_remove_constt does_remove_const):
-    does_remove_const(does_remove_const)
-  {}
-  bool does_expr_lose_const(const exprt &expr) const
-  {
-    return does_remove_const.does_expr_lose_const(expr);
-  }
-
-private:
-  does_remove_constt does_remove_const;
-
-};
 
 SCENARIO("does_expr_lose_const",
   "[core][analyses][does_remove_const][does_expr_remove_const]")
@@ -78,14 +62,10 @@ SCENARIO("does_expr_lose_const",
     typet const_pointer_to_const_int_type=pointer_typet(const_primitive_type);
     const_qualifier.write(const_pointer_to_const_int_type);
 
-    // const int const_primitive;
     symbol_exprt const_primitive_symbol(
       "const_primitive", const_primitive_type);
-
-    // int non_const_primitive;
     symbol_exprt non_const_primitive_symbol(
       "non_const_primitive", non_const_primitive_type);
-
     symbol_exprt pointer_to_int_symbol(
       "pointer_to_int", pointer_to_int_type);
     symbol_exprt const_pointer_to_int_symbol(

unit/analyses/does_remove_const/does_remove_const_util.h

@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+ Module: Does Remove Const Unit Tests
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Does Remove Const Unit Tests
+
+#ifndef CPROVER__ANALYSES_DOES_REMOVE_CONST_DOES_REMOVE_CONST_UTIL_H
+#define CPROVER__ANALYSES_DOES_REMOVE_CONST_DOES_REMOVE_CONST_UTIL_H
+
+#include <analyses/does_remove_const.h>
+
+// This class provides access to private members and functions of
+// does_remove_const
+class does_remove_const_testt
+{
+public:
+  explicit does_remove_const_testt(does_remove_constt does_remove_const):
+    does_remove_const(does_remove_const)
+  {}
+
+  bool does_expr_lose_const(const exprt &expr) const
+  {
+    return does_remove_const.does_expr_lose_const(expr);
+  }
+
+  bool is_type_at_least_as_const_as(
+    const typet &type_more_const, const typet &type_compare) const
+  {
+    return does_remove_const.is_type_at_least_as_const_as(
+      type_more_const, type_compare);
+  }
+
+  bool does_type_preserve_const_correctness(
+    const typet *target_type, const typet *source_type) const
+  {
+    return does_remove_const.does_type_preserve_const_correctness(
+      target_type, source_type);
+  }
+
+private:
+  does_remove_constt does_remove_const;
+};
+
+#endif // CPROVER__ANALYSES_DOES_REMOVE_CONST_DOES_REMOVE_CONST_UTIL_H