From 9869b38e82ebe4596a6e6716a8ebcd1b40e409c0 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 27 Nov 2018 19:33:30 +0100
Subject: [PATCH] [Aorai] Add an history for Aorai current state variable
---
src/plugins/aorai/aorai_option.ml | 10 ++++++++++
src/plugins/aorai/aorai_option.mli | 2 ++
src/plugins/aorai/aorai_utils.ml | 25 +++++++++++++++++++++----
src/plugins/aorai/data_for_aorai.ml | 8 +++++++-
src/plugins/aorai/data_for_aorai.mli | 5 +++--
5 files changed, 43 insertions(+), 7 deletions(-)
diff --git a/src/plugins/aorai/aorai_option.ml b/src/plugins/aorai/aorai_option.ml
index 1dfe1a0504a..c31e0137a17 100644
--- a/src/plugins/aorai/aorai_option.ml
+++ b/src/plugins/aorai/aorai_option.ml
@@ -160,6 +160,16 @@ module Deterministic=
let default () = false
end)
+module InstrumentationHistory =
+ Int
+ (struct
+ let option_name = "-aorai-instrumentation-history"
+ let arg_name = "N"
+ let help = "the instrumentation will keep an history of the N last states"
+ let default = 0
+ end)
+
+
let is_on () =
not (Ltl_File.is_default () && To_Buchi.is_default () &&
Buchi.is_default () && Ya.is_default () )
diff --git a/src/plugins/aorai/aorai_option.mli b/src/plugins/aorai/aorai_option.mli
index 111cf0e74ea..636b793b218 100644
--- a/src/plugins/aorai/aorai_option.mli
+++ b/src/plugins/aorai/aorai_option.mli
@@ -43,6 +43,8 @@ module AddingOperationNameAndStatusInSpecification: Parameter_sig.Bool
(** [true] if the user declares that its ya automaton is deterministic. *)
module Deterministic: State_builder.Ref with type data = bool
+module InstrumentationHistory: Parameter_sig.Int
+
val is_on : unit -> bool
val promela_file: unit -> Filepath.Normalized.t
val advance_abstract_interpretation: unit -> bool
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 7615b72d83c..9d1f4b36412 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1132,9 +1132,12 @@ let initGlobals root complete =
mk_global_comment "//* ";
mk_global_comment "//* States and Trans Variables";
- if Aorai_option.Deterministic.get () then
- mk_global_c_var_init curState (getInitialState())
- else
+ if Aorai_option.Deterministic.get () then begin
+ mk_global_c_var_init curState (getInitialState());
+ let init = getInitialState() (* TODO a distinct initial value for history *)
+ and history = Data_for_aorai.whole_history () in
+ List.iter (fun name -> mk_global_c_var_init name init) history
+ end else
mk_global_states_init root;
if complete then begin
@@ -2120,6 +2123,20 @@ let auto_func_block generated_kf loc f st status res =
(Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f))))
loc
]
+ and stmt_history_update =
+ if Aorai_option.Deterministic.get () then
+ let history = Data_for_aorai.whole_history ()
+ and cur_state = Data_for_aorai.(get_varinfo curState) in
+ let add_stmt (src,acc) dst_name =
+ let dst = Data_for_aorai.get_varinfo dst_name in
+ let stmt = equalsStmt (Cil.var dst) (Cil.evar ~loc src) loc in
+ dst, stmt :: acc
+ in
+ snd (List.fold_left add_stmt (cur_state,[]) history)
+ else if Aorai_option.InstrumentationHistory.get () > 0 then
+ Aorai_option.fatal "history is not implemented for non-deterministic \
+ automaton"
+ else []
in
let new_funcs, local_var, main_stmt =
if Aorai_option.Deterministic.get() then
@@ -2130,7 +2147,7 @@ let auto_func_block generated_kf loc f st status res =
let ret = [ Cil.mkStmt ~ghost:true (Cil_types.Return(None,loc)) ] in
let res_block =
(Cil.mkBlock
- ( stmt_begin_list @ main_stmt @ ret))
+ ( stmt_begin_list @ stmt_history_update @ main_stmt @ ret))
in
res_block.blocals <- local_var;
Aorai_option.debug ~dkey "Generated body is:@\n%a"
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 157f44778f2..f4e4d3a64c0 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -177,7 +177,13 @@ let loopInit = "aorai_Loop_Init" (* OK *)
(* C variables *)
let curState = "aorai_CurStates" (* OK *)
-let curStateOld = "aorai_CurStates_old" (* OK *)
+let history n = "aorai_StatesHistory_" ^ string_of_int n (* OK *)
+let whole_history () =
+ let rec aux acc n =
+ if n > 0 then aux (history n :: acc) (n - 1) else acc
+ in
+ aux [] (Aorai_option.InstrumentationHistory.get ())
+
let curTrans = "aorai_CurTrans" (* OK *)
(*let curTransTmp = "aorai_CurTrans_tmp" (* OK *)*)
let curOp = "aorai_CurOperation" (* OK *)
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 786ca7217fb..b5869d06117 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -130,8 +130,9 @@ val curOpStatus : string
(** Name of curState C generated variable (Table of states that can be synchronized with the program) *)
val curState : string
-(** Name of curStateOld C generated variable (Last value of curState) *)
-val curStateOld : string
+(** Name of the history variables (History of previous states) *)
+val history : int -> string
+val whole_history : unit -> string list
(** Name of curTrans C generated variable (Last transitions that can be crossed) *)
val curTrans : string
--
GitLab