Merge pull request #1007 from thk123/bugfix/irrelevant-const-removal

Fix irrelevant loss of const throwing off the const analysis

Author: kroening

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

@@ -0,0 +1,41 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+const int const_number=4;
+
+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();
+}
+
+int main()
+{
+  func();
+
+  return 0;
+}

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

@@ -0,0 +1,18 @@
+CORE
+main.c
+--show-goto-functions --verbosity 10 --pointer-check
+^Removing function pointers and virtual functions$
+^\s*f2\(\);
+--
+^warning: ignoring
+^\s*\d+:\s*f1\(\);
+^\s*\d+:\s*f3\(\);
+^\s*\d+:\s*f4\(\);
+^\s*\d+:\s*f5\(\);
+^\s*\d+:\s*f6\(\);
+^\s*\d+:\s*f7\(\);
+^\s*\d+:\s*f8\(\);
+^\s*\d+:\s*f9\(\);
+--
+Though this example program appears to lose const-ness, since it is a primitive
+it is a copy so it is irrelevant.

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

@@ -12,6 +12,7 @@
 #define CPROVER_ANALYSES_DOES_REMOVE_CONST_H
 
 #include <util/type.h>
+#include <util/namespace.h>
 
 class goto_programt;
 class namespacet;
@@ -27,10 +28,15 @@ 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;
+
+  friend class does_remove_const_testt;
 };
 
 #endif // CPROVER_ANALYSES_DOES_REMOVE_CONST_H

unit/Makefile

@@ -1,6 +1,9 @@
 .PHONY: all cprover.dir test
 
 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