sim: deadcode should check program variable isn't part of any memory of globals in the current eq.

Author: Cameron-Low

src/ecPV.ml

@@ -698,6 +698,15 @@ module Mpv2 = struct
         Sm.exists check_mp mod_.PV.s_gl
       else false
 
+  let is_mod_pv' env pv eqo =
+    if is_glob pv then
+      let x = get_glob pv in
+      let check_mp mp =
+        let restr = NormMp.get_restr_use env mp in
+        not (NormMp.use_mem_xp x restr) in
+      Sm.exists check_mp eqo.s_gl
+    else false
+
   let is_mod_mp env mp mod_ =
     let restr = NormMp.get_restr_use env mp in
     let check_v pv _ty =

src/ecPV.mli

@@ -194,6 +194,7 @@ module Mpv2 : sig
   val split_nmod : env -> PV.t -> PV.t -> t -> t
   val split_mod : env -> PV.t -> PV.t -> t -> t
 
+  val is_mod_pv' : env -> prog_var -> t -> bool
   val mem_pv_l : env -> prog_var -> t -> bool
   val mem_pv_r : env -> prog_var -> t -> bool
 end

src/phl/ecPhlEqobs.ml

@@ -112,12 +112,14 @@ let check_lvalue aux lv =
 let check_not_l sim lvl eqo =
   let aux pv =
     check sim pv sim.sim_ifvl &&
+      not (Mpv2.is_mod_pv' sim.sim_env pv eqo) &&
       not (Mpv2.mem_pv_l sim.sim_env pv eqo) in
   check_lvalue aux lvl
 
 let check_not_r sim lvr eqo =
   let aux pv =
     check sim pv sim.sim_ifvr &&
+      not (Mpv2.is_mod_pv' sim.sim_env pv eqo) &&
       not (Mpv2.mem_pv_r sim.sim_env pv eqo) in
   check_lvalue aux lvr
 

theories/query_counting/Counter.eca

@@ -34,7 +34,7 @@ module Counter(S : System) = {
 }.
 
 section.
-  declare module S <: System.
+  declare module S <: System { -Counter }.
   declare module D <: Distinguisher { -S }.