Fix exp.volatiles_are_top and exp.globs_are_top being ignored by relational (Apron) analysis

src/analyses/apron/relationAnalysis.apron.ml

@@ -52,17 +52,23 @@ struct
   (* Functions for manipulating globals as temporary locals. *)
 
   let read_global ask getg st g x =
-    if ThreadFlag.has_ever_been_multi ask then
-      Priv.read_global ask getg st g x
-    else (
-      let rel = st.rel in
-      (* If it has escaped and we have never been multi-threaded, we can still refer to the local *)
-      let g_var = if g.vglob then RV.global g else RV.local g in
-      let x_var = RV.local x in
-      let rel' = RD.add_vars rel [g_var] in
-      let rel' = RD.assign_var rel' x_var g_var in
+    let x_var = RV.local x in
+    let rel' =
+      if ThreadFlag.has_ever_been_multi ask then
+        Priv.read_global ask getg st g x
+      else (
+        let rel = st.rel in
+        (* If it has escaped and we have never been multi-threaded, we can still refer to the local *)
+        let g_var = if g.vglob then RV.global g else RV.local g in
+        let rel' = RD.add_vars rel [g_var] in
+        let rel' = RD.assign_var rel' x_var g_var in
+        rel'
+      )
+    in
+    if (GobConfig.get_bool "exp.volatiles_are_top" && BaseUtil.is_always_unknown g) || GobConfig.get_bool "exp.globs_are_top" then
+      RD.forget_vars rel' [x_var]
+    else
       rel'
-    )
 
   module VH = BatHashtbl.Make (Basetype.Variables)
 

tests/regression/36-apron/100-volatiles-are-top.c

@@ -0,0 +1,19 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain interval --enable exp.volatiles_are_top
+// Test that exp.volatiles_are_top is respected by the relational (apron) analysis.
+// volatile and extern variables should be treated as top when read.
+#include <goblint.h>
+
+extern int ext;
+volatile int vol;
+
+int main(void) {
+  ext = 5;
+  int x = ext;   // x should be top: ext is extern, exp.volatiles_are_top is on
+  __goblint_check(x == 5); // UNKNOWN!
+
+  vol = 3;
+  int y = vol;   // y should be top: vol is volatile, exp.volatiles_are_top is on
+  __goblint_check(y == 3); // UNKNOWN!
+
+  return 0;
+}