diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
index a816d71fcd56a6f5ab7c3250b2f94e79d66c06b3..c39a616ce7e5ea1bb53d8bbd826cdc308701d539 100644
--- a/src/plugins/aorai/Makefile.in
+++ b/src/plugins/aorai/Makefile.in
@@ -51,6 +51,8 @@ PLUGIN_CMO:= bool3 \
path_analysis \
promelaoutput \
logic_simplification \
+ aorai_graph \
+ aorai_metavariables \
data_for_aorai \
aorai_utils \
ltl_output \
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 554af1f3639ad3531632e0f8dfec0de3e106852b..f6315b5ce509e2b506f61ef0a6446d5d1189eda2 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -265,7 +265,7 @@ let actions_to_range l =
in List.fold_left treat_one_action Cil_datatype.Term.Map.empty l
let make_start_transition ?(is_main=false) kf init_states =
- let auto = Data_for_aorai.getAutomata () in
+ let auto = Data_for_aorai.getGraph () in
let is_crossable =
if is_main then
Aorai_utils.isCrossableAtInit
@@ -303,7 +303,7 @@ let make_start_transition ?(is_main=false) kf init_states =
let make_return_transition kf state =
let s = Kernel_function.find_return kf in
set_return_state s state;
- let auto = Data_for_aorai.getAutomata () in
+ let auto = Data_for_aorai.getGraph () in
let treat_one_state state bindings acc =
let my_trans = Path_analysis.get_transitions_of_state state auto in
let last = Data_for_aorai.Aorai_state.Set.singleton state in
@@ -624,7 +624,7 @@ let compute_forward () =
if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
Aorai_option.abort "Main function %a is ignored by Aorai"
Kernel_function.pretty kf;
- let (states,_) = Data_for_aorai.getAutomata () in
+ let (states,_) = Data_for_aorai.getGraph () in
let start =
List.fold_left
(fun acc s ->
@@ -833,7 +833,7 @@ let filter_possible_states kf states =
let filter_return_states kf states =
let end_state = Return_state.find (Kernel_function.find_return kf) in
- let auto = Data_for_aorai.getAutomata () in
+ let auto = Data_for_aorai.getGraph () in
let is_possible_state start_state state _ =
try
let trans = Path_analysis.get_transitions_of_state state auto in
diff --git a/src/plugins/aorai/aorai_graph.ml b/src/plugins/aorai/aorai_graph.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9425f061212e66d0e319e2891086ff39ab6ff34d
--- /dev/null
+++ b/src/plugins/aorai/aorai_graph.ml
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Promelaast
+
+type state = Promelaast.state
+type transition = (typed_condition * action) trans
+
+module Vertex =
+struct
+ type t = state
+ let compare x y = x.nums - y.nums
+ let hash x = x.nums
+ let equal x y = x.nums = y.nums
+ let default = {
+ nums = -1; name = ""; multi_state = None;
+ acceptation = Bool3.False; init = Bool3.False
+ }
+end
+
+module Edge =
+struct
+ type t = transition
+ let compare x y = x.numt - y.numt
+ let default = {
+ numt = -1; start = Vertex.default; stop = Vertex.default;
+ cross = TTrue,[]
+ }
+end
+
+include Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Vertex) (Edge)
+
+let of_automaton auto =
+ let g = create () in
+ List.iter (fun t -> add_edge_e g (t.start,t,t.stop)) auto.trans;
+ g
+
+let states g =
+ fold_vertex (fun v acc -> v :: acc) g []
+
+let filter_states f g =
+ fold_vertex (fun v acc -> if f v then v :: acc else acc) g []
+
+let init_states g =
+ filter_states (fun v -> v.Promelaast.init = Bool3.True) g
+
+let edges g =
+ fold_edges_e (fun e acc -> e :: acc) g []
+
diff --git a/src/plugins/aorai/aorai_graph.mli b/src/plugins/aorai/aorai_graph.mli
new file mode 100644
index 0000000000000000000000000000000000000000..38d110bb4dba479a48aa7e1ecd1ddb6861344236
--- /dev/null
+++ b/src/plugins/aorai/aorai_graph.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type state = Promelaast.state
+type transition =
+ (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
+type edge = state * transition * state
+
+include Graph.Sig.I
+ with type V.t = state
+ and type V.label = state
+ and type E.t = edge
+ and type E.label = transition
+ and type edge := edge
+
+val of_automaton : Promelaast.typed_automaton -> t
+
+val states : t -> state list
+val init_states : t -> state list
+val edges : t -> edge list
+
diff --git a/src/plugins/aorai/aorai_metavariables.ml b/src/plugins/aorai/aorai_metavariables.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dfcfe026805ca0dbeb3cfb820888ac62bae9e4ea
--- /dev/null
+++ b/src/plugins/aorai/aorai_metavariables.ml
@@ -0,0 +1,143 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Promelaast
+
+
+let dkey_metavar_init = Aorai_option.register_category "metavar-init"
+
+module type InitAnalysisParam =
+sig
+ val is_metavariable : varinfo -> bool
+end
+
+module InitAnalysis (Env : InitAnalysisParam) =
+struct
+ type vertex = Aorai_graph.E.vertex
+ type edge = Aorai_graph.E.t
+ type g = Aorai_graph.t
+
+ module Set = Cil_datatype.Varinfo.Set
+ type data = Bottom | InitializedSet of Set.t
+
+ let dkey = dkey_metavar_init
+
+ let top = InitializedSet Set.empty
+
+ let init v =
+ if v.Promelaast.init = Bool3.True then top else Bottom
+
+ let direction = Graph.Fixpoint.Forward
+
+ let equal d1 d2 =
+ match d1, d2 with
+ | Bottom, d | d, Bottom -> d = Bottom
+ | InitializedSet s1, InitializedSet s2 -> Set.equal s1 s2
+
+ let join d1 d2 =
+ match d1, d2 with
+ | Bottom, d | d, Bottom -> d
+ | InitializedSet s1, InitializedSet s2 ->
+ InitializedSet (Set.inter s1 s2)
+
+ let used_metavariables cond =
+ let result = ref Set.empty in
+ let visit_term =
+ let v = object
+ inherit Visitor.frama_c_inplace
+ method!vlogic_var_use lv =
+ match lv.lv_origin with
+ | Some vi when Env.is_metavariable vi ->
+ result := Set.add vi !result;
+ Cil.SkipChildren
+ | _ -> Cil.SkipChildren
+ end in
+ fun t -> ignore (Visitor.visitFramacTerm v t)
+ in
+ let rec visit_cond = function
+ | TAnd (c1,c2) -> visit_cond c1; visit_cond c2
+ | TOr (c1,c2) -> visit_cond c1; visit_cond c2
+ | TNot (c) -> visit_cond c
+ | TRel (_,t1,t2) -> visit_term t1; visit_term t2
+ | TCall _ | TReturn _ | TTrue | TFalse -> ()
+ in
+ visit_cond cond;
+ !result
+
+ let pretty_state fmt st =
+ Format.pp_print_string fmt st.Promelaast.name
+
+ let pretty_set fmt set =
+ let l = Set.elements set in
+ Pretty_utils.pp_list ~sep:", " Cil_printer.pp_varinfo fmt l
+
+ let _pretty_data fmt = function
+ | Bottom -> Format.printf "Bottom"
+ | InitializedSet set -> pretty_set fmt set
+
+ let alarm (src,_tr,dst) vars =
+ Aorai_option.abort
+ "The metavariables %a may not be initialized before the transition \
+ from %a to %a."
+ pretty_set vars
+ pretty_state src
+ pretty_state dst
+
+ let analyze ((src,tr,dst) as edge) = function
+ | Bottom -> Bottom
+ | InitializedSet initialized ->
+ let cond,act = tr.cross in
+ (* Check that the condition uses only initialized variables *)
+ let used = used_metavariables cond in
+ let diff = Set.diff used initialized in
+ if not (Set.is_empty diff) then
+ alarm edge diff;
+ (* Add variables intialized by the condition *)
+ let add_initialized set = function
+ | Copy_value ((TVar({lv_origin = Some vi}),_),_) -> Set.add vi set
+ | _ -> set
+ in
+ let initialized' = List.fold_left add_initialized initialized act in
+ Aorai_option.debug ~dkey "%a {%a} -> %a {%a}"
+ pretty_state src pretty_set initialized
+ pretty_state dst pretty_set initialized';
+ InitializedSet initialized'
+end
+
+
+let checkInitialization auto =
+ let module P =
+ struct
+ let is_metavariable vi =
+ let module Map = Datatype.String.Map in
+ Map.exists (fun _ vi' -> (vi'.vid = vi.vid)) auto.metavariables
+ end
+ in
+ let module A = InitAnalysis (P) in
+ let module Fixpoint = Graph.Fixpoint.Make (Aorai_graph) (A) in
+ let g = Aorai_graph.of_automaton auto in
+ let _result = Fixpoint.analyze A.init g in
+ ()
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index f7a12ad4d258972d402972bab40bf14eb6e6a730..b9ea313fb7207c211f4fdc96b7ae9c54afde0e96 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -48,7 +48,7 @@ let convert_ltl_exprs t =
POr(c1,c2) -> POr (convert_cond c1, convert_cond c2)
| PAnd(c1,c2) -> PAnd(convert_cond c1, convert_cond c2)
| PNot c -> PNot (convert_cond c)
- | PCall _ | PReturn _ | PTrue | PFalse | AfVar _ -> cond
+ | PCall _ | PReturn _ | PTrue | PFalse | PAssign _ -> cond
| PRel(Neq,PVar x,PCst _) ->
(try
let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2)
@@ -109,10 +109,10 @@ let load_ya_file f =
let load_promela_file f =
try
let c = check_and_open_in f "invalid Promela file" in
- let (s,t) = Promelalexer.parse c in
- let t = convert_ltl_exprs t in
+ let auto = Promelalexer.parse c in
+ let trans = convert_ltl_exprs auto.trans in
close_in c;
- Data_for_aorai.setAutomata (s,t);
+ Data_for_aorai.setAutomata { auto with trans };
with
| Promelalexer.Error(loc,msg) -> syntax_error loc msg
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index b2c42ef706f776857dc628b11d2b232e40fbb9eb..5daa862d825c943c28f72abd2ccc46b654059d2d 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -896,7 +896,7 @@ let mk_global_comment txt = mk_global (GText (txt))
(** {b Initialization management / computation} *)
let mk_global_states_init root =
- let (states,_ as auto) = Data_for_aorai.getAutomata () in
+ let (states,_ as auto) = Data_for_aorai.getGraph () in
let states = List.sort Data_for_aorai.Aorai_state.compare states in
let is_possible_init state =
state.Promelaast.init = Bool3.True &&
@@ -1049,7 +1049,7 @@ let pred_of_condition subst subst_res label cond =
snd (aux None true cond)
let mk_deterministic_lemma () =
- let automaton = Data_for_aorai.getAutomata () in
+ let automaton = Data_for_aorai.getGraph () in
let make_one_lemma state =
let label = Cil_types.FormalLabel "L" in
let disjoint_guards acc trans1 trans2 =
@@ -1092,7 +1092,7 @@ let mk_deterministic_lemma () =
List.iter make_one_lemma (fst automaton)
let make_enum_states () =
- let state_list =fst (Data_for_aorai.getAutomata()) in
+ let state_list =fst (Data_for_aorai.getGraph()) in
let state_list =
List.map (fun x -> (x.Promelaast.name, x.Promelaast.nums)) state_list
in
@@ -1122,7 +1122,7 @@ let make_enum_states () =
let getInitialState () =
let loc = Cil_datatype.Location.unknown in
- let states = fst (Data_for_aorai.getAutomata()) in
+ let states = fst (Data_for_aorai.getGraph()) in
let s = List.find (fun x -> x.Promelaast.init = Bool3.True) states in
Cil.new_exp ~loc (Const (CEnum (find_enum s.nums)))
@@ -1165,11 +1165,12 @@ let initGlobals root complete =
mk_global_comment "//*";
List.iter mk_global_var (Data_for_aorai.aux_variables());
+ let auto = Data_for_aorai.getAutomata () in
mk_global_comment "//* ";
mk_global_comment "//****************** ";
mk_global_comment "//* Metavariables";
mk_global_comment "//*";
- Datatype.String.Map.iter (fun _ -> mk_global_var) !Data_for_aorai.global_table;
+ Datatype.String.Map.iter (fun _ -> mk_global_var) auto.metavariables;
if Aorai_option.Deterministic.get () then begin
(* must flush now previous globals which are used in the lemmas in order to
@@ -1209,7 +1210,7 @@ let automaton_locations loc =
Logic_const.new_identified_term
(Logic_const.tvar
(Data_for_aorai.get_state_logic_var state)), FromAny)
- (fst (Data_for_aorai.getAutomata()))
+ (fst (Data_for_aorai.getGraph()))
in
(Logic_const.new_identified_term
(Logic_const.tvar ~loc
@@ -1333,7 +1334,7 @@ let get_reachable_trans_to state st auto current_state =
(* force that we have a crossable transition for each state in which the
automaton might be at current event. *)
let force_transition loc f st current_state =
- let (states, _ as auto) = Data_for_aorai.getAutomata () in
+ let (states, _ as auto) = Data_for_aorai.getGraph () in
(* We iterate aux on all the states, to get
- the predicate indicating in which states the automaton cannot possibly
be before the transition (because we can't fire a transition from there).
@@ -1456,7 +1457,7 @@ forces that parent states of a state with action are mutually exclusive,
at least at pebble level.
*)
let incompatible_states loc st current_state =
- let (states,_ as auto) = Data_for_aorai.getAutomata () in
+ let (states,_ as auto) = Data_for_aorai.getGraph () in
let aux precond state =
let trans = get_reachable_trans_to state st auto current_state in
let actions = partition_action trans in
@@ -1834,7 +1835,7 @@ let auto_func_behaviors loc f st state =
in
Aorai_option.debug
"func behavior for %a (%s)" Kernel_function.pretty f call_or_ret;
- let (states, _) as auto = Data_for_aorai.getAutomata() in
+ let (states, _) as auto = Data_for_aorai.getGraph() in
let requires = auto_func_preconditions loc f st state in
let post_cond =
let called_pre =
@@ -1983,7 +1984,7 @@ let auto_func_block generated_kf loc f st status res =
in
Aorai_option.debug
~dkey "func code for %a (%s)" Kernel_function.pretty f call_or_ret;
- let (states, _) as auto = Data_for_aorai.getAutomata() in
+ let (states, _) as auto = Data_for_aorai.getGraph() in
(* For the following tests, we need a copy of every state. *)
@@ -2077,7 +2078,7 @@ let auto_func_block generated_kf loc f st status res =
new_funcs,res_block,local_var
let get_preds_wrt_params_reachable_states state f status =
- let auto = Data_for_aorai.getAutomata () in
+ let auto = Data_for_aorai.getGraph () in
let treat_one_trans acc tr = Logic_simplification.tor acc (fst tr.cross) in
let find_trans state prev tr =
Path_analysis.get_edges prev state auto @ tr
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index a0d12c2dc3e0d065997f9da436a1133bfefce998..ad68e06ec7a814d0195d322274e4e352366f3f2c 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -33,7 +33,7 @@ open Cil
let dkey = Aorai_option.register_category "action"
let get_acceptance_pred () =
- let (st,_) = Data_for_aorai.getAutomata () in
+ let (st,_) = Data_for_aorai.getGraph () in
List.fold_left
(fun acc s ->
match s.acceptation with
@@ -371,14 +371,14 @@ let pred_reachable reachable_states =
(nb, reachable,
Logic_const.pand (unreachable, Aorai_utils.is_out_of_state_pred state))
in
- let (states,_) = Data_for_aorai.getAutomata () in
+ let (states,_) = Data_for_aorai.getGraph () in
let (nb, reachable, unreachable) =
List.fold_left treat_one_state (0,pfalse,ptrue) states
in
(nb > 1, reachable, unreachable)
let possible_start kf (start,int) =
- let auto = Data_for_aorai.getAutomata () in
+ let auto = Data_for_aorai.getGraph () in
let trans = Path_analysis.get_edges start int auto in
let treat_one_trans cond tr =
Logic_const.por
@@ -388,7 +388,7 @@ let possible_start kf (start,int) =
Logic_const.pand (Aorai_utils.is_state_pred start, cond)
let neg_trans kf trans =
- let auto = Data_for_aorai.getAutomata () in
+ let auto = Data_for_aorai.getGraph () in
let rec aux l acc =
match l with
| [] -> acc
@@ -527,7 +527,7 @@ class visit_adding_pre_post_from_buch treatloops =
predicate_to_invariant kf stmt pred
end
in
- let (states,_) = Data_for_aorai.getAutomata () in
+ let (states,_) = Data_for_aorai.getGraph () in
List.iter treat_one_state states;
if has_multiple_choice then begin
let add_possible_state state _ acc =
@@ -584,7 +584,7 @@ class visit_adding_pre_post_from_buch treatloops =
Data_for_aorai.Aorai_state.Map.fold treat_one_state possible_states []
in
let partition_pre_state map =
- let (states,_) = Data_for_aorai.getAutomata () in
+ let (states,_) = Data_for_aorai.getGraph () in
let is_equiv st1 st2 =
let check_one _ o1 o2 =
match o1, o2 with
@@ -840,7 +840,7 @@ class visit_adding_pre_post_from_buch treatloops =
in
(i+1,bhv :: bhvs)
in
- let (states,_) = Data_for_aorai.getAutomata () in
+ let (states,_) = Data_for_aorai.getGraph () in
List.rev (snd (List.fold_left aux (0,bhvs) states))
end
in
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index a29a1f62c0cbb1c6cc71a72e170a830a5eae5033..1c9122c284cbec3ba4699d8653bc7b9ee883e10c 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -129,14 +129,14 @@ let pnot t =
let rec is_same_expression e1 e2 =
match e1,e2 with
- | AVar x, AVar y -> x = y
- | AVar _,_ | _,AVar _ -> false
| PVar x, PVar y -> x = y
| PVar _,_ | _,PVar _ -> false
| PCst cst1, PCst cst2 -> Logic_utils.is_same_pconstant cst1 cst2
| PCst _,_ | _,PCst _ -> false
| PPrm (f1,x1), PPrm(f2,x2) -> f1 = x1 && f2 = x2
| PPrm _,_ | _,PPrm _ -> false
+ | PMetavar x, PMetavar y -> x = y
+ | PMetavar _,_ | _,PMetavar _ -> false
| PBinop(b1,l1,r1), PBinop(b2,l2,r2) ->
b1 = b2 && is_same_expression l1 l2 && is_same_expression r1 r2
| PBinop _, _ | _, PBinop _ -> false
@@ -207,147 +207,7 @@ let buch_sync = "Aorai_Sync" (* Deprecated ? *)
(* ************************************************************************* *)
(* Buchi automata as stored after parsing *)
-let automata = ref ([],[])
-
-
-type table = varinfo Datatype.String.Map.t
-
-let global_table = ref Datatype.String.Map.empty (*mettre dans .mli*)
-
-
-module Automaton_graph =
-struct
- let dummy_vertex = List.hd (Aorai_state.reprs)
-
- module Vertex =
- struct
- type t = Promelaast.state
- let compare x y = x.nums - y.nums
- let hash x = x.nums
- let equal x y = x.nums = y.nums
- end
-
- module Edge =
- struct
- type t = (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
- let compare x y = x.numt - y.numt
- let default =
- {numt = -1; start = dummy_vertex; stop = dummy_vertex; cross = TTrue,[]}
- end
-
- include Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Vertex) (Edge)
-
- let of_automaton (_,transitions) =
- let g = create () in
- List.iter (fun t -> add_edge_e g (t.start,t,t.stop)) transitions;
- g
-end
-
-let dkey_metavar_init = Aorai_option.register_category "metavar-init"
-
-let checkVariableInitialization auto =
- let module A =
- struct
- type vertex = Automaton_graph.E.vertex
- type edge = Automaton_graph.E.t
- type g = Automaton_graph.t
-
- module Set = Cil_datatype.Varinfo.Set
- type data = Bottom | InitializedSet of Set.t
-
- let top = InitializedSet Set.empty
-
- let direction = Graph.Fixpoint.Forward
-
- let equal d1 d2 =
- match d1, d2 with
- | Bottom, d | d, Bottom -> d = Bottom
- | InitializedSet s1, InitializedSet s2 -> Set.equal s1 s2
-
- let join d1 d2 =
- match d1, d2 with
- | Bottom, d | d, Bottom -> d
- | InitializedSet s1, InitializedSet s2 ->
- InitializedSet (Set.inter s1 s2)
-
- let used_metavariables cond =
- let result = ref Set.empty in
- let visit_term =
- let v = object
- inherit Visitor.frama_c_inplace
- method!vlogic_var_use lv =
- match lv.lv_origin with
- | None -> Cil.SkipChildren
- | Some vi ->
- let module Map = Datatype.String.Map in
- if Map.exists (fun _ vi' -> (vi'.vid = vi.vid)) !global_table then
- result := Set.add vi !result;
- Cil.SkipChildren
- end in
- fun t -> ignore (Visitor.visitFramacTerm v t)
- in
- let rec visit_cond =
- function
- | TAnd (c1,c2) -> visit_cond c1; visit_cond c2
- | TOr (c1,c2) -> visit_cond c1; visit_cond c2
- | TNot (c) -> visit_cond c
- | TRel (_,t1,t2) -> visit_term t1; visit_term t2
- | TCall _ | TReturn _ | TTrue | TFalse -> ()
- in
- visit_cond cond;
- !result
-
- let pretty_state fmt st =
- Format.pp_print_string fmt st.name
-
- let pretty_set fmt set =
- let l = Set.elements set in
- Pretty_utils.pp_list ~sep:", " Cil_printer.pp_varinfo fmt l
-
- let _pretty_data fmt = function
- | Bottom -> Format.printf "Bottom"
- | InitializedSet set -> pretty_set fmt set
-
- let alarm (src,_trans,dst) vars =
- Aorai_option.abort
- "The metavariables %a may not be initialized before the transition \
- from %a to %a."
- pretty_set vars
- pretty_state src
- pretty_state dst
-
- let analyze ((src,trans,dst) as edge) = function
- | Bottom -> Bottom
- | InitializedSet initialized ->
- let cond,act = trans.cross in
- (* Check that the condition uses only initialized variables *)
- let used = used_metavariables cond in
- let diff = Set.diff used initialized in
- if not (Set.is_empty diff) then
- alarm edge diff;
- (* Add variables intialized by the condition *)
- let add_initialized set = function
- | Copy_value ((TVar({lv_origin = Some vi}),_),_) -> Set.add vi set
- | _ -> set
- in
- let initialized' = List.fold_left add_initialized initialized act in
- Aorai_option.debug ~dkey:dkey_metavar_init "%a {%a} -> %a {%a}"
- pretty_state src pretty_set initialized
- pretty_state dst pretty_set initialized';
- InitializedSet initialized'
- end
- in
- let module Initialization = Graph.Fixpoint.Make (Automaton_graph) (A) in
- let g = Automaton_graph.of_automaton auto in
- let init_states = Path_analysis.get_init_states auto in
- let init_data v =
- if List.exists (fun st -> st.nums = v.nums) init_states (* TODO: use sets *)
- then A.top
- else A.Bottom
- in
- let _result = Initialization.analyze init_data g in
- ()
-
+let automata = ref None
(* Each transition with a parametrized cross condition (call param access or return value access) has its parametrized part stored in this array. *)
let cond_of_parametrizedTransitions = ref (Array.make (1) [[]])
@@ -360,13 +220,24 @@ let functions_from_c = ref []
let ignored_functions = ref []
(** Return the buchi automata as stored after parsing *)
-let getAutomata () = !automata
+let getAutomata () =
+ match !automata with
+ | Some auto -> auto
+ | None ->
+ Aorai_option.fatal "The automaton has not been compiled yet"
+
+let getGraph () =
+ let auto = getAutomata () in
+ auto.states, auto.trans
(** Return the number of transitions of the automata *)
-let getNumberOfTransitions () = List.length (snd !automata)
+let getNumberOfTransitions () =
+ List.length (getAutomata ()).trans
(** Return the number of states of the automata *)
-let getNumberOfStates () = List.length (fst !automata)
+let getNumberOfStates () =
+ List.length (getAutomata ()).states
+
let is_c_global name =
try ignore (Globals.Vars.find_from_astinfo name VGlobal); true
@@ -487,7 +358,7 @@ let new_trans start stop cond =
{ start = start; stop = stop; cross = cond; numt = TransIndex.next () }
let check_states s =
- let states,trans = getAutomata() in
+ let {states;trans} = getAutomata() in
let max = getNumberOfStates () in
List.iter
(fun x -> if x.nums >= max then
@@ -565,17 +436,14 @@ type current_event =
repr of the stack does not take into account
this particular event. *)
-(*New definition of environment to be able to handle metavariable*)
-type env = { event:current_event list ; var:table}
-
let add_current_event event env cond =
let is_empty tbl = Cil_datatype.Varinfo.Hashtbl.length tbl = 0 in
- match env.event with
+ match env with
[] -> assert false
| old_event :: tl ->
match event, old_event with
| ENone, _ -> env, cond
- | _, ENone -> {env with event = event::tl}, cond
+ | _, ENone -> event::tl, cond
| ECall (kf1,_,_), ECall (kf2,_,_)
when Kernel_function.equal kf1 kf2 -> env, cond
| ECall (kf1,tbl1,_), ECall (kf2,tbl2,_)->
@@ -584,15 +452,15 @@ let add_current_event event env cond =
an empty event. If this situation occurs in an handwritten
automaton that uses formals we simply reject it.
*)
- if is_empty tbl1 && is_empty tbl2 then {env with event = ENone::tl}, TFalse
+ if is_empty tbl1 && is_empty tbl2 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: two call events for distinct \
functions %a and %a at the same time."
Kernel_function.pretty kf1 Kernel_function.pretty kf2
- | ECall (_,_,_), EMulti -> { env with event = event::tl }, cond
+ | ECall (_,_,_), EMulti -> event::tl, cond
| ECall (kf1,tbl1,_), EReturn kf2 ->
- if is_empty tbl1 then {env with event = ENone::tl}, TFalse
+ if is_empty tbl1 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: trying to call %a and \
@@ -600,62 +468,62 @@ let add_current_event event env cond =
Kernel_function.pretty kf1 Kernel_function.pretty kf2
| ECall(kf1,_,_), ECOR kf2
when Kernel_function.equal kf1 kf2 ->
- {env with event = event::tl}, cond
+ event::tl, cond
| ECall (kf1,tbl1,_), ECOR kf2 ->
- if is_empty tbl1 then {env with event = ENone::tl}, TFalse
+ if is_empty tbl1 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: trying to call %a and \
call or return from %a at the same time."
Kernel_function.pretty kf1 Kernel_function.pretty kf2
| EReturn kf1, ECall(kf2,tbl2,_) ->
- if is_empty tbl2 then {env with event = ENone::tl}, TFalse
+ if is_empty tbl2 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: trying to call %a and \
return from %a at the same time."
Kernel_function.pretty kf2 Kernel_function.pretty kf1
| EReturn kf1, (ECOR kf2 | EReturn kf2)
- when Kernel_function.equal kf1 kf2 -> {env with event = event::tl}, cond
- | EReturn _, EReturn _ -> {env with event = ENone::tl} , TFalse
- | EReturn _, ECOR _ -> {env with event = ENone::tl}, TFalse
- | EReturn _, EMulti -> {env with event = ENone::tl}, TFalse
+ when Kernel_function.equal kf1 kf2 -> event::tl, cond
+ | EReturn _, EReturn _ -> ENone::tl, TFalse
+ | EReturn _, ECOR _ -> ENone::tl, TFalse
+ | EReturn _, EMulti -> ENone::tl, TFalse
| (EMulti | ECOR _), _ -> assert false
(* These are compound event. They cannot be found as individual ones*)
let merge_current_event env1 env2 cond1 cond2 =
- assert (List.tl (env1.event) == List.tl (env2.event));
- let old_env = List.tl (env2.event) in
- match (List.hd (env1.event), List.hd (env2.event)) with
+ assert (List.tl env1 == List.tl env2);
+ let old_env = List.tl env2 in
+ match List.hd env1, List.hd env2 with
| ENone, _ -> env2, tor cond1 cond2
| _, ENone -> env1, tor cond1 cond2
| ECall(kf1,_,_), ECall(kf2,_,_)
when Kernel_function.equal kf1 kf2 -> env2, tor cond1 cond2
- | ECall _, ECall _ -> { env2 with event = EMulti::old_env}, tor cond1 cond2
+ | ECall _, ECall _ -> EMulti::old_env, tor cond1 cond2
| ECall _, EMulti -> env2, tor cond1 cond2
| ECall (kf1,_,_), ECOR kf2 when Kernel_function.equal kf1 kf2 ->
env2, tor cond1 cond2
| ECall (kf1,_,_), EReturn kf2 when Kernel_function.equal kf1 kf2 ->
- { env2 with event = ECOR kf1 :: old_env }, tor cond1 cond2
- | ECall _, (ECOR _ | EReturn _) -> { env2 with event = (EMulti :: old_env) }, tor cond1 cond2
+ ECOR kf1 :: old_env, tor cond1 cond2
+ | ECall _, (ECOR _ | EReturn _) -> EMulti :: old_env, tor cond1 cond2
| EReturn kf1, ECall (kf2,_,_) when Kernel_function.equal kf1 kf2 ->
- { env2 with event = ECOR kf1 :: old_env }, tor cond1 cond2
- | EReturn _, ECall _ -> { env2 with event = EMulti :: old_env }, tor cond1 cond2
+ ECOR kf1 :: old_env, tor cond1 cond2
+ | EReturn _, ECall _ -> EMulti :: old_env, tor cond1 cond2
| EReturn kf1, EReturn kf2 when Kernel_function.equal kf1 kf2 ->
env2, tor cond1 cond2
- | EReturn _, EReturn _ -> { env2 with event = EMulti :: old_env }, tor cond1 cond2
+ | EReturn _, EReturn _ -> EMulti :: old_env, tor cond1 cond2
| EReturn _, EMulti -> env2, tor cond1 cond2
| EReturn kf1, ECOR kf2 when Kernel_function.equal kf1 kf2 ->
env2, tor cond1 cond2
| EReturn _, ECOR _ ->
- { env2 with event = EMulti :: old_env }, tor cond1 cond2
+ EMulti :: old_env, tor cond1 cond2
| ECOR kf1, (ECall(kf2,_,_) | EReturn kf2 | ECOR kf2)
when Kernel_function.equal kf1 kf2 -> env1, tor cond1 cond2
| ECOR _, (ECall _ | EReturn _ | ECOR _) ->
- { env2 with event = EMulti :: old_env }, tor cond1 cond2
+ EMulti :: old_env, tor cond1 cond2
| ECOR _, EMulti -> env2, tor cond1 cond2
| EMulti, (ECall _ | EReturn _ | ECOR _) -> env1, tor cond1 cond2
- | EMulti, EMulti -> { env2 with event = EMulti::old_env }, tor cond1 cond2
+ | EMulti, EMulti -> EMulti::old_env, tor cond1 cond2
let get_bindings st my_var =
let my_lval = TVar my_var, TNoOffset in
@@ -714,15 +582,15 @@ let check_one top info counter s =
| ECOR _ | EReturn _ | EMulti | ENone -> None
-let find_metavar s env =
+let find_metavar s metaenv =
try
- Datatype.String.Map.find s (env.var)
+ Datatype.String.Map.find s metaenv
with Not_found ->
Aorai_option.abort "Metavariable %s not declared" s
let find_in_env env counter s =
let current, stack =
- match env.event with
+ match env with
| current::stack -> current, stack
| [] -> Aorai_option.fatal "Empty type-checking environment"
in
@@ -795,7 +663,7 @@ let find_prm_in_env env ?tr counter f x =
it in an aux variable or array here.
*)
env, Logic_const.tvar (Cil.cvar_to_lvar vi), cond
- in treat_env true env.event
+ in treat_env true env
end
module C_logic_env =
@@ -834,17 +702,17 @@ end
module LTyping = Logic_typing.Make(C_logic_env)
-let type_expr env ?tr ?current e =
+let type_expr metaenv env ?tr ?current e =
let loc = Cil_datatype.Location.unknown in
let rec aux env cond e =
match e with
| PVar s ->
let var = find_in_env env current s in
env, var, cond
- | AVar s ->
- let var = Logic_const.tvar (Cil.cvar_to_lvar (find_metavar s env)) in
- env, var, cond
| PPrm(f,x) -> find_prm_in_env env ?tr current f x
+ | PMetavar s ->
+ let var = Logic_const.tvar (Cil.cvar_to_lvar (find_metavar s metaenv)) in
+ env, var, cond
| PCst (Logic_ptree.IntConstant s) ->
let e = Cil.parseIntLogic ~loc s in
env, e, cond
@@ -1024,22 +892,22 @@ let type_expr env ?tr ?current e =
in
aux env TTrue e
-let type_cond needs_pebble env tr cond =
+let type_cond needs_pebble metaenv env tr cond =
let current = if needs_pebble then Some tr.stop else None in
let rec aux pos env =
function
- | AfVar (s, e) ->
+ | PAssign (s, e) ->
if not pos then
Aorai_option.abort
"Metavariable assignment cannot be done under a negation";
- let vi = Datatype.String.Map.find s !global_table in
- let env, e, c = type_expr env ~tr ?current e in
+ let vi = find_metavar s metaenv in
+ let env, e, c = type_expr metaenv env ~tr ?current e in
let assign = Copy_value ((TVar (Cil.cvar_to_lvar vi), TNoOffset), e) in
(* TODO: check type assignability *)
env, c, [assign]
| PRel(rel,e1,e2) ->
- let env, e1, c1 = type_expr env ~tr ?current e1 in
- let env, e2, c2 = type_expr env ~tr ?current e2 in
+ let env, e1, c1 = type_expr metaenv env ~tr ?current e1 in
+ let env, e2, c2 = type_expr metaenv env ~tr ?current e2 in
let call_cond = if pos then tand c1 c2 else tor (tnot c1) (tnot c2) in
let rel = TRel(Logic_typing.type_rel rel,e1,e2) in
let cond = if pos then tand call_cond rel else tor call_cond rel in
@@ -1093,7 +961,7 @@ let type_cond needs_pebble env tr cond =
else
env, TReturn kf, []
in
- aux true {env with event = ENone::env.event} cond
+ aux true (ENone::env) cond
module Reject_state =
State_builder.Option_ref(Aorai_state)
@@ -1113,7 +981,7 @@ let add_if_needed states st =
then st::states
else states
-let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
+let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end seq =
let loc = Cil_datatype.Location.unknown in
match seq with
| [] -> (* We identify start and end. *)
@@ -1166,7 +1034,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
if is_opt then TTrue
else
let e = Extlib.the elt.min_rep in
- let _,e,_ = type_expr env ?current e in
+ let _,e,_ = type_expr metaenv env ?current e in
(* If we have done at least the lower bound of cycles, we can exit
the loop. *)
TRel(Cil_types.Rle,e,counter)
@@ -1181,7 +1049,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
let e = Logic_const.tint ~loc i in
TRel(Cil_types.Rlt, counter, e)
| Some e ->
- let _,e,_ = type_expr env ?current e in
+ let _,e,_ = type_expr metaenv env ?current e in
Max_value_counter.replace counter e;
(* The counter is incremented after the test: it
must be strictly less than the upper bound to enter
@@ -1195,7 +1063,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
assert (elt.nested <> []);
(* we don't have a completely empty condition. *)
type_seq
- default_state tr env needs_pebble curr_start my_end elt.nested
+ default_state tr metaenv env needs_pebble curr_start my_end elt.nested
| Some cond ->
let seq_start =
match elt.nested with
@@ -1205,7 +1073,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
let trans_start = new_trans curr_start seq_start (Normal (TTrue,[]))
in
let inner_env, cond, act =
- type_cond needs_pebble env trans_start cond
+ type_cond needs_pebble metaenv env trans_start cond
in
let (env,states, seq_transitions, seq_end) =
match elt.nested with
@@ -1214,7 +1082,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
let intermediate = new_intermediate_state () in
let (env, states, transitions, _, seq_end) =
type_seq
- default_state tr
+ default_state tr metaenv
inner_env needs_pebble seq_start intermediate elt.nested
in env, states, transitions, seq_end
in
@@ -1227,12 +1095,12 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
Aorai_option.fatal
"Transition guard translated as epsilon transition");
let states = add_if_needed states seq_start in
- (match env.event with
+ (match env with
| [] | (ENone | ECall _) :: _ ->
(env, states, transitions, curr_start, seq_end)
| EReturn kf1 :: ECall (kf2,_,_) :: tl
when Kernel_function.equal kf1 kf2 ->
- {env with event = tl}, states, transitions, curr_start, seq_end
+ tl, states, transitions, curr_start, seq_end
| (EReturn _ | ECOR _ ) :: _ ->
(* If there is as mismatch (e.g. Call f; Return g), it will
be caught later. There are legitimate situations for
@@ -1241,12 +1109,12 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
*)
(env, states, transitions, curr_start, seq_end)
| EMulti :: env_tmp ->
- {env with event = env_tmp}, states, transitions, curr_start, seq_end)
+ env_tmp, states, transitions, curr_start, seq_end)
in
let loop_end = if has_loop then new_intermediate_state () else inner_end
in
let (_,oth_states,oth_trans,oth_start,_) =
- type_seq default_state tr env needs_pebble loop_end curr_end seq
+ type_seq default_state tr metaenv env needs_pebble loop_end curr_end seq
in
let trans = inner_trans @ oth_trans in
let states = List.fold_left add_if_needed oth_states inner_states in
@@ -1348,7 +1216,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq =
if needs_pebble then Some curr_start else None
in
let _,t,_ =
- type_expr env ?current (Extlib.the elt.min_rep)
+ type_expr metaenv env ?current (Extlib.the elt.min_rep)
in
TRel (Cil_types.Req, t, Logic_const.tinteger ~loc 0)
in
@@ -1432,7 +1300,7 @@ let find_otherwise_trans auto st =
try let tr = List.find (fun x -> x.cross = Otherwise) trans in Some tr.stop
with Not_found -> None
-let type_trans auto env tr =
+let type_trans auto metaenv env tr =
let needs_pebble = not (single_path auto tr) in
let has_siblings =
match Path_analysis.get_transitions_of_state tr.start auto with
@@ -1449,7 +1317,7 @@ let type_trans auto env tr =
let default_state = find_otherwise_trans auto tr.start in
let has_default_state = Extlib.has_some default_state in
let _,states, transitions,_,_ =
- type_seq has_default_state tr env needs_pebble tr.start tr.stop seq
+ type_seq has_default_state tr metaenv env needs_pebble tr.start tr.stop seq
in
let (states, transitions) =
if List.exists (fun st -> st.multi_state <> None) states then begin
@@ -1592,13 +1460,16 @@ let add_default_trans (states, transitions as auto) otherwise =
let transitions = List.fold_left add_one_trans transitions otherwise in
states, transitions
-let type_cond_auto (st,tr as auto) =
- let otherwise = List.filter (fun t -> t.cross = Otherwise) tr in
+let type_cond_auto auto =
+ let original_auto = auto in
+ let otherwise = List.filter (fun t -> t.cross = Otherwise) auto.trans in
let add_if_needed acc st =
if List.memq st acc then acc else st::acc
in
let type_trans (states,transitions,add_reject) tr =
- let (intermediate_states, trans, needs_reject) = type_trans auto {event = []; var = !global_table } tr in (*TODO*)
+ let (intermediate_states, trans, needs_reject) =
+ type_trans (auto.states,auto.trans) auto.metavariables [] tr
+ in
Aorai_option.debug
"Considering parsed transition %s -> %s" tr.start.name tr.stop.name;
Aorai_option.debug
@@ -1621,7 +1492,7 @@ let type_cond_auto (st,tr as auto) =
add_reject)
in
let (states, trans, add_reject) =
- List.fold_left type_trans (st,[],[]) tr
+ List.fold_left type_trans (auto.states,[],[]) auto.trans
in
let auto = propagate_epsilon_transitions (states, trans) in
let auto = add_reject_trans auto add_reject in
@@ -1630,12 +1501,13 @@ let type_cond_auto (st,tr as auto) =
must ensure that we use consecutive numbers starting from 0, or we'll
have needlessly long arrays.
*)
- let (states, transitions as auto) =
+ let states, trans =
match Reject_state.get_option () with
| Some state ->
(states, (new_trans state state (TTrue,[])):: transitions)
| None -> auto
in
+ let auto = { original_auto with states ; trans } in
if Aorai_option.debug_atleast 1 then
Promelaoutput.output_dot_automata auto "aorai_debug_typed.dot";
let (_,trans) =
@@ -1646,7 +1518,7 @@ let type_cond_auto (st,tr as auto) =
in match cond with
TFalse -> acc
| _ -> (i+1,{ t with cross = (cond,action); numt = i } :: l))
- (0,[]) transitions
+ (0,[]) trans
in
let _, states =
List.fold_left
@@ -1661,13 +1533,14 @@ let type_cond_auto (st,tr as auto) =
end else acc)
(0,[]) states
in
- (List.rev states, List.rev trans)
+ { original_auto with states = List.rev states; trans = List.rev trans }
+
(** Stores the buchi automaton and its variables and
functions as it is returned by the parsing *)
let setAutomata auto =
let auto = type_cond_auto auto in
- automata:=auto;
+ automata:=Some auto;
check_states "typed automata";
if Aorai_option.debug_atleast 1 then
Promelaoutput.output_dot_automata auto "aorai_debug_reduced.dot";
@@ -1677,14 +1550,16 @@ let setAutomata auto =
(* all transitions have a true parameterized guard, i.e. [[]] *)
cond_of_parametrizedTransitions :=
Array.make (getNumberOfTransitions ()) [[]] ;
- checkVariableInitialization auto
+ Aorai_metavariables.checkInitialization auto
-let getState num = List.find (fun st -> st.nums = num) (fst !automata)
+let getState num =
+ List.find (fun st -> st.nums = num) (getAutomata ()).states
-let getStateName num = (getState num).name
+let getStateName num =
+ (getState num).name
let getTransition num =
- List.find (fun trans -> trans.numt = num) (snd !automata)
+ List.find (fun trans -> trans.numt = num) (getAutomata ()).trans
(** Initializes some tables according to data from Cil AST. *)
let setCData () =
@@ -2181,6 +2056,7 @@ let debug_computed_state ?(dkey=dkey) () =
(* ************************************************************************* *)
let removeUnusedTransitionsAndStates () =
+ let auto = getAutomata () in
(* Step 1 : computation of reached states and crossed transitions *)
let treat_one_state state map set =
Aorai_state.Map.fold
@@ -2192,7 +2068,7 @@ let removeUnusedTransitionsAndStates () =
(Aorai_state.Set.add state set)
in
let reached _ state set = Aorai_state.Map.fold treat_one_state state set in
- let init = Path_analysis.get_init_states (getAutomata ()) in
+ let init = Path_analysis.get_init_states (getGraph ()) in
let reached_states = Pre_state.fold reached (Aorai_state.Set.of_list init) in
let reached_states = Post_state.fold reached reached_states in
let reached_states = Loop_init_state.fold reached reached_states in
@@ -2221,7 +2097,7 @@ let removeUnusedTransitionsAndStates () =
(i+1,
{ trans with start = new_start; stop = new_stop; numt = i } :: list)
with Not_found -> acc)
- (0,[]) (snd (getAutomata()))
+ (0,[]) auto.trans
in
let state_list = List.map new_state state_list in
Reject_state.may
@@ -2231,7 +2107,7 @@ let removeUnusedTransitionsAndStates () =
Reject_state.set new_reject
with Not_found -> Reject_state.clear ());
(* Step 3 : rewriting stored information *)
- automata:= (state_list,trans_list);
+ automata := Some { auto with states =state_list; trans = trans_list };
check_states "reduced automata";
let rewrite_state state =
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 908c003cf9a1791f3ebf9e0e0ff225a43e83a6db..2d440c0e0e881aaf4346133cb80ed4c0034ad177 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -56,7 +56,6 @@ val add_logic : string -> Cil_types.logic_info -> unit
(** *)
val get_logic : string -> Cil_types.logic_info
-val global_table : varinfo Datatype.String.Map.t ref
(** *)
val add_predicate : string -> Cil_types.logic_info -> unit
@@ -207,6 +206,9 @@ val new_trans: state -> state -> 'a -> 'a trans
(** Return the buchi automata as stored after parsing *)
val getAutomata : unit -> Promelaast.typed_automaton
+(** Return only the graph part of the automata *)
+val getGraph : unit -> state list * (typed_condition * action) trans list
+
(** Type-checks the parsed automaton and stores the result.
This might introduce new global variables in case of sequences.
*)
diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.mli
index 38bc6845c73736023f7ba5f208fc86170d73aa91..3f7ac668c9f4195a43edebe8f82d7b6e89a126c4 100644
--- a/src/plugins/aorai/promelaast.mli
+++ b/src/plugins/aorai/promelaast.mli
@@ -27,9 +27,9 @@
parser/lexer before its translation into Data_for_aorai module. *)
type expression =
- | AVar of string (* Metavariable *)
| PVar of string
| PPrm of string * string (* f().N *)
+ | PMetavar of string
| PCst of Logic_ptree.constant
| PBinop of Logic_ptree.binop * expression * expression
| PUnop of Logic_ptree.unop * expression
@@ -47,7 +47,7 @@ type condition =
| PCall of string * string option
(** Call might be done in a given behavior *)
| PReturn of string
- | AfVar of string * expression
+ | PAssign of string * expression
and seq_elt =
{ condition: condition option;
@@ -133,7 +133,11 @@ type 'condition trans =
}
(** Internal representation of a Buchi automata : a list of states and a list of transitions.*)
-type 'condition automaton = (state list) * ('condition trans list)
+type 'condition automaton = {
+ states: state list;
+ trans: ('condition trans) list;
+ metavariables: Cil_types.varinfo Datatype.String.Map.t;
+}
type parsed_automaton = parsed_condition automaton
diff --git a/src/plugins/aorai/promelaoutput.ml b/src/plugins/aorai/promelaoutput.ml
index 4e8bc5969d2095307b01ec11d8db9d1baefa61e2..85afe95f6ed1ec1e5c2a0199398ec14c9d0d5bc3 100644
--- a/src/plugins/aorai/promelaoutput.ml
+++ b/src/plugins/aorai/promelaoutput.ml
@@ -39,6 +39,7 @@ let string_of_unop = function
let rec print_parsed_expression fmt = function
| PVar s -> Format.fprintf fmt "%s" s
| PPrm (f,s) -> Format.fprintf fmt "%s().%s" f s
+ | PMetavar s -> Format.fprintf fmt "$%s" s
| PCst (IntConstant s) -> Format.fprintf fmt "%s" s
| PCst (FloatConstant s) -> Format.fprintf fmt "%s" s
| PCst (StringConstant s) -> Format.fprintf fmt "%S" s
@@ -54,7 +55,6 @@ let rec print_parsed_expression fmt = function
print_parsed_expression e1 print_parsed_expression e2
| PField(e,s) -> Format.fprintf fmt "%a.%s" print_parsed_expression e s
| PArrow(e,s) -> Format.fprintf fmt "%a->%s" print_parsed_expression e s
- | AVar s -> Format.fprintf fmt "%s" s
let rec print_parsed_condition fmt = function
| PRel(rel,e1,e2) ->
@@ -73,7 +73,7 @@ let rec print_parsed_condition fmt = function
| PCall (s,None) -> Format.fprintf fmt "CALL(%s)" s
| PCall (s, Some b) -> Format.fprintf fmt "CALL(%s::%s)" s b
| PReturn s -> Format.fprintf fmt "RETURN(%s)" s
- | AfVar (s, e) -> Format.fprintf fmt " %s := %a " s print_parsed_expression e
+ | PAssign (s, e) -> Format.fprintf fmt " %s := %a " s print_parsed_expression e
let rec print_seq_elt fmt elt =
Format.fprintf fmt "(%a%a){@[%a,%a@]}"
@@ -187,9 +187,9 @@ let print_statel fmt stl =
Format.fprintf fmt "@[<2>States:@\n%a@]"
(Pretty_utils.pp_list ~sep:"@\n" ~suf:"@\n" print_state) stl
-let print_raw_automata fmt (stl,trl) =
+let print_raw_automata fmt auto =
Format.fprintf fmt "@[<2>Automaton:@\n%a%a@]"
- print_statel stl print_transitionl trl
+ print_statel auto.states print_transitionl auto.trans
let dot_state out st =
let shape =
@@ -213,7 +213,7 @@ let dot_trans out tr =
print_state_label tr.stop
print_label tr
-let output_dot_automata (states_l,trans_l) fichier =
+let output_dot_automata {states ; trans} fichier =
let cout = open_out fichier in
let fmt = formatter_of_out_channel cout in
let output_functions = escape_newline fmt in
@@ -236,13 +236,13 @@ let output_dot_automata (states_l,trans_l) fichier =
one_line_comment " dot property.dot -Tps > property.ps";
Format.fprintf fmt "@[<2>@\ndigraph %s {@\n@\n%a@\n%a@\n%t}@\n@]"
(Filename.chop_extension (Filename.basename fichier))
- (Pretty_utils.pp_list dot_state) states_l
- (Pretty_utils.pp_list dot_trans) trans_l
+ (Pretty_utils.pp_list dot_state) states
+ (Pretty_utils.pp_list dot_trans) trans
(fun fmt ->
if DotSeparatedLabels.get () then
(Format.fprintf fmt
"/* guards of transitions */@\ncomment=\"%a\";@\n"
- (Pretty_utils.pp_list ~sep:"@\n" print_trans) trans_l));
+ (Pretty_utils.pp_list ~sep:"@\n" print_trans) trans));
Format.pp_set_formatter_out_functions fmt output_functions;
close_out cout
diff --git a/src/plugins/aorai/promelaparser.mly b/src/plugins/aorai/promelaparser.mly
index bae7efad71dad89aa34e2fa47ef4dea5cbda5de2..2946304bdbeba34476341be5a3471f92db860788 100644
--- a/src/plugins/aorai/promelaparser.mly
+++ b/src/plugins/aorai/promelaparser.mly
@@ -77,7 +77,7 @@ promela
st::l
) observed_states []
in
- (states , $3)
+ { states; trans = $3; metavariables = Datatype.String.Map.empty }
}
| PROMELA_NEVER PROMELA_LBRACE states PROMELA_SEMICOLON
PROMELA_RBRACE EOF {
@@ -91,7 +91,7 @@ promela
st::l
) observed_states []
in
- (states , $3) }
+ { states; trans = $3; metavariables = Datatype.String.Map.empty } }
;
states
diff --git a/src/plugins/aorai/promelaparser_withexps.mly b/src/plugins/aorai/promelaparser_withexps.mly
index 36f93360a5037fe1805b122424f6be432fa8c681..1fd125c99c7ae122256cc1f512f116e16dcc159f 100644
--- a/src/plugins/aorai/promelaparser_withexps.mly
+++ b/src/plugins/aorai/promelaparser_withexps.mly
@@ -88,7 +88,7 @@ promela
st::l
) observed_states []
in
- (states , $3)
+ { states; trans = $3; metavariables = Datatype.String.Map.empty }
}
| PROMELA_NEVER PROMELA_LBRACE states
PROMELA_SEMICOLON PROMELA_RBRACE EOF {
@@ -102,7 +102,7 @@ promela
st::l
) observed_states []
in
- (states , $3) }
+ { states; trans = $3; metavariables = Datatype.String.Map.empty } }
;
states
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index bc494754928b3af104a3d3f2016a20b45923b4cc..732342c02fbcb7ef139f70af0a6b3872f371b838 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -46,6 +46,7 @@ let is_no_repet (min,max) =
let observed_states = Hashtbl.create 1
let prefetched_states = Hashtbl.create 1
+let metavariables = ref Datatype.String.Map.empty
let fetch_and_create_state name =
Hashtbl.remove prefetched_states name ;
@@ -80,7 +81,7 @@ let add_metavariable name typename =
typename name
in
let vi = Cil.makeGlobalVar (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty in
- Data_for_aorai.global_table := Datatype.String.Map.add name vi !Data_for_aorai.global_table
+ metavariables := Datatype.String.Map.add name vi !metavariables
type pre_cond = Behavior of string | Pre of Promelaast.condition
@@ -156,7 +157,7 @@ main
end;
st::l)
observed_states []
- in
+ and trans = $2 in
(try
Hashtbl.iter
(fun _ st -> if st.init=True then raise Exit) observed_states;
@@ -172,7 +173,7 @@ main
in
Aorai_option.abort "%s" r
end;
- (states, $2)
+ { states; trans; metavariables = !metavariables }
}
;
@@ -330,16 +331,12 @@ single_cond:
| RETURN_OF LPAREN IDENTIFIER RPAREN { PReturn $3 }
| TRUE { PTrue }
| FALSE { PFalse }
- /*TODO*/
- | NOT single_cond { match $2 with
- | AfVar(_, _) -> Aorai_option.abort "Not corresponding to program" (*Parsing.symbol_end_pos*)
- | _ -> PNot $2 }
+ | NOT single_cond { PNot $2 }
| single_cond AND single_cond { PAnd ($1,$3) }
| single_cond OR single_cond { POr ($1,$3) }
| LPAREN single_cond RPAREN { $2 }
| logic_relation { $1 }
-/*TODO*/
- | VAR IDENTIFIER AFF arith_relation { AfVar($2, $4) }
+ | VAR IDENTIFIER AFF arith_relation { PAssign ($2, $4) }
;
logic_relation
@@ -391,6 +388,5 @@ access_leaf
| IDENTIFIER LPAREN RPAREN DOT IDENTIFIER { PPrm($1,$5) }
| IDENTIFIER { PVar $1 }
| LPAREN access RPAREN { $2 }
-/*TODO*/
- | VAR IDENTIFIER { AVar($2) }
+ | VAR IDENTIFIER { PMetavar $2 }
;