Merge pull request #6102 from tautschnig/fix-wmm-shared_buffer

tautschnig · web-flow · commit 865d3b6f3e6d · 2021-05-12T14:11:58.000+02:00
goto-instrument/wmm: do not lookup non-existent symbols in the namespace
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwdrr005_POWER_ALL/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwdrr005_POWER_ALL/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 aclwdrr005.c
 POWER ALL
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwdrr005_POWER_OPC/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwdrr005_POWER_OPC/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 aclwdrr005.c
 POWER OPC
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwdrr015_POWER_ALL/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwdrr015_POWER_ALL/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwdrr015.c
 POWER ALL
 ^EXIT=10$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwdrr015_POWER_OPC/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwdrr015_POWER_OPC/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwdrr015.c
 POWER OPC
 ^EXIT=10$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_ALL/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_ALL/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwsrr000.c
 RMO ALL
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_OPC/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_OPC/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwsrr000.c
 RMO OPC
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_ALL/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_ALL/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwsrr002.c
 POWER ALL
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_OPC/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_OPC/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwsrr002.c
 POWER OPC
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwsrr002_RMO_ALL/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwsrr002_RMO_ALL/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwsrr002.c
 RMO ALL
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_aclwsrr002_RMO_OPC/test.desc b/regression/goto-instrument-wmm-core/ppc_aclwsrr002_RMO_OPC/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 aclwsrr002.c
 RMO OPC
 ^EXIT=0$
diff --git a/regression/goto-instrument-wmm-core/ppc_safe004_POWER_OPC/test.desc b/regression/goto-instrument-wmm-core/ppc_safe004_POWER_OPC/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 safe004.c
 POWER OPC
 ^EXIT=0$
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -41,41 +41,25 @@ const shared_bufferst::varst &shared_bufferst::operator()(
 
   vars.type=symbol.type;
 
-  vars.w_buff0=add(object, symbol.base_name, "$w_buff0", symbol.type);
-  vars.w_buff1=add(object, symbol.base_name, "$w_buff1", symbol.type);
+  vars.w_buff0 = add(symbol, "$w_buff0", symbol.type);
+  vars.w_buff1 = add(symbol, "$w_buff1", symbol.type);
 
-  vars.w_buff0_used=add(object, symbol.base_name, "$w_buff0_used",
-    bool_typet());
-  vars.w_buff1_used=add(object, symbol.base_name, "$w_buff1_used",
-    bool_typet());
+  vars.w_buff0_used = add(symbol, "$w_buff0_used", bool_typet());
+  vars.w_buff1_used = add(symbol, "$w_buff1_used", bool_typet());
 
-  vars.mem_tmp=add(object, symbol.base_name, "$mem_tmp", symbol.type);
-  vars.flush_delayed=add(object, symbol.base_name, "$flush_delayed",
-    bool_typet());
+  vars.mem_tmp = add(symbol, "$mem_tmp", symbol.type);
+  vars.flush_delayed = add(symbol, "$flush_delayed", bool_typet());
 
-  vars.read_delayed=
-    add(object, symbol.base_name, "$read_delayed", bool_typet());
-  vars.read_delayed_var=
-    add(
-      object,
-      symbol.base_name,
-      "$read_delayed_var",
-      pointer_type(symbol.type));
+  vars.read_delayed = add(symbol, "$read_delayed", bool_typet());
+  vars.read_delayed_var =
+    add(symbol, "$read_delayed_var", pointer_type(symbol.type));
 
   for(unsigned cnt=0; cnt<nb_threads; cnt++)
   {
-    vars.r_buff0_thds.push_back(
-      shared_bufferst::add(
-        object,
-        symbol.base_name,
-        "$r_buff0_thd"+std::to_string(cnt),
-        bool_typet()));
-    vars.r_buff1_thds.push_back(
-      shared_bufferst::add(
-        object,
-        symbol.base_name,
-        "$r_buff1_thd"+std::to_string(cnt),
-        bool_typet()));
+    vars.r_buff0_thds.push_back(shared_bufferst::add(
+      symbol, "$r_buff0_thd" + std::to_string(cnt), bool_typet()));
+    vars.r_buff1_thds.push_back(shared_bufferst::add(
+      symbol, "$r_buff1_thd" + std::to_string(cnt), bool_typet()));
   }
 
   return vars;
@@ -85,8 +69,7 @@ const shared_bufferst::varst &shared_bufferst::operator()(
 /// \par parameters: var, suffix, type of the var, added as an instrumentation
 /// \return identifier of the new var
 irep_idt shared_bufferst::add(
-  const irep_idt &object,
-  const irep_idt &base_name,
+  const symbolt &object,
   const std::string &suffix,
   const typet &type,
   bool instrument)
@@ -95,10 +78,10 @@ irep_idt shared_bufferst::add(
 
   symbolt &new_symbol = get_fresh_aux_symbol(
     type,
-    id2string(object) + suffix,
-    id2string(base_name) + suffix,
-    ns.lookup(object).location,
-    ns.lookup(object).mode,
+    id2string(object.name) + suffix,
+    id2string(object.base_name) + suffix,
+    object.location,
+    object.mode,
     symbol_table);
   new_symbol.is_static_lifetime=true;
   new_symbol.value.make_nil();
diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h
@@ -159,12 +159,8 @@ class shared_bufferst
   irep_idt choice(const irep_idt &function_id, const std::string &suffix)
   {
     const auto maybe_symbol = symbol_table.lookup(function_id);
-    const std::string function_base_name =
-      maybe_symbol
-        ? id2string(maybe_symbol->base_name)
-        : "main";
-    return add(function_base_name+"_weak_choice",
-      function_base_name+"_weak_choice", suffix, bool_typet());
+    CHECK_RETURN(maybe_symbol);
+    return add(*maybe_symbol, "_weak_choice" + suffix, bool_typet());
   }
 
   bool is_buffered(
@@ -244,29 +240,24 @@ class shared_bufferst
   messaget &message;
 
   irep_idt add(
-    const irep_idt &object,
-    const irep_idt &base_name,
+    const symbolt &object,
     const std::string &suffix,
     const typet &type,
     bool added_as_instrumentation);
 
-  irep_idt add(
-    const irep_idt &object,
-    const irep_idt &base_name,
-    const std::string &suffix,
-    const typet &type)
+  irep_idt
+  add(const symbolt &object, const std::string &suffix, const typet &type)
   {
-    return add(object, base_name, suffix, type, true);
+    return add(object, suffix, type, true);
   }
 
   /* inserting a non-instrumenting, fresh variable */
   irep_idt add_fresh_var(
-    const irep_idt &object,
-    const irep_idt &base_name,
+    const symbolt &object,
     const std::string &suffix,
     const typet &type)
   {
-    return add(object, base_name, suffix, type, false);
+    return add(object, suffix, type, false);
   }
 
   void add_initialization(goto_programt &goto_program);

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE`
`2`	`2`	`aclwdrr005.c`
`3`	`3`	`POWER ALL`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+THOROUGH`
`2`	`2`	`aclwdrr015.c`
`3`	`3`	`POWER ALL`
`4`	`4`	`^EXIT=10$`