disabling permanently dead rules

Author: Jérôme FERET

core/KaSa_rep/export/export.ml

@@ -2678,13 +2678,13 @@ functor
             ))
       in
       *)
-    let permanently_remove l state = 
+    let permanently_remove l lrules state = 
       let state, c_compil = get_c_compilation state in
       let errors = get_errors state in 
       let parameters = get_parameters state in 
       let state, kappa_handler = get_handler state in 
       let map = c_compil.Cckappa_sig.working_set_valuations in 
-      let errors, l = List.fold_left 
+       let errors, l = List.fold_left 
                 (fun (errors, l) elt -> 
                   let errors, (id,_) = Ckappa_sig.Ws_index_map_and_set.Map.find_default parameters
                   errors
@@ -2693,8 +2693,9 @@ functor
                   errors, (Ckappa_sig.mvbdu_var_of_guard  id (Handler.get_nsites kappa_handler))::l)
                    (errors, []) l 
                 in 
-      let l = List.sort compare l in   
-      let state =set_errors errors state in 
+    
+                let l = List.sort compare l in   
+                let state =set_errors errors state in 
       let state = 
         match Remanent_state.get_reachability_result state with 
         | None -> state
@@ -2706,7 +2707,12 @@ functor
           let state = set_errors errors state in 
           let errors, (a,b)  = Reachability.map_mvbdu 
           (fun parameters errors bdu_handler mvbdu -> Ckappa_sig.Views_bdu.mvbdu_definitely_remove parameters bdu_handler errors mvbdu l ) errors (snd (fst x)) (snd x) in 
-          let state = Remanent_state.set_reachability_result ((fst (fst x),a),b) state in 
+          let lrules = List.rev_map Ckappa_sig.rule_id_of_int (List.rev lrules) in 
+       (*   let errors, (a,b) = Reachability.remove_rule_list errors a b lrules in *)
+          let gb = Reachability.get_global_dynamic_information b in 
+          let errors, (g,gb) = Analyzer_headers.remove_rule_list errors (fst (fst x)) gb lrules in 
+          let b = Reachability.set_global_dynamic_information gb b in 
+          let state = Remanent_state.set_reachability_result ((g,a),b) state in 
           set_errors errors state in 
       state  
 
@@ -2810,7 +2816,7 @@ functor
       let state, acc =
         permanently_disable_init_c_id_list diff.Diff.diff_init.removed_elt state acc
       in
-      let state = permanently_remove acc state in   
+      let state = permanently_remove acc diff.Diff.diff_rules.removed_elt  state in   
       let state, handler = get_handler state in
       let state, cc_compil = get_c_compilation state in
       let errors = get_errors state in

core/KaSa_rep/frontend/preprocess.ml

@@ -668,7 +668,7 @@ let translate_view parameters error handler (k : Ckappa_sig.c_agent_id)
                 Misc_sa.const_unit site_dic
             in
             (match bool, output with
-            | true, _ ->
+           | true, _ ->
               ( error,
                 ( c_interface,
                   bond_list,

core/KaSa_rep/reachability_analysis/analyzer.ml

@@ -96,6 +96,23 @@ module type Analyzer = sig
      dynamic_information 
      -> Exception.exceptions_caught_and_uncaught * (static_information*
     dynamic_information)
+
+    val remove_rule_list: 
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information -> Ckappa_sig.c_rule_id list -> 
+      Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
+
+    val get_global_dynamic_information :
+    dynamic_information -> Analyzer_headers.global_dynamic_information
+
+  val set_global_dynamic_information :
+    Analyzer_headers.global_dynamic_information ->
+    dynamic_information ->
+    dynamic_information
+   
 end
 
 (***************************************************************************)
@@ -455,7 +472,31 @@ module Make (Domain : Composite_domain.Composite_domain) = struct
 
 
   let map_mvbdu f errors static dynamic  = 
-    let error, (static, dynamic) = Domain.map_mvbdu f errors static dynamic in 
-    error, ((static), dynamic)
+    let parameters = Domain.get_parameters static in 
+    let errors, (static, dynamic) = Domain.map_mvbdu f errors static dynamic in 
+    let handler = get_bdu_handler dynamic in 
+    let errors, handler, restriction_mvbdu = f parameters errors handler (Domain.get_restriction_mvbdu static) in 
+    let errors, handler, working_set_mvbdu = f parameters errors handler (Domain.get_working_set_mvbdu static) in 
+    let static = Domain.set_restriction_mvbdu restriction_mvbdu static in 
+    let static = Domain.set_working_set_mvbdu working_set_mvbdu static in 
+    let dynamic = set_bdu_handler handler dynamic in 
+    errors, (static, dynamic)
+
+let remove_rule_list  errors static dynamic l = 
+  let parameters = Domain.get_parameters static in 
+  let handler = get_bdu_handler dynamic in 
+  let errors, handler, mv_false = Ckappa_sig.Views_bdu.mvbdu_false parameters handler errors in 
+  let dynamic = set_bdu_handler handler dynamic in 
+  let map = Domain.get_guard_mvbdus static in 
+  let map = 
+  List.fold_left 
+    (fun map id -> 
+      Ckappa_sig.Rule_setmap.Map.add id mv_false map)
+     map l  in 
+  let static = Domain.set_guard_mvbdus map static in 
+  errors, (static, dynamic) 
+  
+ let get_global_dynamic_information = Domain.get_global_dynamic_information 
+let set_global_dynamic_information = Domain.set_global_dynamic_information 
 
 end

core/KaSa_rep/reachability_analysis/analyzer.mli

@@ -96,6 +96,22 @@ module type Analyzer = sig
      dynamic_information 
      -> Exception.exceptions_caught_and_uncaught * (static_information*
     dynamic_information)
+ 
+  val remove_rule_list: 
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information -> Ckappa_sig.c_rule_id list -> 
+      Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
+   
+    val get_global_dynamic_information :
+    dynamic_information -> Analyzer_headers.global_dynamic_information
+
+  val set_global_dynamic_information :
+    Analyzer_headers.global_dynamic_information ->
+    dynamic_information ->
+    dynamic_information
 
 end
 

core/KaSa_rep/reachability_analysis/analyzer_headers.ml

@@ -44,6 +44,7 @@ type ('static, 'dynamic) kasa_state =
 type initial_state = Cckappa_sig.enriched_init
 
 let get_wake_up_relation static = static.global_wake_up_relation
+let set_wake_up_relation global_wake_up_relation static = {static with global_wake_up_relation}
 let get_parameter static = static.global_parameter
 let get_compilation_information static = static.global_compilation_result
 
@@ -284,9 +285,15 @@ let set_mvbdu_handler bdu_handler dynamic =
   { dynamic with mvbdu_handler = bdu_handler }
 
 let get_guard_mvbdus static = static.global_guard_mvbdus
+let set_guard_mvbdus global_guard_mvbdus static = {static with global_guard_mvbdus}
+
 let get_restriction_mvbdu static = static.global_restriction_mvbdu
 let get_working_set_mvbdu static = static.global_working_set_mvbdu
 
+let set_restriction_mvbdu global_restriction_mvbdu static = {static with global_restriction_mvbdu}
+let set_working_set_mvbdu global_working_set_mvbdu
+ static = {static with global_working_set_mvbdu}
+
 let get_nr_guard_parameters static =
   Handler.get_nr_guard_parameters (get_kappa_handler static)
 
@@ -422,6 +429,23 @@ let abstract_away_working_set_vars parameters error bdu_handler mvbdu
   in
   error, bdu_handler, mvbdu
 
+let remove_rule_list  errors static dynamic l = 
+  let parameters = get_parameter static in 
+  let handler = get_mvbdu_handler dynamic in 
+  let errors, handler, mv_false = Ckappa_sig.Views_bdu.mvbdu_false parameters handler errors in 
+  let dynamic = set_mvbdu_handler handler dynamic in 
+  let map = get_guard_mvbdus static in 
+  let map = 
+  List.fold_left 
+    (fun map id -> 
+      Ckappa_sig.Rule_setmap.Map.add id mv_false map)
+     map l  in 
+  let static = set_guard_mvbdus map static in 
+  let map = get_wake_up_relation static in 
+  let errors, map = Common_static.remove_rule_list parameters errors map l in 
+  let static = set_wake_up_relation map static in 
+  errors, (static, dynamic) 
+
 module AbstractWS (IntStorageT : Int_storage.Storage with type dimension = int) =
 struct
   let abstract_away_working_set_vars parameters error bdu_handler global_static
@@ -480,3 +504,5 @@ module AbstractWSMap (MapT : Map_wrapper.S_with_logs) = struct
     in
     error, bdu_handler, result
 end
+
+

core/KaSa_rep/reachability_analysis/analyzer_headers.mli

@@ -229,15 +229,24 @@ val get_guard_mvbdus :
   global_static_information ->
   Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t
 
+val set_guard_mvbdus : 
+  Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t -> global_static_information -> global_static_information
+
 val get_restriction_mvbdu :
   global_static_information -> Ckappa_sig.Views_bdu.mvbdu
 
+val set_restriction_mvbdu : 
+  Ckappa_sig.Views_bdu.mvbdu -> global_static_information -> global_static_information
+
 val get_nr_guard_parameters :
   global_static_information -> Ckappa_sig.c_guard_parameter
 
 val get_working_set_mvbdu :
   global_static_information -> Ckappa_sig.Views_bdu.mvbdu
 
+val set_working_set_mvbdu : 
+ Ckappa_sig.Views_bdu.mvbdu -> global_static_information -> global_static_information
+
 val get_nsites : global_static_information -> Ckappa_sig.c_site_name
 
 val get_mvbdu_handler :
@@ -268,6 +277,14 @@ val dummy_side_effects :
   Ckappa_sig.c_rule_id ->
   Exception.exceptions_caught_and_uncaught * Ckappa_sig.side_effects option
 
+val remove_rule_list: 
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   global_static_information -> 
+     global_dynamic_information -> Ckappa_sig.c_rule_id list -> 
+      Exception.exceptions_caught_and_uncaught * (global_static_information*
+    global_dynamic_information)
+
 module AbstractWS
     (IntStorageT : Int_storage.Storage with type dimension = int) : sig
   val abstract_away_working_set_vars :

core/KaSa_rep/reachability_analysis/common_static.ml

@@ -1179,7 +1179,7 @@ let scan_rule_set ?patch parameter error kappa_handler compil store_result =
 (******************************************************************)
 
 let compute_restriction_mvbdu ?patch_compute_restriction_mvbdu parameters error
-    mvbdu_handler nr_guard_parameters nsites compilation =
+    mvbdu_handler nr_guard_parameters nsites _compilation =
   let starting_mvbdu, starting =
     match patch_compute_restriction_mvbdu with
     | Some (_, mvbdu, i) -> Some mvbdu, Some i
@@ -1200,33 +1200,33 @@ let compute_restriction_mvbdu ?patch_compute_restriction_mvbdu parameters error
     Ckappa_sig.Views_bdu.mvbdu_of_range_list parameters mvbdu_handler error
       pair_list
   in
-  let error, ws_list =
+(*  let error, ws_list =
     Ckappa_sig.Ws_index_map_and_set.Map.fold
       (fun ws (guard, _) (error, pair_list) ->
         let error, b =
           Cckappa_sig.is_ws_permanently_disabled parameters error ws compilation
         in
         ( error,
           if b then
-            ( Ckappa_sig.mvbdu_var_of_guard guard nsites,
+           (* ( Ckappa_sig.mvbdu_var_of_guard guard nsites,
               ( Some Ckappa_sig.dummy_state_index_false,
                 Some Ckappa_sig.dummy_state_index_false ) )
-            :: pair_list
+            ::*) pair_list
           else
             pair_list ))
       compilation.Cckappa_sig.working_set_valuations (error, [])
   in
   let error, mvbdu_handler, mvbdu_ws =
     Ckappa_sig.Views_bdu.mvbdu_of_range_list parameters mvbdu_handler error
       (List.rev ws_list)
-  in
-  let error, mvbdu_handler, mvbdu =
+  in*)
+  (*let error, mvbdu_handler, mvbdu =*)
     match starting_mvbdu with
     | None -> error, mvbdu_handler, mvbdu
     | Some a ->
       Ckappa_sig.Views_bdu.mvbdu_and parameters mvbdu_handler error a mvbdu
-  in
-  Ckappa_sig.Views_bdu.mvbdu_and parameters mvbdu_handler error mvbdu_ws mvbdu
+(*  in
+  Ckappa_sig.Views_bdu.mvbdu_and parameters mvbdu_handler error mvbdu_ws mvbdu*)
 
 let collect_guard_mvbdus ?patch_collect_guard_mvbdus parameters error
     mvbdu_handler compilation bdu_restriction nsites =
@@ -1327,3 +1327,23 @@ let get_tuple_of_interest parameters error agent site map =
   with
   | error, None -> error, Ckappa_sig.PairAgentSitesState_map_and_set.Set.empty
   | error, Some s -> error, s
+
+let remove_rule_list parameters errors site_to_rules l' = 
+  let rec aux list l acc = 
+    match list, l with 
+      | [], _ -> List.rev acc 
+      | _, [] -> (List.rev acc) @ list 
+      | a::b,t::_ when compare a t < 0 -> aux b l (a::acc)
+      | a::b,t::q when compare a t = 0 -> aux b q acc 
+      | a::_,t::q when compare a t > 0 -> aux list q acc 
+      | _, _ -> assert false 
+  in 
+  let diff l l' = aux l l' [] in 
+  Ckappa_sig.Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif.fold 
+    parameters errors  
+    (fun parameters errors i l m -> 
+       Ckappa_sig.Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif.set parameters errors 
+        i (diff l l') m)
+     site_to_rules 
+     site_to_rules 
+    

core/KaSa_rep/reachability_analysis/composite_domain.ml

@@ -99,7 +99,15 @@ module type Composite_domain = sig
   val get_parameters : static_information -> Remanent_parameters_sig.parameters
   val enable_or_disable_rule : (Cckappa_sig.compil, static_information) unary
 
-   val map_mvbdu: 
+   
+   val get_restriction_mvbdu: static_information -> Ckappa_sig.Views_bdu.mvbdu  
+  val set_restriction_mvbdu: Ckappa_sig.Views_bdu.mvbdu -> static_information -> static_information 
+val get_working_set_mvbdu: static_information -> Ckappa_sig.Views_bdu.mvbdu  
+  val set_working_set_mvbdu: Ckappa_sig.Views_bdu.mvbdu -> static_information -> static_information 
+
+  val get_guard_mvbdus: static_information -> Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t
+  val set_guard_mvbdus: Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t-> static_information -> static_information 
+  val map_mvbdu: 
      (Remanent_parameters_sig.parameters 
  -> Exception.exceptions_caught_and_uncaught -> Ckappa_sig.Views_bdu.handler -> Ckappa_sig.Views_bdu.mvbdu -> Exception.exceptions_caught_and_uncaught * Ckappa_sig.Views_bdu.handler * Ckappa_sig.Views_bdu.mvbdu) ->
    Exception.exceptions_caught_and_uncaught 
@@ -108,8 +116,11 @@ module type Composite_domain = sig
      dynamic_information 
      -> Exception.exceptions_caught_and_uncaught * (static_information*
     dynamic_information)
+
 end
 
+
+
 (****************************************************************************)
 (*Analyzer is a functor takes a module Domain as its parameters.*)
 
@@ -133,6 +144,8 @@ module Make (Domain : Analyzer_domain_sig.Domain) = struct
   let set_bonds bonds dynamic = { dynamic with bonds }
   let get_global_static_information = fst
   let get_domain_static_information = snd
+
+  let set_global_static_information a (_,b) = (a,b)
   let lift f x = f (get_global_static_information x)
   let get_parameter static = lift Analyzer_headers.get_parameter static
   let get_compil static = lift Analyzer_headers.get_cc_code static
@@ -699,5 +712,31 @@ let map_mvbdu f errors static dynamic =
 in 
   errors, ((fst static, dstatic), 
           ({dynamic with domain}))
-          
+ 
+let get_restriction_mvbdu static = 
+  Analyzer_headers.get_restriction_mvbdu (get_global_static_information static)
+let get_working_set_mvbdu static = 
+  Analyzer_headers.get_working_set_mvbdu (get_global_static_information static)
+
+let get_guard_mvbdus static = 
+   Analyzer_headers.get_guard_mvbdus (get_global_static_information static)
+
+let set_restriction_mvbdu bdu static = 
+  let global = get_global_static_information static in 
+  let global = Analyzer_headers.set_restriction_mvbdu bdu global in 
+  set_global_static_information global static 
+
+let set_working_set_mvbdu bdu static = 
+   let global = get_global_static_information static in 
+  let global = Analyzer_headers.set_working_set_mvbdu bdu global in 
+  set_global_static_information global static 
+
+
+
+  let set_guard_mvbdus bdu static = 
+    let global = get_global_static_information static in 
+  let global = Analyzer_headers.set_guard_mvbdus bdu global in 
+  set_global_static_information global static 
+
+
 end