CONTRACTS: pointer predicates now use dfcc_cfg_infot

Remi Delmas · Remi Delmas · commit 9e14d8a35017 · 2023-05-10T20:37:34.000Z
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp
@@ -12,6 +12,7 @@ Date: August 2022
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
+#include "dfcc_cfg_info.h"
 #include "dfcc_library.h"
 
 dfcc_is_freeablet::dfcc_is_freeablet(
@@ -23,20 +24,20 @@ dfcc_is_freeablet::dfcc_is_freeablet(
 
 void dfcc_is_freeablet::rewrite_calls(
   goto_programt &program,
-  const exprt &write_set)
+  dfcc_cfg_infot &cfg_info)
 {
   rewrite_calls(
     program,
     program.instructions.begin(),
     program.instructions.end(),
-    write_set);
+    cfg_info);
 }
 
 void dfcc_is_freeablet::rewrite_calls(
   goto_programt &program,
   goto_programt::targett first_instruction,
   const goto_programt::targett &last_instruction,
-  const exprt &write_set)
+  dfcc_cfg_infot &cfg_info)
 {
   auto target = first_instruction;
   while(target != last_instruction)
@@ -54,15 +55,15 @@ void dfcc_is_freeablet::rewrite_calls(
           // redirect call to library implementation
           to_symbol_expr(target->call_function())
             .set_identifier(library.get_dfcc_fun_name(dfcc_funt::IS_FREEABLE));
-          target->call_arguments().push_back(write_set);
+          target->call_arguments().push_back(cfg_info.get_write_set(target));
         }
         else if(fun_name == CPROVER_PREFIX "was_freed")
         {
           // insert call to precondition for vacuity checking
           auto inst = goto_programt::make_function_call(
             library.check_replace_ensures_was_freed_preconditions_call(
               target->call_arguments().at(0),
-              write_set,
+              cfg_info.get_write_set(target),
               target->source_location()),
             target->source_location());
           program.insert_before_swap(target, inst);
@@ -71,7 +72,7 @@ void dfcc_is_freeablet::rewrite_calls(
           // redirect call to library implementation
           to_symbol_expr(target->call_function())
             .set_identifier(library.get_dfcc_fun_name(dfcc_funt::WAS_FREED));
-          target->call_arguments().push_back(write_set);
+          target->call_arguments().push_back(cfg_info.get_write_set(target));
         }
       }
     }
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.h
@@ -21,6 +21,7 @@ Date: August 2022
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
+class dfcc_cfg_infot;
 class exprt;
 
 /// Rewrites calls to is_freeable and was_freed predicates in goto programs
@@ -35,7 +36,7 @@ class dfcc_is_freeablet
   /// Rewrites calls to is_freeable and was_freed predicates into calls
   /// to the library implementation in the given program, passing the
   /// given write_set expression as parameter to the library function.
-  void rewrite_calls(goto_programt &program, const exprt &write_set);
+  void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info);
 
   /// Rewrites calls to is_fresh predicates into calls
   /// to the library implementation in the given program between
@@ -45,7 +46,7 @@ class dfcc_is_freeablet
     goto_programt &program,
     goto_programt::targett first_instruction,
     const goto_programt::targett &last_instruction, // excluding the last
-    const exprt &write_set);
+    dfcc_cfg_infot &cfg_info);
 
 protected:
   dfcc_libraryt &library;
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp
@@ -13,6 +13,7 @@ Date: August 2022
 #include <util/pointer_expr.h>
 #include <util/symbol.h>
 
+#include "dfcc_cfg_info.h"
 #include "dfcc_library.h"
 
 dfcc_is_fresht::dfcc_is_fresht(
@@ -24,20 +25,20 @@ dfcc_is_fresht::dfcc_is_fresht(
 
 void dfcc_is_fresht::rewrite_calls(
   goto_programt &program,
-  const exprt &write_set)
+  dfcc_cfg_infot &cfg_info)
 {
   rewrite_calls(
     program,
     program.instructions.begin(),
     program.instructions.end(),
-    write_set);
+    cfg_info);
 }
 
 void dfcc_is_fresht::rewrite_calls(
   goto_programt &program,
   goto_programt::targett first_instruction,
   const goto_programt::targett &last_instruction,
-  const exprt &write_set)
+  dfcc_cfg_infot &cfg_info)
 {
   auto &target = first_instruction;
   while(target != last_instruction)
@@ -61,7 +62,7 @@ void dfcc_is_fresht::rewrite_calls(
             .set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name);
 
           // pass the write_set
-          target->call_arguments().push_back(write_set);
+          target->call_arguments().push_back(cfg_info.get_write_set(target));
         }
       }
     }
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.h
@@ -21,6 +21,7 @@ Date: August 2022
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
+class dfcc_cfg_infot;
 class exprt;
 
 /// Rewrites calls to is_fresh predicates into calls
@@ -35,7 +36,7 @@ class dfcc_is_fresht
   /// Rewrites calls to is_fresh predicates into calls
   /// to the library implementation in the given program, passing the
   /// given write_set expression as parameter to the library function.
-  void rewrite_calls(goto_programt &program, const exprt &write_set);
+  void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info);
 
   /// Rewrites calls to is_fresh predicates into calls
   /// to the library implementation in the given program between
@@ -45,7 +46,7 @@ class dfcc_is_fresht
     goto_programt &program,
     goto_programt::targett first_instruction,
     const goto_programt::targett &last_instruction,
-    const exprt &write_set);
+    dfcc_cfg_infot &cfg_info);
 
 protected:
   dfcc_libraryt &library;
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp
@@ -16,6 +16,7 @@ Date: August 2022
 
 #include <langapi/language_util.h>
 
+#include "dfcc_cfg_info.h"
 #include "dfcc_library.h"
 
 dfcc_obeys_contractt::dfcc_obeys_contractt(
@@ -27,14 +28,14 @@ dfcc_obeys_contractt::dfcc_obeys_contractt(
 
 void dfcc_obeys_contractt::rewrite_calls(
   goto_programt &program,
-  const exprt &write_set,
+  dfcc_cfg_infot &cfg_info,
   std::set<irep_idt> &function_pointer_contracts)
 {
   rewrite_calls(
     program,
     program.instructions.begin(),
     program.instructions.end(),
-    write_set,
+    cfg_info,
     function_pointer_contracts);
 }
 
@@ -62,7 +63,7 @@ void dfcc_obeys_contractt::rewrite_calls(
   goto_programt &program,
   goto_programt::targett first_instruction,
   const goto_programt::targett &last_instruction,
-  const exprt &write_set,
+  dfcc_cfg_infot &cfg_info,
   std::set<irep_idt> &function_pointer_contracts)
 {
   for(auto &target = first_instruction; target != last_instruction; target++)
@@ -87,7 +88,7 @@ void dfcc_obeys_contractt::rewrite_calls(
               library.dfcc_fun_symbol[dfcc_funt::OBEYS_CONTRACT].name);
 
           // pass the write_set
-          target->call_arguments().push_back(write_set);
+          target->call_arguments().push_back(cfg_info.get_write_set(target));
 
           // record discovered function contract
           get_contract_name(
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h
@@ -21,6 +21,7 @@ Date: August 2022
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
+class dfcc_cfg_infot;
 class exprt;
 
 /// Rewrites calls to obeys_contract predicates into calls
@@ -39,7 +40,7 @@ class dfcc_obeys_contractt
   /// given write_set expression as parameter to the library function.
   void rewrite_calls(
     goto_programt &program,
-    const exprt &write_set,
+    dfcc_cfg_infot &cfg_info,
     std::set<irep_idt> &function_pointer_contracts);
 
   /// Rewrites calls to obeys_contract predicates into calls
@@ -50,7 +51,7 @@ class dfcc_obeys_contractt
     goto_programt &program,
     goto_programt::targett first_instruction,
     const goto_programt::targett &last_instruction,
-    const exprt &write_set,
+    dfcc_cfg_infot &cfg_info,
     std::set<irep_idt> &function_pointer_contracts);
 
 protected:
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp
@@ -15,6 +15,7 @@ Date: August 2022
 #include <util/std_code.h>
 #include <util/symbol.h>
 
+#include "dfcc_cfg_info.h"
 #include "dfcc_library.h"
 
 dfcc_pointer_in_ranget::dfcc_pointer_in_ranget(
@@ -26,20 +27,20 @@ dfcc_pointer_in_ranget::dfcc_pointer_in_ranget(
 
 void dfcc_pointer_in_ranget::rewrite_calls(
   goto_programt &program,
-  const exprt &write_set)
+  dfcc_cfg_infot cfg_info)
 {
   rewrite_calls(
     program,
     program.instructions.begin(),
     program.instructions.end(),
-    write_set);
+    cfg_info);
 }
 
 void dfcc_pointer_in_ranget::rewrite_calls(
   goto_programt &program,
   goto_programt::targett first_instruction,
   const goto_programt::targett &last_instruction,
-  const exprt &write_set)
+  dfcc_cfg_infot cfg_info)
 {
   auto &target = first_instruction;
   while(target != last_instruction)
@@ -64,7 +65,7 @@ void dfcc_pointer_in_ranget::rewrite_calls(
               library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name);
 
           // pass the write_set
-          target->call_arguments().push_back(write_set);
+          target->call_arguments().push_back(cfg_info.get_write_set(target));
         }
       }
     }
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h
@@ -21,6 +21,7 @@ Date: August 2022
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
+class dfcc_cfg_infot;
 class exprt;
 
 /// Rewrites calls to pointer_in_range predicates into calls
@@ -37,7 +38,7 @@ class dfcc_pointer_in_ranget
   /// Rewrites calls to pointer_in_range predicates into calls
   /// to the library implementation in the given program, passing the
   /// given write_set expression as parameter to the library function.
-  void rewrite_calls(goto_programt &program, const exprt &write_set);
+  void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info);
 
   /// Rewrites calls to pointer_in_range predicates into calls
   /// to the library implementation in the given program between
@@ -47,7 +48,7 @@ class dfcc_pointer_in_ranget
     goto_programt &program,
     goto_programt::targett first_instruction,
     const goto_programt::targett &last_instruction,
-    const exprt &write_set);
+    dfcc_cfg_infot cfg_info);
 
 protected:
   dfcc_libraryt &library;

Original file line number	Diff line number	Diff line change
`@@ -13,6 +13,7 @@ Date: August 2022`
`13`	`13`	`#include <util/pointer_expr.h>`
`14`	`14`	`#include <util/symbol.h>`
`15`	`15`
	`16`	`+#include "dfcc_cfg_info.h"`
`16`	`17`	`#include "dfcc_library.h"`
`17`	`18`
`18`	`19`	`dfcc_is_fresht::dfcc_is_fresht(`
`@@ -24,20 +25,20 @@ dfcc_is_fresht::dfcc_is_fresht(`
`24`	`25`
`25`	`26`	`void dfcc_is_fresht::rewrite_calls(`
`26`	`27`	`goto_programt &program,`
`27`		`- const exprt &write_set)`
	`28`	`+ dfcc_cfg_infot &cfg_info)`
`28`	`29`	`{`
`29`	`30`	`rewrite_calls(`
`30`	`31`	`program,`
`31`	`32`	`program.instructions.begin(),`
`32`	`33`	`program.instructions.end(),`
`33`		`- write_set);`
	`34`	`+ cfg_info);`
`34`	`35`	`}`
`35`	`36`
`36`	`37`	`void dfcc_is_fresht::rewrite_calls(`
`37`	`38`	`goto_programt &program,`
`38`	`39`	`goto_programt::targett first_instruction,`
`39`	`40`	`const goto_programt::targett &last_instruction,`
`40`		`- const exprt &write_set)`
	`41`	`+ dfcc_cfg_infot &cfg_info)`
`41`	`42`	`{`
`42`	`43`	`auto &target = first_instruction;`
`43`	`44`	`while(target != last_instruction)`
`@@ -61,7 +62,7 @@ void dfcc_is_fresht::rewrite_calls(`
`61`	`62`	`.set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name);`
`62`	`63`
`63`	`64`	`// pass the write_set`
`64`		`- target->call_arguments().push_back(write_set);`
	`65`	`+ target->call_arguments().push_back(cfg_info.get_write_set(target));`
`65`	`66`	`}`
`66`	`67`	`}`
`67`	`68`	`}`
Original file line number	Diff line number	Diff line change
`@@ -15,6 +15,7 @@ Date: August 2022`
`15`	`15`	`#include <util/std_code.h>`
`16`	`16`	`#include <util/symbol.h>`
`17`	`17`
	`18`	`+#include "dfcc_cfg_info.h"`
`18`	`19`	`#include "dfcc_library.h"`
`19`	`20`
`20`	`21`	`dfcc_pointer_in_ranget::dfcc_pointer_in_ranget(`
`@@ -26,20 +27,20 @@ dfcc_pointer_in_ranget::dfcc_pointer_in_ranget(`
`26`	`27`
`27`	`28`	`void dfcc_pointer_in_ranget::rewrite_calls(`
`28`	`29`	`goto_programt &program,`
`29`		`- const exprt &write_set)`
	`30`	`+ dfcc_cfg_infot cfg_info)`
`30`	`31`	`{`
`31`	`32`	`rewrite_calls(`
`32`	`33`	`program,`
`33`	`34`	`program.instructions.begin(),`
`34`	`35`	`program.instructions.end(),`
`35`		`- write_set);`
	`36`	`+ cfg_info);`
`36`	`37`	`}`
`37`	`38`
`38`	`39`	`void dfcc_pointer_in_ranget::rewrite_calls(`
`39`	`40`	`goto_programt &program,`
`40`	`41`	`goto_programt::targett first_instruction,`
`41`	`42`	`const goto_programt::targett &last_instruction,`
`42`		`- const exprt &write_set)`
	`43`	`+ dfcc_cfg_infot cfg_info)`
`43`	`44`	`{`
`44`	`45`	`auto &target = first_instruction;`
`45`	`46`	`while(target != last_instruction)`
`@@ -64,7 +65,7 @@ void dfcc_pointer_in_ranget::rewrite_calls(`
`64`	`65`	`library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name);`
`65`	`66`
`66`	`67`	`// pass the write_set`
`67`		`- target->call_arguments().push_back(write_set);`
	`68`	`+ target->call_arguments().push_back(cfg_info.get_write_set(target));`
`68`	`69`	`}`
`69`	`70`	`}`
`70`	`71`	`}`