[CONTRACTS] Add loop-contract symbols into symbol table during typecheck

src/linking/remove_internal_symbols.cpp

@@ -43,8 +43,12 @@
 
     find_symbols_sett new_symbols;
 
-    find_type_and_expr_symbols(symbol.type, new_symbols);
-    find_type_and_expr_symbols(symbol.value, new_symbols);
+    // ID of named subs of loop contracts
+    std::vector<irep_idt> loop_contracts_subs{
+      ID_C_spec_loop_invariant, ID_C_spec_decreases};
+
+    find_type_and_expr_symbols(symbol.type, new_symbols, loop_contracts_subs);
+    find_type_and_expr_symbols(symbol.value, new_symbols, loop_contracts_subs);
 
     for(const auto &s : new_symbols)
       working_set.push_back(&ns.lookup(s));

src/util/find_symbols.cpp

@@ -27,17 +27,22 @@
   F_ALL
 };
 
+/// Find identifiers with id ID_symbol of the sub expressions and the subs with
+/// ID in \p subs_to_find
+/// considering both free and bound variables, as well as any type tags.
 static bool find_symbols(
   symbol_kindt,
   const typet &,
   std::function<bool(const symbol_exprt &)>,
-  std::unordered_set<irep_idt> &bindings);
+  std::unordered_set<irep_idt> &bindings,
+  const std::vector<irep_idt> &subs_to_find);
 
 static bool find_symbols(
   symbol_kindt kind,
   const exprt &src,
   std::function<bool(const symbol_exprt &)> op,
-  std::unordered_set<irep_idt> &bindings)
+  std::unordered_set<irep_idt> &bindings,
+  const std::vector<irep_idt> &subs_to_find)
 {
   if(kind == symbol_kindt::F_EXPR_FREE)
   {
@@ -48,10 +53,12 @@
       for(const auto &v : binding_expr.variables())
         new_bindings.insert(v.get_identifier());
 
-      if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
+      if(!find_symbols(
+           kind, binding_expr.where(), op, new_bindings, subs_to_find))
         return false;
 
-      return find_symbols(kind, binding_expr.type(), op, bindings);
+      return find_symbols(
+        kind, binding_expr.type(), op, bindings, subs_to_find);
     }
     else if(src.id() == ID_let)
     {
@@ -60,23 +67,38 @@
       for(const auto &v : let_expr.variables())
         new_bindings.insert(v.get_identifier());
 
-      if(!find_symbols(kind, let_expr.where(), op, new_bindings))
+      if(!find_symbols(kind, let_expr.where(), op, new_bindings, subs_to_find))
         return false;
 
-      if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
+      if(!find_symbols(kind, let_expr.op1(), op, new_bindings, subs_to_find))
         return false;
 
-      return find_symbols(kind, let_expr.type(), op, bindings);
+      return find_symbols(kind, let_expr.type(), op, bindings, subs_to_find);
     }
   }
 
   for(const auto &src_op : src.operands())
   {
-    if(!find_symbols(kind, src_op, op, bindings))
+    if(!find_symbols(kind, src_op, op, bindings, subs_to_find))
       return false;
   }
 
-  if(!find_symbols(kind, src.type(), op, bindings))
+  // Go over all named subs with id in subs_to_find
+  // and find symbols recursively.
+  for(const auto &sub_to_find : subs_to_find)
+  {
+    auto sub_expr = static_cast<const exprt &>(src.find(sub_to_find));
+    if(sub_expr.is_not_nil())
+    {
+      for(const auto &sub_op : sub_expr.operands())
+      {
+        if(!find_symbols(kind, sub_op, op, bindings, subs_to_find))
+          return false;
+      }
+    }
+  }
+
+  if(!find_symbols(kind, src.type(), op, bindings, subs_to_find))
     return false;
 
   if(src.id() == ID_symbol)
@@ -95,46 +117,58 @@
     }
   }
 
-  const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
+  const irept &c_sizeof_type = src.find(ID_C_c_sizeof_type);
 
   if(
-    c_sizeof_type.is_not_nil() &&
-    !find_symbols(
-      kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
+    c_sizeof_type.is_not_nil() && !find_symbols(
+                                    kind,
+                                    static_cast<const typet &>(c_sizeof_type),
+                                    op,
+                                    bindings,
+                                    subs_to_find))
   {
     return false;
   }
 
   const irept &va_arg_type=src.find(ID_C_va_arg_type);
 
   if(
-    va_arg_type.is_not_nil() &&
-    !find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
+    va_arg_type.is_not_nil() && !find_symbols(
+                                  kind,
+                                  static_cast<const typet &>(va_arg_type),
+                                  op,
+                                  bindings,
+                                  subs_to_find))
   {
     return false;
   }
 
   return true;
 }
 
+/// Find identifiers with id ID_symbol of the sub expressions and the subs with
+/// ID in \p subs_to_find
+/// considering both free and bound variables, as well as any type tags.
 static bool find_symbols(
   symbol_kindt kind,
   const typet &src,
   std::function<bool(const symbol_exprt &)> op,
-  std::unordered_set<irep_idt> &bindings)
+  std::unordered_set<irep_idt> &bindings,
+  const std::vector<irep_idt> &subs_to_find)
 {
   if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
   {
     if(
       src.has_subtype() &&
-      !find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
+      !find_symbols(
+        kind, to_type_with_subtype(src).subtype(), op, bindings, subs_to_find))
     {
       return false;
     }
 
     for(const typet &subtype : to_type_with_subtypes(src).subtypes())
     {
-      if(!find_symbols(kind, subtype, op, bindings))
+      if(!find_symbols(kind, subtype, op, bindings, subs_to_find))
         return false;
     }
 
@@ -155,26 +189,27 @@
 
     for(const auto &c : struct_union_type.components())
     {
-      if(!find_symbols(kind, c, op, bindings))
+      if(!find_symbols(kind, c, op, bindings, subs_to_find))
         return false;
     }
   }
   else if(src.id()==ID_code)
   {
     const code_typet &code_type=to_code_type(src);
-    if(!find_symbols(kind, code_type.return_type(), op, bindings))
+    if(!find_symbols(kind, code_type.return_type(), op, bindings, subs_to_find))
       return false;
 
     for(const auto &p : code_type.parameters())
     {
-      if(!find_symbols(kind, p, op, bindings))
+      if(!find_symbols(kind, p, op, bindings, subs_to_find))
         return false;
     }
   }
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
-    if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
+    if(!find_symbols(
+         kind, to_array_type(src).size(), op, bindings, subs_to_find))
       return false;
   }
   else if(
@@ -204,19 +239,21 @@
 static bool find_symbols(
   symbol_kindt kind,
   const typet &type,
-  std::function<bool(const symbol_exprt &)> op)
+  std::function<bool(const symbol_exprt &)> op,
+  const std::vector<irep_idt> &subs_to_find = {})
 {
   std::unordered_set<irep_idt> bindings;
-  return find_symbols(kind, type, op, bindings);
+  return find_symbols(kind, type, op, bindings, subs_to_find);
 }
 
 static bool find_symbols(
   symbol_kindt kind,
   const exprt &src,
-  std::function<bool(const symbol_exprt &)> op)
+  std::function<bool(const symbol_exprt &)> op,
+  const std::vector<irep_idt> &subs_to_find = {})
 {
   std::unordered_set<irep_idt> bindings;
-  return find_symbols(kind, src, op, bindings);
+  return find_symbols(kind, src, op, bindings, subs_to_find);
 }
 
 void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
@@ -278,20 +315,34 @@
     });
 }
 
-void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
+void find_type_and_expr_symbols(
+  const exprt &src,
+  find_symbols_sett &dest,
+  const std::vector<irep_idt> &subs_to_find)
 {
-  find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
-    dest.insert(e.get_identifier());
-    return true;
-  });
+  find_symbols(
+    symbol_kindt::F_ALL,
+    src,
+    [&dest](const symbol_exprt &e) {
+      dest.insert(e.get_identifier());
+      return true;
+    },
+    subs_to_find);
 }
 
-void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
+void find_type_and_expr_symbols(
+  const typet &src,
+  find_symbols_sett &dest,
+  const std::vector<irep_idt> &subs_to_find)
 {
-  find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
-    dest.insert(e.get_identifier());
-    return true;
-  });
+  find_symbols(
+    symbol_kindt::F_ALL,
+    src,
+    [&dest](const symbol_exprt &e) {
+      dest.insert(e.get_identifier());
+      return true;
+    },
+    subs_to_find);
 }
 
 void find_symbols(const exprt &src, find_symbols_sett &dest)

src/util/find_symbols.h

@@ -79,16 +79,20 @@ void find_non_pointer_type_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
-/// Find identifiers of the sub expressions with id ID_symbol, considering both
-/// free and bound variables, as well as any type tags.
+/// Find identifiers with id ID_symbol of the sub expressions and the subs with
+/// ID in \p subs_to_find
+/// considering both free and bound variables, as well as any type tags.
 void find_type_and_expr_symbols(
   const typet &src,
-  find_symbols_sett &dest);
+  find_symbols_sett &dest,
+  const std::vector<irep_idt> &subs_to_find = {});
 
-/// Find identifiers of the sub expressions with id ID_symbol, considering both
-/// free and bound variables, as well as any type tags.
+/// Find identifiers with id ID_symbol of the sub expressions and the subs with
+/// ID in \p subs_to_find
+/// considering both free and bound variables, as well as any type tags.
 void find_type_and_expr_symbols(
   const exprt &src,
-  find_symbols_sett &dest);
+  find_symbols_sett &dest,
+  const std::vector<irep_idt> &subs_to_find = {});
 
 #endif // CPROVER_UTIL_FIND_SYMBOLS_H