diff --git a/.Makefile.lint b/.Makefile.lint index db7beb8b71b8c1c6fc848d2a38c54b179fb0a26b..e9056d2e216fb962a7e5f928aa6c3cf864b4bb78 100644 --- a/.Makefile.lint +++ b/.Makefile.lint @@ -168,9 +168,6 @@ ML_LINT_KO+=src/plugins/aorai/logic_simplification.ml ML_LINT_KO+=src/plugins/aorai/logic_simplification.mli ML_LINT_KO+=src/plugins/aorai/ltl_output.ml ML_LINT_KO+=src/plugins/aorai/path_analysis.ml -ML_LINT_KO+=src/plugins/aorai/promelaast.mli -ML_LINT_KO+=src/plugins/aorai/promelaoutput.ml -ML_LINT_KO+=src/plugins/aorai/promelaoutput.mli ML_LINT_KO+=src/plugins/aorai/utils_parser.ml ML_LINT_KO+=src/plugins/callgraph/callgraph_api.mli ML_LINT_KO+=src/plugins/callgraph/cg.ml diff --git a/.gitignore b/.gitignore index c4204e5ff6e7981f0a1fa70898438580dd785939..a2f38663078062c50368522097ca56df17535309 100644 --- a/.gitignore +++ b/.gitignore @@ -98,8 +98,10 @@ autom4te.cache /doc/aorai/frama-c-aorai-example.tgz /doc/aorai/frama-c-aorai-example /doc/aorai/main.pdf +/doc/aorai/ya_file.tex /doc/aorai/basic_ya.tex /doc/aorai/extended_ya.tex +/doc/aorai/ya_variables.tex /doc/code/print_api/*.html /doc/code/print_api/*.dot diff --git a/Makefile b/Makefile index 647c9af39913a6426e12726286ad2892783d631b..425f754815018e9fc44c1fb3cd645dfefc513942 100644 --- a/Makefile +++ b/Makefile @@ -1708,7 +1708,10 @@ check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -path '*/tests' -prune '!' -name '*') ALL_ML_FILES+=ptests/ptests.ml + +ifeq ($(origin MANUAL_ML_FILES),undefined) MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES)) +endif # Allow control of files to be linted/fixed by external sources # (e.g. pre-commit hook that will concentrate on files which have changed) diff --git a/doc/aorai/Makefile b/doc/aorai/Makefile index 64dd2da0479967a0679830c4985166a1959610db..515b0938ec06b9de1bd34f5ad8c4e9f97b161cca 100644 --- a/doc/aorai/Makefile +++ b/doc/aorai/Makefile @@ -8,7 +8,7 @@ EXAMPLES=example.c example.ltl example.ya \ example_loop2.c example_loop2.ya \ README -BNF=basic_ya.bnf extended_ya.bnf +BNF=ya_file.bnf basic_ya.bnf extended_ya.bnf ya_variables.bnf all: main.pdf $(ARCHIVENAME).tgz diff --git a/doc/aorai/main.tex b/doc/aorai/main.tex index 85c46c98adfde48955bbbde37718555a928377b5..237b8c8235e278e013c9af5db91dcd1250b15b35 100644 --- a/doc/aorai/main.tex +++ b/doc/aorai/main.tex @@ -14,7 +14,7 @@ \definecolor{gris}{rgb}{0.95,0.95,0.95} \definecolor{GrisClair}{rgb}{0.98,0.98,0.98} \usepackage[leftbars]{changebar} - +\usepackage{courier} \input{macros} %\setboolean{extension}{true} @@ -36,12 +36,16 @@ } \lstdefinelanguage{ya}{ - alsoletter={\\,\%}, - morekeywords={CALL,RETURN,COR,return,true,false,transitions,\\result}, + alsoletter={\\,\%,\$}, + morekeywords={CALL,RETURN,COR,return,true,false,transitions,\\result,other}, keywordsprefix={\%}, } -\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL} +\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL,ya} +\lstset{ +basicstyle=\ttfamily, +keywordstyle=\bfseries, +} \title{\aorai\ Plugin Tutorial\\\textit{\normalsize (A.k.a. LTL to ACSL)}} \author{Nicolas Stouls and Virgile Prevosto\\ @@ -332,35 +336,27 @@ For compatibility reasons, other syntaxes, like LTL or PROMELA, are supported. \section{YA} \label{sec:ya} +\lstset{language=ya} \subsection{YA file}\label{sec:ya-file} -The description of the automaton can be done in more than one way, but we -recommend to follow the guidelines explained below: -\begin{itemize} -\item Initial states of automaton are specified using the -\emph{\%init} keyword followed by a comma-separated list -containing the states' name: -\begin{lstlisting}[language=ya] -%init: S1, S2, ..., Sn; -\end{lstlisting} -\item Acceptance states are specified using the \emph{\%accept} keyword -followed by a comma separated list containing the states' name -\begin{lstlisting}[language=ya] -%accept: S1, S2, ..., Sn; -\end{lstlisting} -\begin{new} -\item Reject states are specified using the \emph{\%reject} keyword, -followed by a comma separated list containing the states' name -\begin{lstlisting}[language=ya] -%reject: S1, S2, ..., Sn; -\end{lstlisting} -\end{new} -\item If the automaton is supposed to be deterministic, this can be - specified using the following directive: -\begin{lstlisting}[language=ya] -%deterministic; -\end{lstlisting} +A YA file follows the grammar described in Fig.~\ref{ya-file}. +\begin{figure}[htb] +\input{ya_file.tex} +\caption{Structure of a YA file}\label{ya-file} +\end{figure} +The directives specify the initial and accepting state(s). There must be at +least one initial state (exactly one if the automaton is supposed to be +deterministic. All initial and accepting state must appear in the list of +states afterwards. + +A state is simply described by its name and the list of transitions +starting from this state with their guard. The specific \lstinline|other| +guard indicates that this transition is taken if none of the other ones +can be taken. If it appears, it must be last in the list of transitions. + +Conditions that can occur in guards are described in the next section. + \begin{new} -\item By default, \aorai considers that all functions calls and returns trigger +By default, \aorai considers that all functions calls and returns trigger a transition of the automaton. In order to have transitions only for the functions that explicitly appear in the description of the automaton, the following directive must be used: @@ -368,26 +364,6 @@ following directive must be used: %explicit transitions; \end{lstlisting} \end{new} -\item States and transitions are described by sets of the following form -\begin{lstlisting}[language=ya] - state: { condition_1 } -> new_state_1 - | { condition_2 } -> new_state_2 - | { condition_n } -> new_state_n - ; -\end{lstlisting} -A condition which is always true can be omitted along with its surrounding -braces: -\begin{lstlisting} - state: -> new_state; -\end{lstlisting} -In addition, the last transition can have the following form: -\begin{lstlisting} - state: ... - other -> new_state -\end{lstlisting} -indicating that this transition is crossed if and only if none of the -preceding transitions is activated. -\end{itemize} \subsection{Basic YA guards}\label{sec:basic-ya-guards} The syntax for basic YA conditions is described in @@ -491,7 +467,7 @@ most common patterns: \item \lstinline|{,e}| is equivalent to \lstinline|{0,e}| \end{itemize} -Note that a repetition modifier that allows to have a non-fixed number of +Note that a repetition modifier that allows a non-fixed number of repetitions prevents the automaton to be \lstinline|%deterministic|. \lstinline|id(seq)| indicates that we have a \lstinline|CALL(id)| event, @@ -531,36 +507,72 @@ S0: { main::bhv() } -> Sf Sf: -> Sf; \end{lstlisting} -\begin{new} -\subsubsection{Sharing values} +\subsubsection{YA variables} Extended guards do not allow to specify relations between the parameters of -distinct, non-nested calls. For instance, we cannot specify that a call to -\texttt{fopen(f)} must be followed by a call to \texttt{fclose(f)} with the same -\texttt{f} in both cases. In order to do that, it is possible to parameterize -the description of the automaton by directives of the following form: -\begin{lstlisting}[language=ya] -%parameter: decl; -\end{lstlisting} -where \texttt{decl} is an ACSL declaration. The parameter declared that way will -be treated as an existentially-quantified variable across the automaton. -For instance, in order to check whether a call to \texttt{fopen} is always -matched by a call to \texttt{fclose}, we can use the following automaton: +distinct, non-nested calls. In order to be more flexible, it is possible to declare +variables in a Ya file, to assign them values when crossing a transition, and to use +them in guards. The syntax for that is described in Fig.~\ref{fig:ya-variables}. +\begin{figure}[htb] +\input{ya_variables.tex} +\caption{Syntax for declaring and using YA variables} +\label{fig:ya-variables} +\end{figure} + +Only \lstinline|char|, \lstinline|int|, \lstinline|long| variables are currently +supported. Furthermore, variables can only be introduced in deterministic automata, +which do not use extended guards. + +A variable \lstinline|$x| %$ +must have been declared in the directives of the file to be used in a guard. Furthermore +if it is used in a transition starting from state \lstinline|S|, then all possible paths +from the initial state to \lstinline|S| must contain at least one assignment to \lstinline|$x|. +Note that assignments are performed sequentially, so that if +\lstinline|$x| has already been assigned in a given sequence of actions, it can automatically +be used in subsequent assignments (on the other hand, since conditions are evaluated +before actions, it must have been initialized elsewhere if it were to be used in the +condition part of the guard. + +in the right hand side of an action, it is possible to refer to the value of a formal +parameter of \lstinline|f| when the transition is triggered over a \lstinline|CALL| +to \lstinline|f| and to its return value when hangling a \lstinline|RETURN| event, +as described in section~\ref{sec:basic-ya-guards} for conditions. + +An example of YA automaton with variables is given below. It uses variables \lstinline|$x| and +\lstinline|$y| that are updated when calling \lstinline|f| and returning from \lstinline|i|, +while \lstinline|$x| is used when calling \lstinline|h|.%$ \begin{lstlisting}[language=ya] -%init: S0; -%accept: Sf; -%reject: S1; -%parameter: FILE* f; -%explicit transitions; +%init: a; +%accept: i; +%deterministic; -S0: { fopen(){\result==f}; } -> S1; - | -> S0; +$x : int; +$y : int; -S1: { fclose{stream==f}(); } -> Sf +a : { CALL(main) } -> b; -Sf: -> Sf +b : + { CALL(f) } $x:=f().x; $y := $x; -> c +| { CALL(g) } -> d +; + +c : { RETURN(f) } -> e; + +d : { RETURN(g) } -> g; + +e : + { CALL(h) && $x > 0 } -> f +| { RETURN(main) } -> i +; + +f : { RETURN(h) } -> g; + +g : { CALL(i) } -> h; + +h : { RETURN(i) } $y := 0; $x := 1; -> e; + +i : -> i; \end{lstlisting} -\end{new} \section{LTL} \label{sec:ltl} @@ -1225,6 +1237,11 @@ The plug-in is composed of three parts: \section{Recent updates} +\subsection{Frama-C Titanium} +\begin{itemize} +\item Various bug fixes +\item Introduction of YA variables +\end{itemize} \subsection{Frama-C Aluminium} \begin{itemize} \item Generated functions now have a body in addition to a specification diff --git a/doc/aorai/transf.mll b/doc/aorai/transf.mll index 475b11df4f16554aa2b58e396ea391aa2295a336..b063bc1459d07b1f8894465de6deb1f73a17ec2d 100644 --- a/doc/aorai/transf.mll +++ b/doc/aorai/transf.mll @@ -17,9 +17,10 @@ let make_keyword () = let keyword = Buffer.contents full_kw in + let sep = if String.contains keyword '$' then '|' else '$' in print_string "\\addspace"; Printf.printf - "\\lstinline$%s$" keyword; + "\\lstinline%c%s%c" sep keyword sep; print_string "\\spacetrue"; Buffer.clear full_kw } diff --git a/doc/aorai/ya_file.bnf b/doc/aorai/ya_file.bnf new file mode 100644 index 0000000000000000000000000000000000000000..fccc7ad491d8998b546912be74f24e51799979d9 --- /dev/null +++ b/doc/aorai/ya_file.bnf @@ -0,0 +1,16 @@ +\begin{syntax} +file ::= directive* state+; +\\ +directive ::= '%init' ':' id+ ';'; name of initial state(s) + | '%accept' ':' id+ ';'; name of accepting state(s) + | '%deterministic' ';' ; deterministic automaton +\\ +state ::= id ':' transition; + ('|' transition)* ';'; state name and transitions from state +\\ +transition ::= guard '->' id; guard and end state of the transition + | '->' id; transition that is always taken + | 'other' '->' id; default transition. must appear last +\\ +guard ::= '{' condition '}' +\end{syntax} diff --git a/doc/aorai/ya_variables.bnf b/doc/aorai/ya_variables.bnf new file mode 100644 index 0000000000000000000000000000000000000000..866fa127a0deb1230e807243b1de70d1f1b4bcfc --- /dev/null +++ b/doc/aorai/ya_variables.bnf @@ -0,0 +1,11 @@ +\begin{syntax} +directive ::= ... | '$' id ':' type +\\ +type::= 'char' | 'int' | 'long' +\\ +guard ::= '{' condition '}' action* +\\ +action ::= '$' id ':=' lval ';' +\\ +lval ::= ... | '$'id +\end{syntax} diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 27b6beac5547cd0d203f912d37adb9724f172e37..4ea8648e40dc63301f34c82cb47896ec507e368a 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -714,6 +714,10 @@ src/plugins/aorai/VERSIONS.txt: .ignore src/plugins/aorai/YA.README: .ignore src/plugins/aorai/aorai_dataflow.ml: AORAI_LGPL src/plugins/aorai/aorai_dataflow.mli: AORAI_LGPL +src/plugins/aorai/aorai_graph.ml: AORAI_LGPL +src/plugins/aorai/aorai_graph.mli: AORAI_LGPL +src/plugins/aorai/aorai_metavariables.ml: AORAI_LGPL +src/plugins/aorai/aorai_metavariables.mli: AORAI_LGPL src/plugins/aorai/aorai_option.ml: AORAI_LGPL src/plugins/aorai/aorai_option.mli: AORAI_LGPL src/plugins/aorai/aorai_register.ml: AORAI_LGPL diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml index 3c439cfe907832f4290811a298fe5d90488ab46a..c86c90d612ac304fa9e99da7332fc533e5da9009 100644 --- a/src/kernel_internals/parsing/errorloc.ml +++ b/src/kernel_internals/parsing/errorloc.ml @@ -191,12 +191,12 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos = with _ -> close_in_noerr in_ch with _ -> () -let pretty_pos fmt pos = +let pp_pos fmt pos = if pos = Cil_datatype.Position.unknown then Format.fprintf fmt "<unknown>" else Format.fprintf fmt "%d:%d" pos.Filepath.pos_lnum (pos.Filepath.pos_cnum - pos.Filepath.pos_bol) -let pretty_pos_between fmt (pos_start, pos_end) = +let pp_location fmt (pos_start, pos_end) = if pos_start.Filepath.pos_path = pos_end.Filepath.pos_path then if pos_start.Filepath.pos_lnum = pos_end.Filepath.pos_lnum then (* single file, single line *) @@ -210,7 +210,7 @@ let pretty_pos_between fmt (pos_start, pos_end) = pos_start.Filepath.pos_lnum pos_end.Filepath.pos_lnum else (* multiple files (very rare) *) Format.fprintf fmt "Location: between %a and %a" - pretty_pos pos_start pretty_pos pos_end + pp_pos pos_start pp_pos pos_end let parse_error ?(source=Cil_datatype.Position.of_lexing_pos (Lexing.lexeme_start_p !current.lexbuf)) msg = let start_pos = try Some (Parsing.symbol_start_pos ()) with | _ -> None in @@ -239,7 +239,7 @@ let parse_error ?(source=Cil_datatype.Position.of_lexing_pos (Lexing.lexeme_star Kernel.feedback ~source:start_pos "%s:@." str ~append:(fun fmt -> Format.fprintf fmt "%a%a\n" - pretty_pos_between (start_pos, source) + pp_location (start_pos, source) pretty_token (Lexing.lexeme !current.lexbuf); Format.fprintf fmt "%a@." (pp_context_from_file ~start_line:start_pos.Filepath.pos_lnum ~ctx:2) source); diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli index 3722a65a22283a23f9bdacc79837ba15c2ecea30..0089c29d902db394d3eb49a57e1080a95625782e 100644 --- a/src/kernel_internals/parsing/errorloc.mli +++ b/src/kernel_internals/parsing/errorloc.mli @@ -73,6 +73,10 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and val pp_context_from_file: ?ctx:int -> ?start_line:int -> Format.formatter -> Filepath.position -> unit +(** prints a readable description of a location + @since Frama-C+dev *) +val pp_location: Format.formatter -> Cil_types.location -> unit + (** Parse errors are usually fatal, but their reporting is sometimes delayed until the end of the current parsing phase. Functions that intend to ultimately fail should call {!clear_errors} when they diff --git a/src/plugins/aorai/.gitignore b/src/plugins/aorai/.gitignore index 4a6e0c9805a7e9c317398b3867de0527f647999b..dbc3d247b6627099a25ed2b34608c057d6120bfe 100644 --- a/src/plugins/aorai/.gitignore +++ b/src/plugins/aorai/.gitignore @@ -16,4 +16,5 @@ /ptests_local_config.ml /tests/*/result /tests/test_config_prove -/tests/*/result_prove \ No newline at end of file +/tests/*/result_prove +/top \ No newline at end of file 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..0662bf5764d7444a1214427368a085dc296b5dbe 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 @@ -276,8 +276,7 @@ let make_start_transition ?(is_main=false) kf init_states = let my_trans = Path_analysis.get_transitions_of_state state auto in let treat_one_trans acc trans = if is_crossable trans kf then begin - let (_,action) = trans.cross in - let bindings = actions_to_range action in + let bindings = actions_to_range trans.actions in let fst_set = Data_for_aorai.Aorai_state.Set.singleton trans.stop in @@ -303,14 +302,13 @@ 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 let treat_one_trans acc trans = if Aorai_utils.isCrossable trans kf Promelaast.Return then begin - let (_,action) = trans.cross in - let my_bindings = actions_to_range action in + let my_bindings = actions_to_range trans.actions in let new_bindings = compose_actions bindings (last, last, my_bindings) in add_or_merge trans.stop new_bindings acc end else acc @@ -624,7 +622,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 +831,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..6f957dd83458f358f0927363a17e853b328e084e --- /dev/null +++ b/src/plugins/aorai/aorai_graph.ml @@ -0,0 +1,70 @@ +(**************************************************************************) +(* *) +(* This file is part of Aorai plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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 = Promelaast.typed_trans + +module Vertex = +struct + type t = state + let compare x y = Stdlib.compare x.nums y.nums + let hash x = Hashtbl.hash 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 = Stdlib.compare x.numt y.numt + let default = { + numt = -1; start = Vertex.default; stop = Vertex.default; + cross = TTrue; actions = [] + } +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..8735c3cc1e7e89a420359612647f33a25d589f95 --- /dev/null +++ b/src/plugins/aorai/aorai_graph.mli @@ -0,0 +1,41 @@ +(**************************************************************************) +(* *) +(* This file is part of Aorai plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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_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..2692a1658d3b28745a43c09b89bd225610c76e13 --- /dev/null +++ b/src/plugins/aorai/aorai_metavariables.ml @@ -0,0 +1,161 @@ +(**************************************************************************) +(* *) +(* This file is part of Aorai plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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 = Aorai_option.register_category "check-metavar" + + +module VarSet = Cil_datatype.Varinfo.Set + +let pretty_set fmt set = + let l = VarSet.elements set in + Pretty_utils.pp_list ~sep:", " Cil_printer.pp_varinfo fmt l + +let pretty_state fmt st = + Format.pp_print_string fmt st.Promelaast.name + +let pretty_trans fmt tr = + Format.fprintf fmt "from %a to %a:@\n{ @[%a@] } %a" + pretty_state tr.start + pretty_state tr.stop + Promelaoutput.Typed.print_condition tr.cross + Promelaoutput.Typed.print_actionl tr.actions + + +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 + + type data = Bottom | InitializedSet of VarSet.t + + let top = InitializedSet VarSet.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 -> VarSet.equal s1 s2 + + let join d1 d2 = + match d1, d2 with + | Bottom, d | d, Bottom -> d + | InitializedSet s1, InitializedSet s2 -> + InitializedSet (VarSet.inter s1 s2) + + let _pretty_data fmt = function + | Bottom -> Format.printf "Bottom" + | InitializedSet set -> pretty_set fmt set + + let check tr used initialized = + let diff = VarSet.diff used initialized in + if not (VarSet.is_empty diff) then + Aorai_option.abort + "The metavariables %a may not be initialized before the transition %a" + pretty_set diff + pretty_trans tr + + let term_mvars t = + let result = ref VarSet.empty in + 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 := VarSet.add vi !result; + Cil.SkipChildren + | _ -> Cil.SkipChildren + end in + ignore (Visitor.visitFramacTerm v t); + !result + + let rec cond_mvars = function + | TAnd (c1,c2) | TOr (c1,c2) -> VarSet.union (cond_mvars c1) (cond_mvars c2) + | TNot (c) -> cond_mvars c + | TRel (_,t1,t2) -> VarSet.union (term_mvars t1) (term_mvars t2) + | TCall _ | TReturn _ | TTrue | TFalse -> VarSet.empty + + let analyze (_,tr,_) = function + | Bottom -> Bottom + | InitializedSet initialized -> + (* Check that the condition uses only initialized variables *) + check tr (cond_mvars tr.cross) (initialized); + (* Add initialized variables and check the right hand side *) + let add initialized = function + | Copy_value ((TVar({lv_origin = Some vi}),_),t) -> + check tr (term_mvars t) initialized; + VarSet.add vi initialized + | _ -> initialized + in + let initialized' = List.fold_left add initialized tr.actions in + Aorai_option.debug ~dkey "%a {%a} -> %a {%a}" + pretty_state tr.start pretty_set initialized + pretty_state tr.stop 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 _ -> Cil_datatype.Varinfo.equal vi) 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 + () + +let checkSingleAssignment auto = + let check_action tr assigned = function + | Copy_value ((TVar({lv_origin = Some vi}),_),_) -> + if VarSet.mem vi assigned then + Aorai_option.abort + "The metavariable %a is assigned several times during the \ + transition %a" + Cil_printer.pp_varinfo vi + pretty_trans tr; + VarSet.add vi assigned + | _ -> assigned + in + let check_trans tr = + ignore (List.fold_left (check_action tr) VarSet.empty tr.actions) + in + List.iter check_trans auto.trans diff --git a/src/plugins/aorai/aorai_metavariables.mli b/src/plugins/aorai/aorai_metavariables.mli new file mode 100644 index 0000000000000000000000000000000000000000..47c4a7a22bacdb49b1d1486d97ccc86f299ab2cc --- /dev/null +++ b/src/plugins/aorai/aorai_metavariables.mli @@ -0,0 +1,28 @@ +(**************************************************************************) +(* *) +(* This file is part of Aorai plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + +val checkInitialization : Promelaast.typed_automaton -> unit + +val checkSingleAssignment : Promelaast.typed_automaton -> unit diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml index 664f3289886e08fbe4ea271b3460dbfd5f3ba63f..14c35b7f0e6b8b37975985009e4fa2e4282c4d41 100644 --- a/src/plugins/aorai/aorai_register.ml +++ b/src/plugins/aorai/aorai_register.ml @@ -50,13 +50,13 @@ let convert_ltl_exprs t = | PNot c -> PNot (convert_cond c) | PCall _ | PReturn _ | PTrue | PFalse -> cond | PRel(Neq,PVar x,PCst _) -> - (try + (try let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2) with Not_found -> cond) | PRel _ -> cond in let rec convert_seq_elt e = - { e with + { e with condition = Extlib.opt_map convert_cond e.condition; nested = convert_seq e.nested; } and convert_seq s = List.map convert_seq_elt s in @@ -97,22 +97,45 @@ let ltl_to_ltlLight f_ltl (f_out : Filepath.Normalized.t) = with | Ltllexer.Error (loc,msg) -> syntax_error loc msg -let load_ya_file f = +let parse_error' lexbuf msg = + let open Lexing in + let start_p = Cil_datatype.Position.of_lexing_pos (lexeme_start_p lexbuf) + and end_p = Cil_datatype.Position.of_lexing_pos (lexeme_end_p lexbuf) + and lexeme = Lexing.lexeme lexbuf in + let start_line = start_p.Filepath.pos_lnum in + let abort str = + Aorai_option.feedback ~source:start_p "%s@.%a, before or at token: %s\n%a@." + str + Errorloc.pp_location (start_p, end_p) + lexeme + (Errorloc.pp_context_from_file ~start_line ~ctx:2) start_p; + raise (Log.AbortError "aorai") + in + Pretty_utils.ksfprintf abort msg + +let load_ya_file filename = + let channel = check_and_open_in filename "invalid Ya file" in + let lexbuf = Lexing.from_channel channel in + Lexing.(lexbuf.lex_curr_p <- + { lexbuf.lex_curr_p with pos_fname = (filename :> string) }); try - let c = check_and_open_in f "invalid Ya file" in - let automata = Yalexer.parse c in - close_in c; - Data_for_aorai.setAutomata automata; + let automata = Yaparser.main Yalexer.token lexbuf in + close_in channel; + Data_for_aorai.setAutomata automata with - | Yalexer.Error (loc,msg) -> syntax_error loc msg + | Parsing.Parse_error | Invalid_argument _ -> + parse_error' lexbuf "syntax error" + | Yalexer.Lexing_error msg -> + parse_error' lexbuf "%s" msg + 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 @@ -236,7 +259,7 @@ let output () = (* Dot file *) if (Aorai_option.Dot.get()) then begin - Promelaoutput.output_dot_automata (Data_for_aorai.getAutomata ()) + Promelaoutput.Typed.output_dot_automata (Data_for_aorai.getAutomata ()) (!dot_file:>string); printverb "Generating dot file : done\n" end; @@ -255,7 +278,7 @@ let output () = printverb "C file generation : done\n"; ) () end; - + printverb "Finished.\n"; (* Some test traces. *) Data_for_aorai.debug_computed_state (); @@ -302,7 +325,7 @@ let work () = let root = fst (Globals.entry_point ()) in if (Aorai_option.Axiomatization.get()) then begin - (* Step 5 : incrementing pre/post + (* Step 5 : incrementing pre/post conditions with states and transitions information *) printverb "Refining pre/post : \n"; Aorai_dataflow.compute (); @@ -339,7 +362,7 @@ let work () = (* Step 4': Computing the set of possible pre-states and post-states of each function *) (* And so for pre/post transitions *) printverb "Abstracting pre/post : skipped\n"; - + (* Step 5': incrementing pre/post conditions with states and transitions information *) printverb "Refining pre/post : skipped\n"; @@ -353,7 +376,7 @@ let work () = Aorai_visitors.add_sync_with_buch file; printverb "Annotation of Cil : partial\n" end; - + (* Step 8 : clearing tables whose information has been invalidated by our transformations. *) diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml index 453d6c4381e193fd796a073b4493ed9c8d83c45a..d73cb2c8b83e9d923e51c5a610aa32de6095c8aa 100644 --- a/src/plugins/aorai/aorai_utils.ml +++ b/src/plugins/aorai/aorai_utils.ml @@ -66,8 +66,7 @@ let isCrossable tr func st = | TFalse -> False | TRel _ -> Undefined in - let cond,_ = tr.cross in - let res = isCross cond <> False in + let res = isCross tr.cross <> False in Aorai_option.debug ~level:2 "Function %a %s-state, \ transition %s -> %s is%s possible" Kernel_function.pretty func (if st=Call then "pre" else "post") @@ -307,8 +306,7 @@ let isCrossableAtInit tr func = | TRel(rel,t1,t2) -> eval_rel_at_init rel t1 t2 in - let (cond,_) = tr.cross in - match isCross cond with + match isCross tr.cross with | Bool3.True | Bool3.Undefined -> true | Bool3.False -> false @@ -557,7 +555,7 @@ let mk_behavior_call generated_kf kf bhv = (* Translate the cross condition of an automaton edge to an expression. Used in mk_stmt. This might generate calls to auxiliary functions, to take into account a guard that uses a function behavior. *) -let crosscond_to_exp generated_kf curr_f curr_status loc (cond,_) res = +let crosscond_to_exp generated_kf curr_f curr_status loc cond res = let check_current_event f status = Kernel_function.equal curr_f f && curr_status = status in @@ -837,12 +835,14 @@ let is_state_pred state = (Req,one_term(), Logic_const.tvar (Data_for_aorai.get_state_logic_var state)) -let is_state_stmt (state,copy) loc = - if Aorai_option.Deterministic.get () - then - mkStmtOneInstr - ~ghost:true (Set (Cil.var copy, int2enumstate_exp loc state.nums, loc)) - else mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc)) +let is_state_non_det_stmt (_,copy) loc = + mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc)) + +let is_state_det_stmt state loc = + let var = Data_for_aorai.get_varinfo curState in + mkStmtOneInstr + ~ghost:true (Set (Cil.var var, int2enumstate_exp loc state.nums, loc)) + let is_state_exp state loc = if Aorai_option.Deterministic.get () @@ -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 = @@ -1059,10 +1059,10 @@ let mk_deterministic_lemma () = let subst = Cil_datatype.Logic_var.Hashtbl.create 5 in let subst_res = Kernel_function.Hashtbl.create 5 in let guard1 = - pred_of_condition subst subst_res label (fst trans1.cross) + pred_of_condition subst subst_res label trans1.cross in let guard2 = - pred_of_condition subst subst_res label (fst trans2.cross) + pred_of_condition subst subst_res label trans2.cross in let pred = Logic_const.pnot (Logic_const.pand (guard1, guard2)) in let quants = @@ -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,6 +1165,13 @@ 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) auto.metavariables; + if Aorai_option.Deterministic.get () then begin (* must flush now previous globals which are used in the lemmas in order to be able to put these last ones in the right places in the AST. *) @@ -1203,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 @@ -1281,7 +1288,7 @@ let action_assigns trans = add_if_needed caux (Logic_const.tvar aux) empty | _ -> empty in - let _,res = List.fold_left treat_one_action empty_pebble (snd trans.cross) in + let _,res = List.fold_left treat_one_action empty_pebble trans.actions in Writes res let get_reachable_trans state st auto current_state = @@ -1327,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). @@ -1347,7 +1354,7 @@ let force_transition loc f st current_state = *) let add_one_trans (has_crossable_trans, crossable_non_reject) trans = let has_crossable_trans = - Logic_simplification.tor has_crossable_trans (fst trans.cross) + Logic_simplification.tor has_crossable_trans trans.cross in let crossable_non_reject = crossable_non_reject || @@ -1421,7 +1428,7 @@ let partition_action trans = *) in let treat_one_trans acc tr = - List.fold_left (treat_one_action tr.start) acc (snd tr.cross) + List.fold_left (treat_one_action tr.start) acc tr.actions in List.fold_left treat_one_trans Cil_datatype.Term_lval.Map.empty trans @@ -1450,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 @@ -1523,7 +1530,8 @@ let add_behavior_pebble_actions ~loc f st behaviors state trans = let set = Data_for_aorai.pebble_set_at set Logic_const.here_label in let treat_action guard res action = match action with - | Copy_value _ | Counter_incr _ | Counter_init _ -> res + | Copy_value _ | Counter_incr _ | Counter_init _ -> + res | Pebble_init (_,_,v) -> let a = Cil_const.make_logic_var_quant aux.lv_name aux.lv_type in let guard = rename_pred aux a guard in @@ -1551,9 +1559,9 @@ let add_behavior_pebble_actions ~loc f st behaviors state trans = :: res in let treat_one_trans acc tr = - let guard = crosscond_to_pred (fst tr.cross) f st in + let guard = crosscond_to_pred tr.cross f st in let guard = Logic_const.pold guard in - List.fold_left (treat_action guard) acc (snd tr.cross) + List.fold_left (treat_action guard) acc tr.actions in let res = List.fold_left treat_one_trans [] trans in let res = Logic_const.term (Tunion res) set.term_type in @@ -1562,14 +1570,50 @@ let add_behavior_pebble_actions ~loc f st behaviors state trans = in Cil.mk_behavior ~name ~assumes ~post_cond () :: behaviors -let mk_action ~loc a = +(* NB: we assume that the terms coming from YA automata keep quite simple. + Notably that they do not introduce themselves any \at. *) +let make_old loc init t = + let vis = + object(self) + inherit Visitor.frama_c_inplace + val is_old = Stack.create () + method private is_old = + if Stack.is_empty is_old then false else Stack.top is_old + method! vterm t = + match t.term_node with + | TLval lv -> + if Cil_datatype.Term_lval.Set.mem lv init then begin + if self#is_old then begin + Stack.push false is_old; + DoChildrenPost + (fun t -> + ignore (Stack.pop is_old); + Logic_const.(tat ~loc (t,here_label))) + end else DoChildren + end + else begin + if not self#is_old then begin + Stack.push true is_old; + DoChildrenPost + (fun t -> + ignore (Stack.pop is_old); + Logic_const.told ~loc t) + end else DoChildren + end + | _ -> DoChildren + end + in Visitor.visitFramacTerm vis t + +let mk_action ~loc init a = let term_lval lv = Logic_const.term ~loc (TLval lv) (Cil.typeOfTermLval lv) in + let add_lv lv = Cil_datatype.Term_lval.Set.add lv init in match a with | Counter_init lv -> [Logic_const.prel ~loc - (Req, term_lval lv, Logic_const.tinteger ~loc 1)] + (Req, term_lval lv, Logic_const.tinteger ~loc 1)], + add_lv lv | Counter_incr lv -> [Logic_const.prel ~loc (Req, term_lval lv, @@ -1577,11 +1621,13 @@ let mk_action ~loc a = (TBinOp (PlusA, Logic_const.told ~loc (term_lval lv), Logic_const.tinteger ~loc 1)) - (Cil.typeOfTermLval lv))] - | Pebble_init _ | Pebble_move _ -> [] (* Treated elsewhere *) + (Cil.typeOfTermLval lv))], + add_lv lv + | Pebble_init _ | Pebble_move _ -> [],init (* Treated elsewhere *) | Copy_value (lv,t) -> [Logic_const.prel ~loc - (Req, term_lval lv, Logic_const.told t)] + (Req, term_lval lv, make_old loc init t)], + add_lv lv let is_reachable state status = let treat_one_state _ map = Data_for_aorai.Aorai_state.Map.mem state map in @@ -1621,28 +1667,59 @@ let get_accessible_transitions auto state status = Data_for_aorai.Aorai_state.Set.fold (fun s acc -> Path_analysis.get_edges s state auto @ acc) previous_set [] +let get_aux_var_bhv_name = function + | TVar v, _ -> + Data_for_aorai.get_fresh (v.lv_name ^ "_unchanged") + | lv -> + Aorai_option.fatal "unexpected lval for action variable: %a" + Printer.pp_term_lval lv + (* Assumes that we don't have a multi-state here. pebbles are handled elsewhere *) -let mk_unchanged_aux_vars trans = - let my_aux_vars = Cil_datatype.Term_lval.Set.empty in - let add_one_action acc = function - | Counter_init lv | Counter_incr lv | Copy_value (lv,_) -> - Cil_datatype.Term_lval.Set.add lv acc - | Pebble_init _ | Pebble_move _ -> acc +let mk_unchanged_aux_vars_bhvs loc f st status = + let (states,_ as auto) = Data_for_aorai.getGraph() in + let add_state_trans acc state = + let trans = get_reachable_trans state st auto status in + List.rev_append trans acc in - let add_one_trans acc tr = - let (_,actions) = tr.cross in - List.fold_left add_one_action acc actions + let crossable_trans = + List.fold_left add_state_trans [] states in - let my_aux_vars = List.fold_left add_one_trans my_aux_vars trans in - let treat_lval lv acc = + let add_trans_aux_var trans map = function + | Counter_init lv | Counter_incr lv | Copy_value (lv,_) -> + let other_trans = + match Cil_datatype.Term_lval.Map.find_opt lv map with + | Some l -> l + | None -> [] + in + Cil_datatype.Term_lval.Map.add lv (trans :: other_trans) map + | Pebble_init _ | Pebble_move _ -> map + in + let add_trans_aux_vars map trans = + List.fold_left (add_trans_aux_var trans) map trans.actions + in + let possible_actions = + List.fold_left add_trans_aux_vars + Cil_datatype.Term_lval.Map.empty + crossable_trans + in + let out_trans trans = + Logic_const.new_predicate + (Logic_const.por ~loc + (is_out_of_state_pred trans.start, + Logic_const.pnot (crosscond_to_pred trans.cross f st))) + in + let mk_behavior lv trans acc = + let name = get_aux_var_bhv_name lv in + let assumes = List.map out_trans trans in let t = Data_for_aorai.tlval lv in let ot = Logic_const.told t in let p = Logic_const.prel (Req,t,ot) in - (Normal, Logic_const.new_predicate p) :: acc + let post_cond = [Normal, Logic_const.new_predicate p] in + Cil.mk_behavior ~name ~assumes ~post_cond () :: acc in - Cil_datatype.Term_lval.Set.fold treat_lval my_aux_vars [] + Cil_datatype.Term_lval.Map.fold mk_behavior possible_actions [] let mk_behavior ~loc auto kf e status state = Aorai_option.debug "analysis of state %s (%d)" @@ -1665,15 +1742,14 @@ let mk_behavior ~loc auto kf e status state = List.fold_left (fun (in_guard, out_guard, all_assigns, action_bhvs) trans -> Aorai_option.debug "examining transition %d" trans.numt; - let (cond,actions) = trans.cross in Aorai_option.debug "transition %d is active" trans.numt; - let guard = crosscond_to_pred cond kf e in + let guard = crosscond_to_pred trans.cross kf e in let my_in_guard,my_out_guard = match state.multi_state with | None -> guard, Logic_const.pnot ~loc guard | Some (_,aux) -> let set = - find_pebble_origin Logic_const.here_label actions + find_pebble_origin Logic_const.here_label trans.actions in pebble_guard ~loc set aux guard, pebble_guard_neg ~loc set aux guard @@ -1682,7 +1758,7 @@ let mk_behavior ~loc auto kf e status state = Logic_const.pand ~loc (out_guard, my_out_guard) in let in_guard, all_assigns, action_bhvs = - match actions with + match trans.actions with | [] -> (Logic_const.por ~loc (in_guard,my_in_guard), all_assigns, @@ -1702,30 +1778,34 @@ let mk_behavior ~loc auto kf e status state = Normal, Logic_const.new_predicate (is_state_pred state) in - let treat_one_action acc a = - let posts = mk_action ~loc a in + let treat_one_action (other_posts, init) a = + let posts, init = mk_action ~loc init a in match state.multi_state with | None -> - acc @ + other_posts @ List.map (fun x -> (Normal, Logic_const.new_predicate x)) - posts + posts, + init | Some (_,aux) -> let set = find_pebble_origin - Logic_const.pre_label actions + Logic_const.pre_label trans.actions in - acc @ + other_posts @ List.map (fun x -> (Normal, Logic_const.new_predicate (pebble_post ~loc set aux x))) - posts + posts, + init in - let post_cond = - List.fold_left treat_one_action [post_cond] actions + let post_cond,_ = + List.fold_left treat_one_action + ([post_cond], Cil_datatype.Term_lval.Set.empty) + trans.actions in let assigns = action_assigns trans in let all_assigns = concat_assigns assigns all_assigns in @@ -1773,7 +1853,7 @@ let mk_behavior ~loc auto kf e status state = else begin let post_cond = match state.multi_state with - | None -> mk_unchanged_aux_vars my_trans + | None -> [] (* Done elsewhere *) | Some (set,_) -> let set = Data_for_aorai.pebble_set_at set Logic_const.here_label @@ -1828,7 +1908,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 = @@ -1868,11 +1948,14 @@ let auto_func_behaviors loc f st state = let global_behavior = Cil.mk_behavior ~requires ~post_cond ~assigns () in + let non_action_behaviors = + mk_unchanged_aux_vars_bhvs loc f st state + in (* Keep behaviors ordered according to the states they describe *) - global_behavior :: (List.rev behaviors) + global_behavior :: (List.rev_append behaviors non_action_behaviors) -let act_convert loc (_,act) res = +let act_convert loc act res = let treat_one_act = function | Counter_init t_lval -> @@ -1897,173 +1980,173 @@ let act_convert loc (_,act) res = in List.map treat_one_act act -let copy_stmt s = - let vis = new Visitor.frama_c_refresh (Project.current()) in - Visitor.visitFramacStmt vis s +let mk_transitions_stmt generated_kf loc f st res trans = + List.fold_right + (fun trans + (aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) -> + let (tr_stmts, tr_vars, tr_funcs, exp) = + crosscond_to_exp generated_kf f st loc trans.cross res + in + let cond = Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp in + (tr_stmts @ aux_stmts, + tr_vars @ aux_vars, + Cil_datatype.Varinfo.Set.union tr_funcs new_funcs, + Cil.mkBinOp loc LOr exp_from_trans cond, + (Cil.copy_exp cond, act_convert loc trans.actions res) + :: stmt_from_action)) + trans + ([],[],Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc, []) + +let mkIfStmt loc exp1 block1 block2 = + Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc)) + +let mk_deterministic_stmt + generated_kf loc auto f fst status ret state + (other_stmts, other_funcs, other_vars, trans_stmts as res) = + if is_reachable state status then begin + let trans = get_accessible_transitions auto state status in + let aux_stmts, aux_vars, aux_funcs, _, stmt_from_action = + mk_transitions_stmt generated_kf loc f fst ret trans + in + let stmts = + List.fold_left + (fun acc (cond, stmt_act) -> + [mkIfStmt loc cond + (mkBlock (is_state_det_stmt state loc :: stmt_act)) + (mkBlock acc)]) + trans_stmts + (List.rev stmt_from_action) + in + aux_stmts @ other_stmts, + Cil_datatype.Varinfo.Set.union aux_funcs other_funcs, + aux_vars @ other_vars, + stmts + end else res -(* mk_stmt loc (states, tr) f fst status state +(* mk_non_deterministic_stmt loc (states, tr) f fst status state Generates the statement updating the variable representing the state argument. If state is reachable, generates a "If then else" statement, else it is just an assignment. Used in auto_func_block. *) -let mk_stmt generated_kf loc (states, tr) f fst status ((st,_) as state) res = +let mk_non_deterministic_stmt + generated_kf loc (states, tr) f fst status ((st,_) as state) res = if is_reachable st status then begin let useful_trans = get_accessible_transitions (states,tr) st status in - let aux_stmts, new_vars, new_funcs, exp_from_trans,stmt_from_action = - List.fold_right - (fun trans - (aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) -> - let (tr_stmts, tr_vars, tr_funcs, exp) = - crosscond_to_exp generated_kf f fst loc trans.cross res - in - (tr_stmts @ aux_stmts, - tr_vars @ aux_vars, - Cil_datatype.Varinfo.Set.union tr_funcs new_funcs, - Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp - ::exp_from_trans, - act_convert loc trans.cross res :: stmt_from_action)) - useful_trans - ([],[],Cil_datatype.Varinfo.Set.empty, [], []) - in - let mkIfStmt exp1 block1 block2 = - Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc)) - in - let if_cond = - List.fold_left - (fun acc exp -> Cil.mkBinOp loc LOr exp acc) - (List.hd exp_from_trans) - (List.tl exp_from_trans) - in - let then_stmt = is_state_stmt state loc in - let else_stmt = - if Aorai_option.Deterministic.get () then [] - else [is_out_of_state_stmt state loc] + let aux_stmts, new_vars, new_funcs, cond,stmt_from_action = + mk_transitions_stmt generated_kf loc f fst res useful_trans in + let then_stmt = is_state_non_det_stmt state loc in + let else_stmt = [is_out_of_state_stmt state loc] in let trans_stmts = - if Aorai_option.Deterministic.get () then - List.fold_left2 - (fun acc cond stmt_act -> - [mkIfStmt cond - (mkBlock (copy_stmt then_stmt :: stmt_act)) (mkBlock acc)]) - else_stmt - (List.rev exp_from_trans) + let actions = + List.fold_left + (fun acc (cond, stmt_act) -> + if stmt_act = [] then acc + else + (mkIfStmt loc cond (mkBlock stmt_act) (mkBlock []))::acc) + [] (List.rev stmt_from_action) - else - let actions = - List.fold_left2 - (fun acc cond stmt_act -> - if stmt_act = [] then acc - else - (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc) - [] - (List.rev exp_from_trans) - (List.rev stmt_from_action) - in - mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions + in + mkIfStmt loc cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions in new_funcs, new_vars, aux_stmts @ trans_stmts end else - if Aorai_option.Deterministic.get () then - Cil_datatype.Varinfo.Set.empty, [], [] - else Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc] + Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc] -let auto_func_block generated_kf loc f st status res = - let dkey = func_body_dkey in - let call_or_ret = - match st with - | Promelaast.Call -> "call" - | Promelaast.Return -> "return" +let equalsStmt lval exp loc = (* assignment *) + Cil.mkStmtOneInstr ~ghost:true (Set (lval, exp, loc)) + +let mk_deterministic_body generated_kf loc f st status res = + let (states, _ as auto) = Data_for_aorai.getGraph() in + let aux_stmts, aux_funcs, aux_vars, trans_stmts = + List.fold_right + (mk_deterministic_stmt generated_kf loc auto f st status res) + states + ([], Cil_datatype.Varinfo.Set.empty, [],[]) 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 + aux_funcs, aux_vars, aux_stmts @ trans_stmts +let mk_non_deterministic_body generated_kf loc f st status res = (* For the following tests, we need a copy of every state. *) - + let (states, _) as auto = Data_for_aorai.getGraph() in let copies, local_var = - if Aorai_option.Deterministic.get () then begin - let orig = Data_for_aorai.get_varinfo curState in - let copy = Cil.copyVarinfo orig (orig.vname ^ "_tmp") in - copy.vglob <- false; - List.map (fun st -> (st, copy)) states, [copy] - end else begin - let bindings = - List.map - (fun st -> - let state_var = Data_for_aorai.get_state_var st in - let copy = Cil.copyVarinfo state_var (state_var.vname ^ "_tmp") in - copy.vglob <- false; - (st,copy)) - states - in bindings, snd (List.split bindings) - end - in - let equalsStmt lval exp = (* assignment *) - Cil.mkStmtOneInstr ~ghost:true (Set (lval, exp, loc)) - in - let stmt_begin_list = - - [ - (* First statement : what is the current status : called or return ? *) - equalsStmt - (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus)) (* current status... *) - (Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))); (* ... equals to what it is *) - - (* Second statement : what is the current operation, i.e. which function ? *) - equalsStmt - (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp)) (* current operation ... *) - (Cil.new_exp loc (Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f)))) (* ...equals to what it is *) - ] - + let bindings = + List.map + (fun st -> + let state_var = Data_for_aorai.get_state_var st in + let copy = Cil.copyVarinfo state_var (state_var.vname ^ "_tmp") in + copy.vglob <- false; + (st,copy)) + states + in bindings, snd (List.split bindings) in - - (* As we work on copies, they need to be set to their actual values *) - let copies_update = - if Aorai_option.Deterministic.get () then - let orig = Data_for_aorai.get_varinfo curState in - [ equalsStmt (Cil.var (List.hd local_var)) (Cil.evar ~loc orig) ] - else - List.map - (fun (st,copy) -> - equalsStmt (Cil.var copy) - (Cil.evar ~loc (Data_for_aorai.get_state_var st))) - copies + List.map + (fun (st,copy) -> + equalsStmt (Cil.var copy) + (Cil.evar ~loc (Data_for_aorai.get_state_var st)) loc) + copies in - (* For each state, we have to generate the statement that will update its copy. *) let new_funcs, local_var, main_stmt = - List.fold_left (fun (new_funcs, aux_vars, stmts) state -> let my_funcs, my_vars, my_stmts = - mk_stmt generated_kf loc auto f st status state res + mk_non_deterministic_stmt generated_kf loc auto f st status state res in Cil_datatype.Varinfo.Set.union my_funcs new_funcs, my_vars @ aux_vars, my_stmts@stmts ) (Cil_datatype.Varinfo.Set.empty, local_var, []) copies - in (* Finally, we replace the state var values by the ones computed in copies. *) let stvar_update = - if Aorai_option.Deterministic.get () then - let orig = Data_for_aorai.get_varinfo curState in - [ equalsStmt (Cil.var orig) (Cil.evar (List.hd local_var))] + List.map + (fun (state,copy) -> + equalsStmt + (Cil.var (Data_for_aorai.get_state_var state)) + (Cil.evar ~loc copy) loc) + copies + in + new_funcs, local_var, copies_update @ main_stmt @ stvar_update + +let auto_func_block generated_kf loc f st status res = + let dkey = func_body_dkey in + let call_or_ret = + match st with + | Promelaast.Call -> "call" + | Promelaast.Return -> "return" + in + Aorai_option.debug + ~dkey "func code for %a (%s)" Kernel_function.pretty f call_or_ret; + + let stmt_begin_list = + [ + (* First statement : what is the current status : called or return ? *) + equalsStmt + (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus)) + (Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))) loc; + (* Second statement : what is the current operation, + i.e. which function ? *) + equalsStmt + (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp)) + (Cil.new_exp loc + (Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f)))) + loc + ] + in + let new_funcs, local_var, main_stmt = + if Aorai_option.Deterministic.get() then + mk_deterministic_body generated_kf loc f st status res else - List.map - (fun (state,copy) -> - equalsStmt - (Cil.var (Data_for_aorai.get_state_var state)) - (Cil.evar ~loc copy)) - copies + mk_non_deterministic_body generated_kf loc f st status res in let ret = [ Cil.mkStmt ~ghost:true (Cil_types.Return(None,loc)) ] in let res_block = (Cil.mkBlock - ( stmt_begin_list @ copies_update @ main_stmt @ stvar_update @ ret)) + ( stmt_begin_list @ main_stmt @ ret)) in res_block.blocals <- local_var; Aorai_option.debug ~dkey "Generated body is:@\n%a" @@ -2071,8 +2154,8 @@ 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 treat_one_trans acc tr = Logic_simplification.tor acc (fst tr.cross) in + let auto = Data_for_aorai.getGraph () in + let treat_one_trans acc tr = Logic_simplification.tor acc tr.cross in let find_trans state prev tr = Path_analysis.get_edges prev state auto @ tr in diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli index 47d4bb47275c2334d1afee6bc16bf632a8c57a0f..efb8b12df79c276e22688cf01d55f06fe5e1e61a 100644 --- a/src/plugins/aorai/aorai_utils.mli +++ b/src/plugins/aorai/aorai_utils.mli @@ -32,12 +32,12 @@ open Promelaast *) val isCrossable: - (typed_condition * action) trans -> kernel_function -> funcStatus -> bool + typed_trans -> kernel_function -> funcStatus -> bool (** Given a transition and the main entry point it returns if the cross condition can be satisfied at the beginning of the program. *) val isCrossableAtInit: - (typed_condition * action) trans -> kernel_function -> bool + typed_trans -> kernel_function -> bool (** This function rewrites a cross condition into an ACSL expression. Moreover, by giving current operation name and its status (call or @@ -71,9 +71,6 @@ val host_state_term: unit -> Cil_types.term_lval corresponding state. *) val is_state_pred: state -> predicate -(** Returns the statement saying the state is affected *) -val is_state_stmt: state * Cil_types.varinfo -> location -> Cil_types.stmt - (** Returns the boolean expression saying the state is affected *) val is_state_exp: state -> location -> Cil_types.exp diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml index a0d12c2dc3e0d065997f9da436a1133bfefce998..486c67733edde58a8bbc4e091943759426a9b1f5 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,24 +371,24 @@ 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 - (cond, Aorai_utils.crosscond_to_pred (fst tr.cross) kf Promelaast.Call) + (cond, Aorai_utils.crosscond_to_pred tr.cross kf Promelaast.Call) in let cond = List.fold_left treat_one_trans Logic_const.pfalse trans in 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 @@ -409,7 +409,7 @@ let neg_trans kf trans = List.fold_left (fun cond tr -> Logic_simplification.tand - cond (Logic_simplification.tnot (fst tr.cross))) + cond (Logic_simplification.tnot tr.cross)) cond trans) TTrue same_start in @@ -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 1bcaa67755f6727b12a02562f4759ac52095f220..6e0dfa5f60a001cb26d5cb642899ee6b1894384d 100644 --- a/src/plugins/aorai/data_for_aorai.ml +++ b/src/plugins/aorai/data_for_aorai.ml @@ -57,19 +57,18 @@ module Aorai_typed_trans = Datatype.Make_with_collections( struct let name = "Aorai_typed_trans" - type t = - (Promelaast.typed_condition * Promelaast.action) Promelaast.trans + type t = Promelaast.typed_trans let structural_descr = Structural_descr.t_abstract let reprs = [ { numt = -1; start = List.hd (Aorai_state.reprs); stop = List.hd (Aorai_state.reprs); - cross = (TTrue,[]); } ] + cross = TTrue; actions=[]; } ] let equal x y = Datatype.Int.equal x.numt y.numt let hash x = x.numt let rehash = Datatype.identity let compare x y = Datatype.Int.compare x.numt y.numt let copy = Datatype.identity let internal_pretty_code = Datatype.undefined - let pretty = Promelaoutput.print_transition + let pretty = Promelaoutput.Typed.print_transition let varname _ = assert false let mem_project = Datatype.never_any_project end) @@ -133,8 +132,10 @@ let rec is_same_expression e1 e2 = | 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 (f1,x1), PPrm(f2,x2) -> f1 = f2 && x1 = 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 @@ -158,7 +159,7 @@ let get_logic name = let declared_predicates = Hashtbl.create 97 -let add_predicate name pred_info = +let add_predicate name pred_info = Hashtbl.replace declared_predicates name pred_info let get_predicate name = @@ -205,7 +206,7 @@ let buch_sync = "Aorai_Sync" (* Deprecated ? *) (* ************************************************************************* *) (* Buchi automata as stored after parsing *) -let automata = ref ([],[]) +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) [[]]) @@ -218,13 +219,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 @@ -341,11 +353,11 @@ let new_state name = let new_intermediate_state () = new_state "aorai_intermediate_state" -let new_trans start stop cond = - { start = start; stop = stop; cross = cond; numt = TransIndex.next () } +let new_trans start stop cross actions = + { start; stop; cross; actions; 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 @@ -354,7 +366,7 @@ let check_states s = states; List.iter (fun x -> - try + try let y = List.find (fun y -> x.nums = y.nums && not (x==y)) states in Aorai_option.fatal "%s: State %s and %s share same id %d" s x.name y.name x.nums @@ -397,25 +409,23 @@ let is_single elt = the entire automaton is processed by adding direct transitions from the starting state to the children of the end state. *) -type eps_trans = - Normal of typed_condition * action - | Epsilon of typed_condition * action - -let print_epsilon_trans fmt = function - | Normal (c,a) -> - Format.fprintf fmt "%a%a" - Promelaoutput.print_condition c - Promelaoutput.print_action a - | Epsilon (c,a) -> - Format.fprintf fmt "epsilon-trans:@\n%a%a" - Promelaoutput.print_condition c - Promelaoutput.print_action a +type 'a eps = Normal of 'a | Epsilon of 'a + +let print_eps f fmt = function + | Normal x -> f fmt x + | Epsilon x -> Format.fprintf fmt "epsilon-trans:@\n%a" f x + +let print_eps_trans fmt tr = + Format.fprintf fmt "%s -> %s:@[%a%a@]" + tr.start.name tr.stop.name + (print_eps Promelaoutput.Typed.print_condition) tr.cross + Promelaoutput.Typed.print_actionl tr.actions type current_event = | ECall of kernel_function * Cil_types.logic_var Cil_datatype.Varinfo.Hashtbl.t - * eps_trans Promelaast.trans + * (typed_condition eps,typed_action) Promelaast.trans | EReturn of kernel_function | ECOR of kernel_function | ENone (* None found yet *) @@ -481,11 +491,11 @@ let add_current_event event env cond = let merge_current_event env1 env2 cond1 cond2 = assert (List.tl env1 == List.tl env2); let old_env = List.tl env2 in - match (List.hd env1, List.hd env2) with + 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 + when Kernel_function.equal kf1 kf2 -> env2, 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 -> @@ -540,11 +550,11 @@ let memo_aux_variable tr counter used_prms vi = let my_lvar = Cil.cvar_to_lvar my_var in Cil_datatype.Varinfo.Hashtbl.add used_prms vi my_lvar; (match tr.cross with - | Normal (cond,action) -> + | Normal _ -> let st = Extlib.opt_map (fun _ -> tr.stop) counter in let loc = get_bindings st my_lvar in let copy = Copy_value (loc,Logic_const.tvar (Cil.cvar_to_lvar vi)) in - tr.cross <- Normal(cond,copy::action) + tr.actions <- copy :: tr.actions | Epsilon _ -> Aorai_option.fatal "Epsilon transition used as Call event" ); @@ -568,6 +578,13 @@ let check_one top info counter s = Some (Logic_const.term (TLval (TResult rt,TNoOffset)) (Ctype rt)) | ECOR _ | EReturn _ | EMulti | ENone -> None + +let find_metavar s metaenv = + try + 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 with @@ -682,14 +699,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 + | PVar s -> + let var = find_in_env env current s 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 @@ -869,13 +889,13 @@ 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 | 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 @@ -885,13 +905,15 @@ let type_cond needs_pebble env tr cond = | POr(c1,c2) -> let env1, c1 = aux pos env c1 in let env2, c2 = aux pos env c2 in - merge_current_event env1 env2 c1 c2 + let env, c = merge_current_event env1 env2 c1 c2 in + env, c | PAnd(c1,c2) -> let env, c1 = aux pos env c1 in let env, c2 = aux pos env c2 in - env, TAnd(c1,c2) + env, TAnd (c1,c2) | PNot c -> - let env, c = aux (not pos) env c in env, TNot c + let env, c = aux (not pos) env c in + env, TNot c | PCall (s,b) -> let kf = try Globals.Functions.find_by_name s @@ -908,18 +930,24 @@ let type_cond needs_pebble env tr cond = b in if pos then - add_current_event + let env, c = add_current_event (ECall (kf, Cil_datatype.Varinfo.Hashtbl.create 3, tr)) env (TCall (kf,b)) - else env, TCall (kf,b) + in + env, c + else + env, TCall (kf,b) | PReturn s -> let kf = try Globals.Functions.find_by_name s with Not_found -> Aorai_option.abort "No such function %s" s in - if pos then add_current_event (EReturn kf) env (TReturn kf) - else env, TReturn kf + if pos then + let env,c = add_current_event (EReturn kf) env (TReturn kf) in + env, c + else + env, TReturn kf in aux true (ENone::env) cond @@ -941,7 +969,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. *) @@ -989,12 +1017,12 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = | _ -> new_intermediate_state () in Aorai_option.debug "Examining single elt:@\n%s -> %s:@[%a@]" - curr_start.name my_end.name Promelaoutput.print_seq_elt elt; + curr_start.name my_end.name Promelaoutput.Parsed.print_seq_elt elt; let guard_exit_loop env current counter = 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) @@ -1009,7 +1037,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 @@ -1023,16 +1051,18 @@ 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 [] -> my_end | _ -> new_intermediate_state () in - let trans_start = new_trans curr_start seq_start (Normal (TTrue,[])) + let trans_start = new_trans curr_start seq_start (Normal TTrue) [] + in + let inner_env, cond = + type_cond needs_pebble metaenv env trans_start cond in - let inner_env, cond = type_cond needs_pebble env trans_start cond in let (env,states, seq_transitions, seq_end) = match elt.nested with | [] -> inner_env, [], [], my_end @@ -1040,15 +1070,15 @@ 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 let states = add_if_needed states curr_start in let transitions = trans_start :: seq_transitions in (match trans_start.cross with - | Normal (conds,action) -> - trans_start.cross <- Normal(tand cond conds,action) + | Normal conds -> + trans_start.cross <- Normal (tand cond conds) | Epsilon _ -> Aorai_option.fatal "Transition guard translated as epsilon transition"); @@ -1058,7 +1088,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = (env, states, transitions, curr_start, seq_end) | EReturn kf1 :: ECall (kf2,_,_) :: tl when Kernel_function.equal kf1 kf2 -> - (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 @@ -1066,20 +1096,20 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = in a non-empty context in particular) *) (env, states, transitions, curr_start, seq_end) - | EMulti :: env -> - (env, states, transitions, curr_start, seq_end)) + | EMulti :: env_tmp -> + 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 let auto = (inner_states,inner_trans) in if at_most_one then begin (* Just adds an epsilon transition from start to end *) - let opt = new_trans curr_start oth_start (Epsilon (TTrue,[])) in + let opt = new_trans curr_start oth_start (Epsilon TTrue) [] in env, states, opt::trans, curr_start, curr_end end else if has_loop then begin @@ -1117,19 +1147,12 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = List.fold_left (fun acc tr -> let init_action = Counter_init (make_counter tr.stop) in - let init_cross = - match tr.cross with - | Normal (cond, actions) -> - Normal(cond, init_action :: actions) - | Epsilon(cond, actions) -> - Epsilon(cond, init_action :: actions) - in - Aorai_option.debug "New init trans %s -> %s: %a" - st.name tr.stop.name - print_epsilon_trans init_cross; + let init_actions = init_action :: tr.actions in let init_trans = - new_trans st tr.stop init_cross + new_trans st tr.stop tr.cross init_actions in + Aorai_option.debug "New init trans %a" + print_eps_trans init_trans; if at_most_one then init_trans :: acc else begin let st = @@ -1141,24 +1164,22 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = (make_counter_term curr_start) else TTrue in - let loop_action = - if needs_counter then begin + let loop_actions = + if needs_counter then let counter = make_counter curr_start in - [ Counter_incr counter ] - end else [] + Counter_incr counter :: tr.actions + else tr.actions in let loop_cross = match tr.cross with - | Normal(cond, actions) -> - Normal(tand loop_cond cond, loop_action @ actions) - | Epsilon(cond, actions) -> - Epsilon(tand loop_cond cond, loop_action @ actions) + | Normal cond -> Normal (tand loop_cond cond) + | Epsilon cond -> Epsilon (tand loop_cond cond) in - Aorai_option.debug "New loop trans %s -> %s: %a" - inner_end.name tr.stop.name - print_epsilon_trans loop_cross; let loop_trans = - new_trans inner_end tr.stop loop_cross in + new_trans inner_end tr.stop loop_cross loop_actions + in + Aorai_option.debug "New loop trans %a" + print_eps_trans loop_trans; init_trans :: loop_trans :: acc end) oth_trans trans @@ -1174,11 +1195,11 @@ 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 - let no_seq = new_trans st oth_start (Epsilon (zero_cond,[])) in + let no_seq = new_trans st oth_start (Epsilon zero_cond) [] in no_seq :: loop_trans end else loop_trans in @@ -1194,11 +1215,10 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = guard_exit_loop env st (make_counter_term curr_end) else TTrue in - let min_cond = Epsilon (min_cond,[]) in - Aorai_option.debug "New exit trans %s -> %s: %a" - inner_end.name oth_start.name - print_epsilon_trans min_cond; - let exit_trans = new_trans inner_end oth_start min_cond in + let min_cond = Epsilon min_cond in + let exit_trans = new_trans inner_end oth_start min_cond [] in + Aorai_option.debug "New exit trans %a" + print_eps_trans exit_trans; let trans = exit_trans :: trans @ oth_trans in states, trans end else begin @@ -1214,7 +1234,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = List.fold_left (fun acc tr -> match tr.cross with - | Normal (cond,_) | Epsilon (cond,_) -> + | Normal cond | Epsilon cond -> let cond = change_bound_var tr.stop st cond in tor acc cond) TFalse trans @@ -1226,7 +1246,7 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = | _ -> let reject = get_reject_state () in let states = add_if_needed states reject in - let trans = new_trans st reject (Normal(cond,[])) :: trans + let trans = new_trans st reject (Normal cond) [] :: trans in states, trans @ oth_trans ) end @@ -1242,6 +1262,13 @@ let rec type_seq default_state tr env needs_pebble curr_start curr_end seq = end else env, states, trans, curr_start, curr_end +let type_action metaenv env = function +| Metavar_assign (s, e) -> + let vi = find_metavar s metaenv in + let _, e, _ = type_expr metaenv env e in + (* TODO: check type assignability *) + Copy_value ((TVar (Cil.cvar_to_lvar vi), TNoOffset), e) + let single_path (states,transitions as auto) tr = Aorai_option.Deterministic.get () || (let init = Path_analysis.get_init_states auto in @@ -1258,7 +1285,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 @@ -1269,15 +1296,26 @@ let type_trans auto env tr = in Aorai_option.debug "Analyzing transition %s -> %s: %a (needs pebble: %B)" - tr.start.name tr.stop.name Promelaoutput.print_parsed tr.cross needs_pebble; + tr.start.name tr.stop.name + Promelaoutput.Parsed.print_guard + tr.cross needs_pebble; match tr.cross with | Seq seq -> 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 + let env,states, transitions,_,_ = + type_seq has_default_state tr metaenv env needs_pebble tr.start tr.stop seq + in + (* Insert metavariable assignments for transitions to tr.stop *) + let meta_actions = List.map (type_action metaenv env) tr.actions in + let add_meta_actions t = + if Aorai_state.equal t.stop tr.stop then + { t with actions = t.actions @ meta_actions } + else + t in - let (states, transitions) = + let transitions = List.map add_meta_actions transitions in + let transitions = if List.exists (fun st -> st.multi_state <> None) states then begin (* We have introduced some multi-state somewhere, we have to introduce pebbles and propagate them from state to state. *) @@ -1292,26 +1330,25 @@ let type_trans auto env tr = (fun trans -> match trans.cross with | Epsilon _ -> trans - | Normal(cond,actions) -> + | Normal _ -> let (dest,d_aux) = memo_multi_state tr.stop in let actions = if tr.start.nums <> start.nums then begin let src,s_aux = memo_multi_state tr.start in - Pebble_move(dest,d_aux,src,s_aux) :: actions + Pebble_move(dest,d_aux,src,s_aux) :: trans.actions end else begin let v = Cil.cvar_to_lvar count in let incr = Counter_incr (TVar v, TNoOffset) in let init = Pebble_init (dest, d_aux, v) in - init::incr::actions + init::incr::trans.actions end in - { trans with - cross = Normal(cond, actions) }) + { trans with actions }) transitions in - states, transitions + transitions end else - states, transitions + transitions in (* For each intermediate state, add a transition to either the default state or a rejection state (in which we will @@ -1326,8 +1363,8 @@ let type_trans auto env tr = in Aorai_option.debug "Resulting transitions:@\n%a" (Pretty_utils.pp_list ~sep:"@\n" - (fun fmt tr -> Format.fprintf fmt "%s -> %s:@[%a@]" - tr.start.name tr.stop.name print_epsilon_trans tr.cross)) + (fun fmt tr -> Format.fprintf fmt "%a" + print_eps_trans tr)) transitions; states, transitions, needs_default | Otherwise -> [],[], false (* treated directly by type_seq *) @@ -1340,8 +1377,7 @@ let add_reject_trans auto intermediate_states = let cond = List.fold_left (fun acc tr -> - let cond,_ = tr.cross in - let cond = change_bound_var tr.stop st cond in + let cond = change_bound_var tr.stop st tr.cross in tor cond acc) TFalse my_trans in @@ -1351,35 +1387,38 @@ let add_reject_trans auto intermediate_states = | _ -> Aorai_option.debug "Adding default transition %s -> %s: %a" - st.name reject_state.name Promelaoutput.print_condition cond; - states, new_trans st reject_state (cond,[]) :: trans + st.name reject_state.name Promelaoutput.Typed.print_condition cond; + states, new_trans st reject_state cond [] :: trans in List.fold_left treat_one_state auto intermediate_states let propagate_epsilon_transitions (states, _ as auto) = - let rec transitive_closure start (conds,actions) known_states curr = + let rec transitive_closure start conds actions known_states curr = let known_states = curr :: known_states in let trans = Path_analysis.get_transitions_of_state curr auto in List.fold_left (fun acc tr -> match tr.cross with - | Epsilon (cond,my_actions) -> + | Epsilon cond -> Aorai_option.debug "Treating epsilon trans %s -> %s" curr.name tr.stop.name; if List.exists (fun st -> st.nums = tr.stop.nums) known_states then acc else transitive_closure - start (tand cond conds, my_actions @ actions) + start (tand cond conds) (tr.actions @ actions) known_states tr.stop @ acc - | Normal (cond, action) -> + | Normal cond -> Aorai_option.debug "Adding transition %s -> %s from epsilon trans" start.name tr.stop.name; - new_trans start tr.stop (tand cond conds,action @ actions) ::acc) + let tr = + new_trans start tr.stop (tand cond conds) (tr.actions @ actions) + in + tr :: acc) [] trans in let treat_one_state acc st = - acc @ transitive_closure st (TTrue,[]) [] st + acc @ transitive_closure st TTrue [] [] st in let trans = List.fold_left treat_one_state [] states in (states, trans) @@ -1393,51 +1432,50 @@ let add_default_trans (states, transitions as auto) otherwise = let cond = List.fold_left (fun acc c -> - let (cond,_) = c.cross in + let cond = c.cross in Aorai_option.debug "considering trans %s -> %s: %a" - c.start.name c.stop.name Promelaoutput.print_condition cond; + c.start.name c.stop.name Promelaoutput.Typed.print_condition cond; let neg = tnot cond in Aorai_option.debug "negation: %a" - Promelaoutput.print_condition neg; + Promelaoutput.Typed.print_condition neg; Aorai_option.debug "acc: %a" - Promelaoutput.print_condition acc; + Promelaoutput.Typed.print_condition acc; let res = tand acc (tnot cond) in Aorai_option.debug "partial result: %a" - Promelaoutput.print_condition res; + Promelaoutput.Typed.print_condition res; res ) TTrue my_trans in Aorai_option.debug "resulting transition: %a" - Promelaoutput.print_condition cond; + Promelaoutput.Typed.print_condition cond; let cond,_ = Logic_simplification.simplifyCond cond in - let new_trans = new_trans st tr.stop (cond,[]) in + let new_trans = new_trans st tr.stop cond [] in new_trans::acc in 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 [] tr in + 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 "Resulting transitions:@\n%a@\nEnd of transitions" - (Pretty_utils.pp_list ~sep:"@\n" - (fun fmt tr -> - Format.fprintf fmt "%s -> %s: %a" - tr.start.name tr.stop.name print_epsilon_trans tr.cross)) - trans; + (Pretty_utils.pp_list ~sep:"@\n" print_eps_trans) trans; let add_reject = if needs_reject then - (List.filter - (fun x -> not (Aorai_state.equal tr.start x || + (List.filter + (fun x -> not (Aorai_state.equal tr.start x || Aorai_state.equal tr.stop x)) intermediate_states) @ add_reject else add_reject @@ -1447,7 +1485,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 @@ -1456,23 +1494,23 @@ 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) + | 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"; + Promelaoutput.Typed.output_dot_automata auto "aorai_debug_typed.dot"; let (_,trans) = List.fold_left (fun (i,l as acc) t -> - let cond, action = t.cross in - let cond = fst (Logic_simplification.simplifyCond cond) + let cond = fst (Logic_simplification.simplifyCond t.cross) in match cond with TFalse -> acc - | _ -> (i+1,{ t with cross = (cond,action); numt = i } :: l)) - (0,[]) transitions + | _ -> (i+1,{ t with cross = cond; numt = i } :: l)) + (0,[]) trans in let _, states = List.fold_left @@ -1487,29 +1525,52 @@ 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 } + + +(* Check Metavariable compatibility *) +let checkMetavariableCompatibility auto = + let is_extended_trans trans = + match trans.cross with + | Otherwise -> false + | Seq [ elt ] -> + elt.nested <> [] || not (is_single elt) + | Seq _ -> true + in + let has_metavariables = not (Datatype.String.Map.is_empty auto.metavariables) + and deterministic = Aorai_option.Deterministic.get () + and uses_extended_guards = List.exists is_extended_trans auto.trans in + if has_metavariables && (not deterministic || uses_extended_guards) then + Aorai_option.abort + "The use of metavariables is incompatible with non-deterministic \ + automata, such as automa using extended transitions." + (** Stores the buchi automaton and its variables and functions as it is returned by the parsing *) let setAutomata auto = + checkMetavariableCompatibility 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"; + Promelaoutput.Typed.output_dot_automata auto "aorai_debug_reduced.dot"; if (Array.length !cond_of_parametrizedTransitions) < (getNumberOfTransitions ()) then (* all transitions have a true parameterized guard, i.e. [[]] *) cond_of_parametrizedTransitions := - Array.make (getNumberOfTransitions ()) [[]] + Array.make (getNumberOfTransitions ()) [[]] ; + Aorai_metavariables.checkInitialization auto ; + Aorai_metavariables.checkSingleAssignment 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 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 () = @@ -1776,14 +1837,14 @@ let merge_bindings tbl1 tbl2 = | None, None -> None | Some tbl, None | None, Some tbl -> Some - (Cil_datatype.Term.Map.merge + (Cil_datatype.Term.Map.merge (merge_range loc) tbl (unchanged loc)) | Some tbl1, Some tbl2 -> Some (Cil_datatype.Term.Map.merge (merge_range loc) tbl1 tbl2) in Cil_datatype.Term.Map.merge merge_vals tbl1 tbl2 -module End_state = +module End_state = Aorai_state.Map.Make(Datatype.Triple(Aorai_state.Set)(Aorai_state.Set)(Vals)) type end_state = End_state.t @@ -1805,7 +1866,7 @@ let pretty_end_state start fmt tbl = start.Promelaast.name stop.Promelaast.name; Aorai_state.Set.iter (fun state -> - Format.fprintf fmt " %s -> %s@\n" + Format.fprintf fmt " %s -> %s@\n" start.Promelaast.name state.Promelaast.name) fst; @@ -1850,7 +1911,7 @@ let included_state tbl1 tbl2 = Cil_datatype.Term.Map.iter (fun loc range1 -> let range2 = Cil_datatype.Term.Map.find loc bindings2 in - if not + if not (included_range range1 range2) then raise Not_found) bindings1) tbl1) @@ -1860,7 +1921,7 @@ let included_state tbl1 tbl2 = with Not_found -> false let merge_end_state tbl1 tbl2 = - let merge_stop_state _ (fst1, last1, tbl1) (fst2, last2, tbl2) = + let merge_stop_state _ (fst1, last1, tbl1) (fst2, last2, tbl2) = let fst = Aorai_state.Set.union fst1 fst2 in let last = Aorai_state.Set.union last1 last2 in let tbl = merge_bindings tbl1 tbl2 in @@ -1872,12 +1933,12 @@ let merge_state tbl1 tbl2 = let merge_state _ = merge_end_state in Aorai_state.Map.merge (Extlib.merge_opt merge_state) tbl1 tbl2 -module Pre_state = +module Pre_state = Kernel_function.Make_Table (Case_state) (struct let name = "Data_for_aorai.Pre_state" - let dependencies = + let dependencies = [ Ast.self; Aorai_option.Ya.self; Aorai_option.Ltl_File.self; Aorai_option.To_Buchi.self; Aorai_option.Deterministic.self ] let size = 17 @@ -1890,7 +1951,7 @@ let set_kf_init_state kf state = let dkey = Aorai_option.register_category "dataflow" -let replace_kf_init_state kf state = +let replace_kf_init_state kf state = Aorai_option.debug ~dkey "Replacing pre-state of %a:@\n @[%a@]" Kernel_function.pretty kf pretty_state state; @@ -1901,12 +1962,12 @@ let get_kf_init_state kf = Pre_state.find kf with Not_found -> Aorai_state.Map.empty -module Post_state = +module Post_state = Kernel_function.Make_Table (Case_state) (struct let name = "Data_for_aorai.Post_state" - let dependencies = + let dependencies = [ Ast.self; Aorai_option.Ya.self; Aorai_option.Ltl_File.self; Aorai_option.To_Buchi.self; Aorai_option.Deterministic.self ] let size = 17 @@ -1973,26 +2034,26 @@ let get_loop_invariant_state stmt = let pretty_pre_state fmt = Pre_state.iter - (fun kf state -> + (fun kf state -> Format.fprintf fmt "Function %a:@\n @[%a@]@\n" Kernel_function.pretty kf pretty_state state) let pretty_post_state fmt = Post_state.iter - (fun kf state -> + (fun kf state -> Format.fprintf fmt "Function %a:@\n @[%a@]@\n" Kernel_function.pretty kf pretty_state state) let pretty_loop_init fmt = Loop_init_state.iter - (fun stmt state -> + (fun stmt state -> let kf = Kernel_function.find_englobing_kf stmt in Format.fprintf fmt "Function %a, sid %d:@\n @[%a@]@\n" Kernel_function.pretty kf stmt.sid pretty_state state) let pretty_loop_invariant fmt = Loop_invariant_state.iter - (fun stmt state -> + (fun stmt state -> let kf = Kernel_function.find_englobing_kf stmt in Format.fprintf fmt "Function %a, sid %d:@\n @[%a@]@\n" Kernel_function.pretty kf stmt.sid pretty_state state) @@ -2006,18 +2067,19 @@ 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 - (fun state (fst, last, _) set -> - Aorai_state.Set.add state + (fun state (fst, last, _) set -> + Aorai_state.Set.add state (Aorai_state.Set.union last (Aorai_state.Set.union fst set))) map (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 @@ -2026,7 +2088,7 @@ let removeUnusedTransitionsAndStates () = raise Empty_automaton; (* Step 2 : computation of translation tables *) let state_list = - List.sort + List.sort (fun x y -> Datatype.String.compare x.Promelaast.name y.Promelaast.name) (Aorai_state.Set.elements reached_states) in @@ -2046,7 +2108,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 @@ -2056,13 +2118,13 @@ 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 = let rewrite_set set = - Aorai_state.Set.fold - (fun s set -> Aorai_state.Set.add (new_state s) set) + Aorai_state.Set.fold + (fun s set -> Aorai_state.Set.add (new_state s) set) set Aorai_state.Set.empty in let rewrite_bindings (fst_states, last_states, bindings) = @@ -2084,7 +2146,7 @@ let removeUnusedTransitionsAndStates () = in Pre_state.iter (fun kf state -> Pre_state.replace kf (rewrite_state state)); Post_state.iter (fun kf state -> Post_state.replace kf (rewrite_state state)); - Loop_init_state.iter + Loop_init_state.iter (fun s state -> Loop_init_state.replace s (rewrite_state state)); Loop_invariant_state.iter (fun s state -> Loop_invariant_state.replace s (rewrite_state state)) diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli index 5205169d0457f927ddc590ed2df2e13daddadea9..8c7ed586075255f9c356a763d28debfe3859f17b 100644 --- a/src/plugins/aorai/data_for_aorai.mli +++ b/src/plugins/aorai/data_for_aorai.mli @@ -42,10 +42,8 @@ exception Empty_automaton module Aorai_state: Datatype.S_with_collections with type t = Promelaast.state -module Aorai_typed_trans: - Datatype.S_with_collections - with - type t = (Promelaast.typed_condition * Promelaast.action) Promelaast.trans +module Aorai_typed_trans: + Datatype.S_with_collections with type t = Promelaast.typed_trans (** Initializes some tables according to data from Cil AST. *) val setCData : unit -> unit @@ -56,7 +54,6 @@ val add_logic : string -> Cil_types.logic_info -> unit (** *) val get_logic : string -> Cil_types.logic_info - (** *) val add_predicate : string -> Cil_types.logic_info -> unit @@ -202,11 +199,14 @@ val buch_sync : string val new_state: string -> state -val new_trans: state -> state -> 'a -> 'a trans +val new_trans: state -> state -> 'c -> 'a list -> ('c,'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_trans list + (** Type-checks the parsed automaton and stores the result. This might introduce new global variables in case of sequences. *) @@ -247,8 +247,7 @@ val is_reject_state: state -> bool (** returns the transition having the corresponding id. @raise Not_found if this is not the case. *) -val getTransition: - int -> (Promelaast.typed_condition * Promelaast.action) Promelaast.trans +val getTransition: int -> Promelaast.typed_trans (* ************************************************************************* *) (**{b Variables information} Usually it seems very useful to access to varinfo diff --git a/src/plugins/aorai/logic_simplification.ml b/src/plugins/aorai/logic_simplification.ml index 88de692c01cff144bff52fc751bdf38321d14f10..9bf174dd1ae3a3f393116c1cce341f65c56c3a55 100644 --- a/src/plugins/aorai/logic_simplification.ml +++ b/src/plugins/aorai/logic_simplification.ml @@ -28,7 +28,7 @@ open Promelaast let pretty_clause fmt l = Format.fprintf fmt "@[<2>[%a@]]@\n" - (Pretty_utils.pp_list ~sep:",@ " Promelaoutput.print_condition) l + (Pretty_utils.pp_list ~sep:",@ " Promelaoutput.Typed.print_condition) l let pretty_dnf fmt l = Format.fprintf fmt "@[<2>[%a@]]@\n" @@ -360,7 +360,7 @@ let simplClause clause dnf = *) let simplifyCond condition = Aorai_option.debug - "initial condition: %a" Promelaoutput.print_condition condition; + "initial condition: %a" Promelaoutput.Typed.print_condition condition; (* Step 1 : Condition is translate into Disjunctive Normal Form *) let res1 = condToDNF condition in Aorai_option.debug "initial dnf: %a" pretty_dnf res1; @@ -394,14 +394,9 @@ let simplifyTrans transl = let (crossCond , pcond ) = simplifyCond (tr.cross) in (* pcond stands for parametrized condition : disjunction of conjunctions of parametrized call/return *) - let tr'={ start = tr.start ; - stop = tr.stop ; - cross = crossCond ; - numt = tr.numt - } - in + let tr'= { tr with cross = crossCond } in Aorai_option.debug "condition is %a, dnf is %a" - Promelaoutput.print_condition crossCond pretty_dnf pcond; + Promelaoutput.Typed.print_condition crossCond pretty_dnf pcond; if tr'.cross <> TFalse then (tr'::ltr,pcond::lpcond) else (ltr,lpcond) ) ([],[]) @@ -437,7 +432,7 @@ let simplifyDNFwrtCtx dnf kf1 status = in let res = tors (List.map simplCNFwrtCtx dnf) in Aorai_option.debug - "After simplification: %a" Promelaoutput.print_condition res; res + "After simplification: %a" Promelaoutput.Typed.print_condition res; res (* Tests : diff --git a/src/plugins/aorai/logic_simplification.mli b/src/plugins/aorai/logic_simplification.mli index 80956533bb63272234cc8d8270a12cbce83f7f68..6c58727222ed78367613ef7d5c86fc6c43e1ccff 100644 --- a/src/plugins/aorai/logic_simplification.mli +++ b/src/plugins/aorai/logic_simplification.mli @@ -45,8 +45,8 @@ val simplifyCond: simplifyCond done on each cross condition. Uncrossable transition are removed. *) val simplifyTrans: - Promelaast.typed_condition Promelaast.trans list -> - (Promelaast.typed_condition Promelaast.trans list)* + Promelaast.typed_trans list -> + (Promelaast.typed_trans list)* (Promelaast.typed_condition list list list) val dnfToCond : diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.mli index 0e19f53d056b7124405d6d68da4e34612a03b096..fe0bdcfe677bb92ffb947f99580bb7814134e60f 100644 --- a/src/plugins/aorai/promelaast.mli +++ b/src/plugins/aorai/promelaast.mli @@ -23,12 +23,13 @@ (* *) (**************************************************************************) -(** The abstract tree of promela representation. Such tree is used by promela +(** The abstract tree of promela representation. Such tree is used by promela parser/lexer before its translation into Data_for_aorai module. *) type expression = | 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 @@ -43,104 +44,114 @@ type condition = | POr of condition * condition | PAnd of condition * condition | PNot of condition - | PCall of string * string option - (** Call might be done in a given behavior *) + | PCall of string * string option + (** Call might be done in a given behavior *) | PReturn of string -and seq_elt = - { condition: condition option; - nested: sequence; - min_rep: expression option; - max_rep: expression option; - } +and seq_elt = { + condition: condition option; + nested: sequence; + min_rep: expression option; + max_rep: expression option; +} and sequence = seq_elt list (** Promela parsed abstract syntax trees. Either a sequence of event or the - otherwise keyword. A single condition is expressed with a singleton + otherwise keyword. A single condition is expressed with a singleton having an empty nested sequence and min_rep and max_rep being equal to one. *) -type parsed_condition = Seq of sequence | Otherwise +type guard = Seq of sequence | Otherwise + +type action = + | Metavar_assign of string * expression type typed_condition = - | TOr of typed_condition * typed_condition (** Logical OR *) - | TAnd of typed_condition * typed_condition (** Logical AND *) - | TNot of typed_condition (** Logical NOT *) - | TCall of Cil_types.kernel_function * Cil_types.funbehavior option - (** Predicate modelling the call of an operation *) - | TReturn of Cil_types.kernel_function - (** Predicate modelling the return of an operation *) - | TTrue (** Logical constant TRUE *) - | TFalse (** Logical constant FALSE *) - | TRel of Cil_types.relation * Cil_types.term * Cil_types.term - (** Condition. If one of the terms contains TResult, TRel is in - conjunction with exactly one TReturn event, and the TResult is - tied to the corresponding value. - *) - -type single_action = + | TOr of typed_condition * typed_condition (** Logical OR *) + | TAnd of typed_condition * typed_condition (** Logical AND *) + | TNot of typed_condition (** Logical NOT *) + | TCall of Cil_types.kernel_function * Cil_types.funbehavior option + (** Predicate modelling the call of an operation *) + | TReturn of Cil_types.kernel_function + (** Predicate modelling the return of an operation *) + | TTrue (** Logical constant TRUE *) + | TFalse (** Logical constant FALSE *) + | TRel of Cil_types.relation * Cil_types.term * Cil_types.term + (** Condition. If one of the terms contains TResult, TRel is in + conjunction with exactly one TReturn event, and the TResult is + tied to the corresponding value. + *) + +(** Additional actions to perform when crossing a transition. + There is at most one Pebble_* action for each transition, and + each transition leading to a state with multi-state has such an action. +*) +type typed_action = | Counter_init of Cil_types.term_lval | Counter_incr of Cil_types.term_lval | Pebble_init of Cil_types.logic_info * Cil_types.logic_var * Cil_types.logic_var - (** adds a new pebble. [Pebble_init(set,aux,count)] indicates that - pebble [count] is put in [set] whose content is governed by C - variable [aux]. - *) + (** adds a new pebble. [Pebble_init(set,aux,count)] indicates that + pebble [count] is put in [set] whose content is governed by C + variable [aux]. + *) | Pebble_move of - Cil_types.logic_info * - Cil_types.logic_var * Cil_types.logic_info * Cil_types.logic_var - (** [Pebble_move(new_set,new_aux,old_set,old_aux)] - moves pebbles from [old_set] to [new_set], governed by the - corresponding aux variables. *) + Cil_types.logic_info * + Cil_types.logic_var * Cil_types.logic_info * Cil_types.logic_var + (** [Pebble_move(new_set,new_aux,old_set,old_aux)] + moves pebbles from [old_set] to [new_set], governed by the + corresponding aux variables. *) | Copy_value of Cil_types.term_lval * Cil_types.term - (** copy the current value of the given term into the given location - so that it can be accessed by a later state. *) + (** copy the current value of the given term into the given location + so that it can be accessed by a later state. *) -(** Additional actions to perform when crossing a transition. - There is at most one Pebble_* action for each transition, and - each transition leading to a state with multi-state has such an action. - *) -type action = single_action list (** Internal representation of a State from the Buchi automata. *) -type state = - { name : string (** State name *); - mutable acceptation : Bool3.t - (** True iff state is an acceptation state *); - mutable init : Bool3.t (** True iff state is an initial state *); - mutable nums : int; (** Numerical ID of the state *) - mutable multi_state: - (Cil_types.logic_info * Cil_types.logic_var) option - (** Translation of some sequences might lead to some kind of pebble - automaton, where we need to distinguish various branches. This is - done by having a set of pebbles instead of just a zero/one switch - to know if we are in the given state. The guards apply to each - active pebble and are thus of the form - \forall integer x; in(x,multi_state) ==> guard. - multi_state is the first lvar of the pair, x is the second - *) - } +type state = { + name : string; (** State name *) + mutable acceptation : Bool3.t; (** True iff state is an acceptation state *) + mutable init : Bool3.t; (** True iff state is an initial state *) + mutable nums : int; (** Numerical ID of the state *) + mutable multi_state: (Cil_types.logic_info * Cil_types.logic_var) option; + (** Translation of some sequences might lead to some kind of pebble + automaton, where we need to distinguish various branches. This is + done by having a set of pebbles instead of just a zero/one switch + to know if we are in the given state. The guards apply to each + active pebble and are thus of the form + \forall integer x; in(x,multi_state) ==> guard. + multi_state is the first lvar of the pair, x is the second + *) +} (** Internal representation of a transition from the Buchi automata. *) -type 'condition trans = - { start : state ; (** Starting state of the transition *) - stop : state ; (** Ending state of the transition *) - mutable cross : 'condition ; (** Cross condition of the transition *) - mutable numt : int (** Numerical ID of the transition *) - } +type ('c,'a) trans = { + start : state ; (** Starting state of the transition *) + stop : state ; (** Ending state of the transition *) + mutable cross : 'c; (** Cross condition of the transition *) + mutable actions : 'a list; (** Actions to execute while crossing *) + mutable numt : int (** Numerical ID of the transition *) +} + +type parsed_trans = (guard, action) trans + +type typed_trans = (typed_condition, typed_action) trans -(** Internal representation of a Buchi automata : a list of states and a list of transitions.*) -type 'condition automaton = (state list) * ('condition trans list) +(** Internal representation of a Buchi automata : a list of states and a list + of transitions.*) +type ('c,'a) automaton = { + states: state list; + trans: (('c,'a) trans) list; + metavariables: Cil_types.varinfo Datatype.String.Map.t; +} -type parsed_automaton = parsed_condition automaton +type parsed_automaton = (guard, action) automaton -type typed_automaton = (typed_condition * action) automaton +type typed_automaton = (typed_condition, typed_action) automaton (** An operation can have two status: currently calling or returning. *) type funcStatus = - | Call - | Return + | Call + | Return (* Local Variables: diff --git a/src/plugins/aorai/promelaoutput.ml b/src/plugins/aorai/promelaoutput.ml index 60570159c36468af8f37f454528ed043976b4e8a..cac471f43abbc85d4e75ee4aae2233a657a517af 100644 --- a/src/plugins/aorai/promelaoutput.ml +++ b/src/plugins/aorai/promelaoutput.ml @@ -30,152 +30,15 @@ open Promelaast open Bool3 open Format -let string_of_unop = function - | Uminus -> "-" - | Ustar -> "*" - | Uamp -> "&" - | Ubw_not -> "~" - -let rec print_parsed_expression fmt = function - | PVar s -> Format.fprintf fmt "%s" s - | PPrm (f,s) -> Format.fprintf fmt "%s().%s" f 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 - | PCst (WStringConstant s) -> Format.fprintf fmt "%S" s - | PBinop(bop,e1,e2) -> - Format.fprintf fmt "(@[%a@])@ %a@ (@[%a@])" - print_parsed_expression e1 Printer.pp_binop (Logic_typing.type_binop bop) - print_parsed_expression e2 - | PUnop(uop,e) -> Format.fprintf fmt "%s@;(@[%a@])" - (string_of_unop uop) - print_parsed_expression e - | PArrget(e1,e2) -> Format.fprintf fmt "%a@;[@(%a@]]" - 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 - -let rec print_parsed_condition fmt = function - | PRel(rel,e1,e2) -> - Format.fprintf fmt "%a %a@ %a" - print_parsed_expression e1 - Printer.pp_relation (Logic_typing.type_rel rel) - print_parsed_expression e2 - | PTrue -> Format.pp_print_string fmt "true" - | PFalse -> Format.pp_print_string fmt "false" - | POr(e1,e2) -> Format.fprintf fmt "(@[%a@])@ or@ (@[%a@])" - print_parsed_condition e1 print_parsed_condition e2 - | PAnd(e1,e2) -> Format.fprintf fmt "(@[%a@])@ and@ (@[%a@])" - print_parsed_condition e1 print_parsed_condition e2 - | PNot c -> Format.fprintf fmt "not(@[%a@])" - print_parsed_condition c - | 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 - -let rec print_seq_elt fmt elt = - Format.fprintf fmt "(%a%a){@[%a,%a@]}" - (Pretty_utils.pp_opt print_parsed_condition) elt.condition - print_sequence elt.nested - (Pretty_utils.pp_opt print_parsed_expression) elt.min_rep - (Pretty_utils.pp_opt print_parsed_expression) elt.max_rep - -and print_sequence fmt l = - Pretty_utils.pp_list ~pre:"[@[" ~sep:";@ " ~suf:"@]]" print_seq_elt fmt l - -let print_parsed fmt = function - | Seq l -> print_sequence fmt l - | Otherwise -> Format.pp_print_string fmt "Otherwise" - -let rec print_condition fmt = function - | TCall (kf,None) -> - Format.fprintf fmt "Call(%a)" Kernel_function.pretty kf - | TCall (kf, Some b) -> - Format.fprintf fmt "Call(%a::%s)" - Kernel_function.pretty kf b.Cil_types.b_name - | TReturn kf -> - Format.fprintf fmt "Return(%a)" Kernel_function.pretty kf - | TOr (c1,c2) -> - Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ or@ @[<hov>(@[<2>%a@])@]" - print_condition c1 print_condition c2 - | TAnd (c1,c2) -> - Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ and@ @[<hov>(@[<2>%a@])@]" - print_condition c1 print_condition c2 - | TNot c -> - Format.fprintf fmt "@[<hov 4>@[<hov 5>not(%a@])@]" print_condition c - | TTrue -> Format.pp_print_string fmt "True" - | TFalse -> Format.pp_print_string fmt "False" - | TRel(rel,exp1,exp2) -> - (* \result will be printed as such, not as f().return *) - Format.fprintf fmt "@[(%a)@]@ %a@ @[(%a)@]" - Printer.pp_term exp1 - Printer.pp_relation rel - Printer.pp_term exp2 - -let print_one_action fmt = function - | Counter_init lv -> - Format.fprintf fmt "@[%a <- 1@]" Printer.pp_term_lval lv - | Counter_incr lv -> - Format.fprintf fmt "@[%a <- @[%a@ +@ 1@]@]" - Printer.pp_term_lval lv Printer.pp_term_lval lv - | Pebble_init (set,_,v) -> - Format.fprintf fmt "@[%a <- {@[ %a @]}@]" - Printer.pp_logic_var set.l_var_info Printer.pp_logic_var v - | Pebble_move(s1,_,s2,_) -> - Format.fprintf fmt "@[%a <- %a@]" - Printer.pp_logic_var s1.l_var_info - Printer.pp_logic_var s2.l_var_info - | Copy_value(lv,v) -> - Format.fprintf fmt "@[%a <- %a@]" Printer.pp_term_lval lv Printer.pp_term v - -let print_action fmt l = - Pretty_utils.pp_list ~sep:"@\n" print_one_action fmt l - -(* Use well-parenthesized combination of escape_newline/normal_newline*) -let escape_newline fmt = - let funcs = Format.pp_get_formatter_out_functions fmt () in - let has_printed = ref false in - let out_newline () = - if !has_printed then funcs.Format.out_string " \\\n" 0 3 - else funcs.Format.out_newline () - in - let out_string s b l = - if String.contains (String.sub s b l) '"' then - has_printed:=not !has_printed; - funcs.Format.out_string s b l - in - Format.pp_set_formatter_out_functions fmt - { funcs with Format.out_newline; out_string }; - funcs - -let print_full_transition fmt (cond,action) = - Format.fprintf fmt "%a@\n%a" print_condition cond print_action action - -let trans_label num = "tr"^string_of_int(num) - -let print_trans fmt trans = - Format.fprintf fmt - "@[<2>%s:@ %a@]" - (trans_label trans.numt) print_full_transition trans.cross +type 'a printer = Format.formatter -> 'a -> unit -let state_label num = "st"^string_of_int(num) -let print_state_label fmt st = - Format.fprintf fmt "@[<2>%s:@ %s@]" (state_label st.nums) st.name +let bool3_to_string = function + | True -> "True" + | False -> "False" + | Undefined -> "Undef" let print_bool3 fmt b = - Format.pp_print_string fmt - (match b with - | True -> "True" - | False -> "False" - | Undefined -> "Undef") - -let print_transition fmt tr = - Format.fprintf fmt "@[<2>{@ %d:@ %s@ {%a}@ %s@]}" - tr.numt tr.start.name print_full_transition tr.cross tr.stop.name - -let print_transitionl fmt trl = - Format.fprintf fmt "@[<2>Transitions:@\n%a@]" - (Pretty_utils.pp_list ~sep:"@\n" ~suf:"@\n" print_transition) trl + Format.pp_print_string fmt (bool3_to_string b) let print_state fmt st = Format.fprintf fmt "@[<2>%s@ (acc=%a;@ init=%a;@ num=%d)@]" @@ -185,64 +48,230 @@ 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) = - Format.fprintf fmt "@[<2>Automaton:@\n%a%a@]" - print_statel stl print_transitionl trl - -let dot_state out st = - let shape = - if st.init = Bool3.True && st.acceptation=Bool3.True then "doubleoctagon" - else if st.acceptation=Bool3.True then "octagon" - else if st.init=Bool3.True then "doublecircle" - else "circle" - in - Format.fprintf out "\"%a\" [shape = %s];@\n" print_state_label st shape - -let dot_trans out tr = - let print_label fmt tr = - if DotSeparatedLabels.get () then - Format.pp_print_int fmt tr.numt - else print_trans fmt tr - in - Format.fprintf - out - "\"%a\"@ ->@ \"%a\"@ [label = @[\"%a\"@]];@\n" - print_state_label tr.start - print_state_label tr.stop - print_label tr - -let output_dot_automata (states_l,trans_l) fichier = - let cout = open_out fichier in - let fmt = formatter_of_out_channel cout in - let output_functions = escape_newline fmt in - let one_line_comment s = - let l = String.length s in - let fill = if l >= 75 then 0 else 75 - l in - let spaces = String.make fill ' ' in - Format.fprintf fmt "@[/* %s%s*/@\n@]" s spaces - in - one_line_comment "File generated by Aorai LTL2ACSL Plug-in"; - one_line_comment ""; - one_line_comment "Usage of dot files '.dot' :"; - one_line_comment " dot <MyFile.dot> -T<DesiredType> > <OutputFile>"; - one_line_comment ""; - one_line_comment " Allowed types : canon,dot,xdot,fig,gd,gd2,"; - one_line_comment " gif,hpgl,imap,cmap,ismap,jpg,jpeg,mif,mp,pcl,pic,plain,"; - one_line_comment " plain-ext,png,ps,ps2,svg,svgz,vrml,vtx,wbmp"; - one_line_comment ""; - one_line_comment " Example with postscript file :"; - 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 - (fun fmt -> +let state_label num = "st"^string_of_int(num) +let print_state_label fmt st = + Format.fprintf fmt "@[<2>%s:@ %s@]" (state_label st.nums) st.name + + +module Parsed = +struct + let string_of_unop = function + | Uminus -> "-" + | Ustar -> "*" + | Uamp -> "&" + | Ubw_not -> "~" + + let rec print_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 + | PCst (WStringConstant s) -> Format.fprintf fmt "%S" s + | PBinop(bop,e1,e2) -> + Format.fprintf fmt "(@[%a@])@ %a@ (@[%a@])" + print_expression e1 Printer.pp_binop (Logic_typing.type_binop bop) + print_expression e2 + | PUnop(uop,e) -> + Format.fprintf fmt "%s@;(@[%a@])" + (string_of_unop uop) + print_expression e + | PArrget(e1,e2) -> + Format.fprintf fmt "%a@;[@(%a@]]" + print_expression e1 print_expression e2 + | PField(e,s) -> Format.fprintf fmt "%a.%s" print_expression e s + | PArrow(e,s) -> Format.fprintf fmt "%a->%s" print_expression e s + + let rec print_condition fmt = function + | PRel(rel,e1,e2) -> + Format.fprintf fmt "%a %a@ %a" + print_expression e1 + Printer.pp_relation (Logic_typing.type_rel rel) + print_expression e2 + | PTrue -> Format.pp_print_string fmt "true" + | PFalse -> Format.pp_print_string fmt "false" + | POr(e1,e2) -> + Format.fprintf fmt "(@[%a@])@ or@ (@[%a@])" + print_condition e1 print_condition e2 + | PAnd(e1,e2) -> + Format.fprintf fmt "(@[%a@])@ and@ (@[%a@])" + print_condition e1 print_condition e2 + | PNot c -> + Format.fprintf fmt "not(@[%a@])" + print_condition c + | 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 + + let rec print_seq_elt fmt elt = + Format.fprintf fmt "(%a%a){@[%a,%a@]}" + (Pretty_utils.pp_opt print_condition) elt.condition + print_sequence elt.nested + (Pretty_utils.pp_opt print_expression) elt.min_rep + (Pretty_utils.pp_opt print_expression) elt.max_rep + + and print_sequence fmt l = + Pretty_utils.pp_list ~pre:"[@[" ~sep:";@ " ~suf:"@]]" print_seq_elt fmt l + + let print_guard fmt = function + | Seq l -> print_sequence fmt l + | Otherwise -> Format.pp_print_string fmt "Otherwise" + + let print_action fmt = function + | Metavar_assign (s, e) -> + Format.fprintf fmt "@[$%s := %a@]" s print_expression e + + let print_actionl fmt l = + Pretty_utils.pp_list ~sep:"@\n" print_action fmt l +end + + +module Typed = +struct + let rec print_condition fmt = function + | TCall (kf,None) -> + Format.fprintf fmt "Call(%a)" Kernel_function.pretty kf + | TCall (kf, Some b) -> + Format.fprintf fmt "Call(%a::%s)" + Kernel_function.pretty kf b.Cil_types.b_name + | TReturn kf -> + Format.fprintf fmt "Return(%a)" Kernel_function.pretty kf + | TOr (c1,c2) -> + Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ or@ @[<hov>(@[<2>%a@])@]" + print_condition c1 print_condition c2 + | TAnd (c1,c2) -> + Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ and@ @[<hov>(@[<2>%a@])@]" + print_condition c1 print_condition c2 + | TNot c -> + Format.fprintf fmt "@[<hov 4>@[<hov 5>not(%a@])@]" print_condition c + | TTrue -> + Format.pp_print_string fmt "True" + | TFalse -> + Format.pp_print_string fmt "False" + | TRel(rel,exp1,exp2) -> + (* \result will be printed as such, not as f().return *) + Format.fprintf fmt "@[(%a)@]@ %a@ @[(%a)@]" + Printer.pp_term exp1 + Printer.pp_relation rel + Printer.pp_term exp2 + + let print_action fmt = function + | Counter_init lv -> + Format.fprintf fmt "@[%a <- 1@]" Printer.pp_term_lval lv + | Counter_incr lv -> + Format.fprintf fmt "@[%a <- @[%a@ +@ 1@]@]" + Printer.pp_term_lval lv Printer.pp_term_lval lv + | Pebble_init (set,_,v) -> + Format.fprintf fmt "@[%a <- {@[ %a @]}@]" + Printer.pp_logic_var set.l_var_info Printer.pp_logic_var v + | Pebble_move(s1,_,s2,_) -> + Format.fprintf fmt "@[%a <- %a@]" + Printer.pp_logic_var s1.l_var_info + Printer.pp_logic_var s2.l_var_info + | Copy_value(lv,v) -> + Format.fprintf fmt "@[%a <- %a@]" Printer.pp_term_lval lv Printer.pp_term v + + let print_actionl fmt l = + Pretty_utils.pp_list ~sep:"@\n" print_action fmt l + + (* Use well-parenthesized combination of escape_newline/normal_newline*) + let escape_newline fmt = + let funcs = Format.pp_get_formatter_out_functions fmt () in + let has_printed = ref false in + let out_newline () = + if !has_printed then funcs.Format.out_string " \\\n" 0 3 + else funcs.Format.out_newline () + in + let out_string s b l = + if String.contains (String.sub s b l) '"' then + has_printed:=not !has_printed; + funcs.Format.out_string s b l + in + Format.pp_set_formatter_out_functions fmt + { funcs with Format.out_newline; out_string }; + funcs + + let trans_label num = "tr"^string_of_int(num) + + let print_trans fmt trans = + Format.fprintf fmt + "@[<2>%s:@ %a@\n%a@]" + (trans_label trans.numt) + print_condition trans.cross + print_actionl trans.actions + + let print_transition fmt tr = + Format.fprintf fmt "@[<2>{@ %d:@ %s@ {%a@\n%a}@ %s@]}" + tr.numt + tr.start.name + print_condition tr.cross + print_actionl tr.actions + tr.stop.name + + let print_transitionl fmt trl = + Format.fprintf fmt "@[<2>Transitions:@\n%a@]" + (Pretty_utils.pp_list ~sep:"@\n" ~suf:"@\n" print_transition) trl + + let print_automata fmt auto = + Format.fprintf fmt "@[<2>Automaton:@\n%a%a@]" + print_statel auto.states print_transitionl auto.trans + + let dot_state out st = + let shape = + if st.init = Bool3.True && st.acceptation=Bool3.True then "doubleoctagon" + else if st.acceptation=Bool3.True then "octagon" + else if st.init=Bool3.True then "doublecircle" + else "circle" + in + Format.fprintf out "\"%a\" [shape = %s];@\n" print_state_label st shape + + let dot_trans out tr = + let print_label fmt tr = if DotSeparatedLabels.get () then - (Format.fprintf fmt - "/* guards of transitions */@\ncomment=\"%a\";@\n" - (Pretty_utils.pp_list ~sep:"@\n" print_trans) trans_l)); - Format.pp_set_formatter_out_functions fmt output_functions; - close_out cout + Format.pp_print_int fmt tr.numt + else print_trans fmt tr + in + Format.fprintf + out + "\"%a\"@ ->@ \"%a\"@ [label = @[\"%a\"@]];@\n" + print_state_label tr.start + print_state_label tr.stop + print_label tr + + 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 + let one_line_comment s = + let l = String.length s in + let fill = if l >= 75 then 0 else 75 - l in + let spaces = String.make fill ' ' in + Format.fprintf fmt "@[/* %s%s*/@\n@]" s spaces + in + one_line_comment "File generated by Aorai LTL2ACSL Plug-in"; + one_line_comment ""; + one_line_comment "Usage of dot files '.dot' :"; + one_line_comment " dot <MyFile.dot> -T<DesiredType> > <OutputFile>"; + one_line_comment ""; + one_line_comment " Allowed types : canon,dot,xdot,fig,gd,gd2,"; + one_line_comment " gif,hpgl,imap,cmap,ismap,jpg,jpeg,mif,mp,pcl,pic,plain,"; + one_line_comment " plain-ext,png,ps,ps2,svg,svgz,vrml,vtx,wbmp"; + one_line_comment ""; + one_line_comment " Example with postscript file :"; + 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 + (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)); + Format.pp_set_formatter_out_functions fmt output_functions; + close_out cout +end (* Local Variables: diff --git a/src/plugins/aorai/promelaoutput.mli b/src/plugins/aorai/promelaoutput.mli index 75dcc4bba262d1d40a0946c004be41c6e2f1e126..3edf6aabb28b442fcab77c27aa9bd6a55265a5b7 100644 --- a/src/plugins/aorai/promelaoutput.mli +++ b/src/plugins/aorai/promelaoutput.mli @@ -23,35 +23,35 @@ (* *) (**************************************************************************) -val print_raw_automata : - Format.formatter -> Promelaast.typed_automaton -> unit +open Promelaast + +type 'a printer = Format.formatter -> 'a -> unit + +val print_state : state printer +val print_statel : state list printer + +module Parsed: +sig + val print_expression: expression printer + val print_condition: condition printer + val print_seq_elt: seq_elt printer + val print_sequence: sequence printer + val print_guard: guard printer + val print_action: action printer + val print_actionl: action list printer +end + +module Typed: +sig + val print_condition : typed_condition printer + val print_action: typed_action printer + val print_actionl: typed_action list printer + val print_transition: typed_trans printer + val print_transitionl: typed_trans list printer + val print_automata : typed_automaton printer + val output_dot_automata : typed_automaton -> string -> unit +end -val print_parsed_expression: Format.formatter -> Promelaast.expression -> unit - -val print_parsed_condition: Format.formatter -> Promelaast.condition -> unit - -val print_seq_elt: Format.formatter -> Promelaast.seq_elt -> unit - -val print_sequence: Format.formatter -> Promelaast.sequence -> unit - -val print_parsed: Format.formatter -> Promelaast.parsed_condition -> unit - -val print_condition: Format.formatter -> Promelaast.typed_condition -> unit - -val print_action: Format.formatter -> Promelaast.action -> unit - -val print_transition: - Format.formatter -> - (Promelaast.typed_condition * Promelaast.action) Promelaast.trans -> unit - -val print_transitionl: - Format.formatter -> - (Promelaast.typed_condition * Promelaast.action) Promelaast.trans list -> unit - -val print_state : Format.formatter -> Promelaast.state -> unit -val print_statel : Format.formatter -> Promelaast.state list -> unit - -val output_dot_automata : Promelaast.typed_automaton -> string -> unit (* Local Variables: diff --git a/src/plugins/aorai/promelaparser.mly b/src/plugins/aorai/promelaparser.mly index bae7efad71dad89aa34e2fa47ef4dea5cbda5de2..4bcac643722e16f76ec9c72423f3e4f44d030119 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 @@ -119,9 +119,9 @@ state trans else let tr_list= - List.fold_left (fun l1 (cr,stop_st) -> - List.fold_left (fun l2 st -> - {start=st;stop=stop_st;cross=Seq (to_seq cr);numt=(-1)}::l2 + List.fold_left (fun l1 (cr,stop) -> + List.fold_left (fun l2 start -> + {start;stop;cross=Seq (to_seq cr);actions=[];numt=(-1)}::l2 ) l1 stl ) [] trl in @@ -166,7 +166,7 @@ label (String.compare (String.sub $1 0 10) "accept_all")=0 then trans:= - {start=old;stop=old;cross=Seq (to_seq PTrue);numt=(-1)} :: + {start=old;stop=old;cross=Seq (to_seq PTrue);actions=[];numt=(-1)} :: !trans; (* If the name includes accept then this state is an acceptation one. *) diff --git a/src/plugins/aorai/promelaparser_withexps.mly b/src/plugins/aorai/promelaparser_withexps.mly index 36f93360a5037fe1805b122424f6be432fa8c681..bf852a65f3747b7a4c976151a3b593b90fe4da18 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 @@ -128,9 +128,9 @@ state trans else let tr_list= - List.fold_left (fun l1 (cr,stop_st) -> - List.fold_left (fun l2 st -> - {start=st;stop=stop_st;cross=Seq (to_seq cr);numt=(-1)}::l2 + List.fold_left (fun l1 (cr,stop) -> + List.fold_left (fun l2 start -> + {start;stop;cross=Seq (to_seq cr);actions=[];numt=(-1)}::l2 ) l1 stl ) [] trl in @@ -178,7 +178,7 @@ label (String.compare (String.sub $1 0 10) "accept_all")=0 then trans:= - {start=old;stop=old;cross=Seq (to_seq PTrue);numt=(-1)}::!trans; + {start=old;stop=old;cross=Seq (to_seq PTrue);actions=[];numt=(-1)}::!trans; (* If the name includes accept then this state is an acceptation one. *) diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml index b559eeb411ce69b62129d8bf7ba5beb05415ec3d..7807773dd168dcd111c2c11a09ae6fa1efe817cc 100644 --- a/src/plugins/aorai/tests/Aorai_test.ml +++ b/src/plugins/aorai/tests/Aorai_test.ml @@ -1,15 +1,15 @@ (* Small script to test that the code generated by aorai can be parsed again * by frama-c. - *) +*) open Kernel module P = Plugin.Register -(struct - let name = "aorai testing module" - let shortname = "aorai-test" - let help = "utility script for aorai regtests" - end) + (struct + let name = "aorai testing module" + let shortname = "aorai-test" + let help = "utility script for aorai regtests" + end) module TestNumber = P.Zero @@ -17,25 +17,25 @@ module TestNumber = let option_name = "-aorai-test-number" let help = "test number when multiple tests are run over the same file" let arg_name = "n" - end) + end) module InternalWpShare = P.Filepath( - struct - let option_name = "-aorai-test-wp-share" - let help = "use custom wp share dir (when in internal plugin mode)" - let arg_name = "dir" - let existence = Filepath.Must_exist - let file_kind = "wp share directory" - end) + struct + let option_name = "-aorai-test-wp-share" + let help = "use custom wp share dir (when in internal plugin mode)" + let arg_name = "dir" + let existence = Filepath.Must_exist + let file_kind = "wp share directory" + end) module ProveAuxSpec = P.False( - struct - let option_name = "-aorai-test-prove-aux-spec" - let help = "use WP + alt-ergo to prove that generated spec and body \ - of auxiliary automata functions match" - end) + struct + let option_name = "-aorai-test-prove-aux-spec" + let help = "use WP + alt-ergo to prove that generated spec and body \ + of auxiliary automata functions match" + end) let ok = ref false @@ -95,6 +95,7 @@ let extend () = Project.set_current my_project; Kernel.SymbolicPath.add ("TMPDIR:"^Filename.get_temp_dir_name()); Files.append_after [ Filepath.Normalized.of_string tmpfile ]; + Kernel.LogicalOperators.on (); Constfold.off (); Ast.compute(); if ProveAuxSpec.get () then begin diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle index 43f443e26e9773bfe488435071f0953066f1112b..af9bc71a2b3a1adf94c0022438693926ffc17f6f 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle @@ -52,9 +52,8 @@ extern int call_to_an_undefined_function(void); T0_S2_tmp = T0_S2; T0_init_tmp = T0_init; accept_S1_tmp = accept_S1; - if (T0_S2 == 1) accept_S1_tmp = 1; - else - if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0; + if (T0_S2 == 1 || accept_S1 == 1) accept_S1_tmp = 1; + else accept_S1_tmp = 0; T0_init_tmp = 0; T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; @@ -159,9 +158,7 @@ int a(void) accept_S1_tmp = accept_S1; accept_S1_tmp = 0; T0_init_tmp = 0; - if (T0_S2 == 1) T0_S2_tmp = 1; - else - if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; + if (T0_S2 == 1 || accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; T0_init = T0_init_tmp; accept_S1 = accept_S1_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle index 31031e82bb479afbb18fa7e403bf822e42c7f654..9da27b6622ebd3fbb5ae7fefb8a0e694d48175d1 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle @@ -271,12 +271,10 @@ int commit_trans(void) accept_S4_tmp = accept_S4; accept_init_tmp = accept_init; accept_init_tmp = 0; - if (accept_S2 == 1) - if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0; + if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0; accept_S3_tmp = 0; - if (accept_S2 == 1) - if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0; + if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0; accept_S1_tmp = 0; accept_S1 = accept_S1_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle index e2122593e23b155dd6385ea9e1f256cf66a3157d..3b6f510bb856cc315fcedd97a9d0796d7bbf4d9a 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle @@ -144,9 +144,7 @@ int rr = 1; accept_all_tmp = 0; accept_S5_tmp = 0; accept_S4_tmp = 0; - if (T0_S2 == 1) - if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0; - else accept_S3_tmp = 0; + if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0; T0_init_tmp = 0; if (T0_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle index 44c7d11061b5a33640e834283e79a608ac9885e1..0e2861364d6f1efef4a6191a0cd4ac2a817c7b23 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle @@ -236,9 +236,7 @@ void opa(void) accept_S3_tmp = accept_S3; accept_all_tmp = accept_all; accept_all_tmp = 0; - if (T1_S2 == 1) - if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0; - else accept_S3_tmp = 0; + if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0; T1_S2_tmp = 0; T0_init_tmp = 0; T0_S4_tmp = 0; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle index 41a681dcff82e65b2fa850c0c8f9f7485adc2a39..384591685af0dcf73ebd192dafbaa2cf6424b777 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle @@ -217,9 +217,8 @@ int decode_int(char *s) accept_S2_tmp = accept_S2; accept_init_tmp = accept_init; accept_init_tmp = 0; - if (accept_S1 == 1) accept_S2_tmp = 1; - else - if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0; + if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1; + else accept_S2_tmp = 0; accept_S1_tmp = 0; accept_S1 = accept_S1_tmp; accept_S2 = accept_S2_tmp; @@ -266,12 +265,10 @@ int decode_int(char *s) accept_S2_tmp = accept_S2; accept_init_tmp = accept_init; accept_init_tmp = 0; - if (accept_S1 == 1) accept_S2_tmp = 1; - else - if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0; - if (accept_S1 == 1) accept_S1_tmp = 1; - else - if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0; + if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1; + else accept_S2_tmp = 0; + if (accept_S1 == 1 || accept_S2 == 1) accept_S1_tmp = 1; + else accept_S1_tmp = 0; accept_S1 = accept_S1_tmp; accept_S2 = accept_S2_tmp; accept_init = accept_init_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle index 2a45f6df9a0c0492d43a914b3956d05da1ec92dc..fd43837e998528a1c7cfa61c0424d06e0c3d4508 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle @@ -106,11 +106,7 @@ int global_argc = 0; accept_T2_tmp = 0; T1_tmp = 0; T0_init_tmp = 0; - if (S1 == 1) S1_tmp = 1; - else - if (T1 == 1) - if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0; - else S1_tmp = 0; + if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; T0_init = T0_init_tmp; T1 = T1_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle index 741ab2d5228be77cd697851f6fb4c8a80e783e9c..a40a3eae30459dfa081154ccd2b0eed95761f1b8 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle @@ -106,11 +106,7 @@ int global_argc = 0; accept_T2_tmp = 0; T1_tmp = 0; T0_init_tmp = 0; - if (S1 == 1) S1_tmp = 1; - else - if (T1 == 1) - if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0; - else S1_tmp = 0; + if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; T0_init = T0_init_tmp; T1 = T1_tmp; @@ -419,9 +415,7 @@ int sumOne(char *t, int length) T0_init_tmp = T0_init; T1_tmp = T1; accept_T2_tmp = accept_T2; - if (T1 == 1) - if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0; - else accept_T2_tmp = 0; + if (T1 == 1 && res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0; if (T1 == 1) T1_tmp = 1; else T1_tmp = 0; T0_init_tmp = 0; S1_tmp = 0; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle index 98fef42772d572f1ea75d8df26c6b528b85884c1..d81509eb53661bace2a79e5e2babdface3e95275 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle @@ -58,9 +58,7 @@ enum aorai_OpStatusList { accept_S2_tmp = 0; accept_S1_tmp = 0; T0_init_tmp = 0; - if (T0_S2 == 1) T0_S2_tmp = 1; - else - if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; + if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; T0_init = T0_init_tmp; accept_S1 = accept_S1_tmp; @@ -249,14 +247,10 @@ int countOne(char *argv) T0_init_tmp = T0_init; accept_S1_tmp = accept_S1; accept_S2_tmp = accept_S2; - if (T0_S2 == 1) accept_S2_tmp = 1; - else - if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0; - if (T0_S2 == 1) accept_S1_tmp = 1; - else - if (accept_S1 == 1) accept_S1_tmp = 1; - else - if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0; + if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1; + else accept_S2_tmp = 0; + if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1; + else accept_S1_tmp = 0; T0_init_tmp = 0; if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle index 4666520a57e4971263d00b54bcf6e80c92189602..5cc019fcad43e0cfacafa6eb123b8055daf1dda4 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle @@ -58,9 +58,7 @@ enum aorai_OpStatusList { accept_S2_tmp = 0; accept_S1_tmp = 0; T0_init_tmp = 0; - if (T0_S2 == 1) T0_S2_tmp = 1; - else - if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; + if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; T0_init = T0_init_tmp; accept_S1 = accept_S1_tmp; @@ -247,14 +245,10 @@ int countOne(char *argv) T0_init_tmp = T0_init; accept_S1_tmp = accept_S1; accept_S2_tmp = accept_S2; - if (T0_S2 == 1) accept_S2_tmp = 1; - else - if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0; - if (T0_S2 == 1) accept_S1_tmp = 1; - else - if (accept_S1 == 1) accept_S1_tmp = 1; - else - if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0; + if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1; + else accept_S2_tmp = 0; + if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1; + else accept_S1_tmp = 0; T0_init_tmp = 0; if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle index 95252b378b334550da4837d9954756ec07d77f4c..0fb781bb7040975d8e51beef6328114ceb34a501 100644 --- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle @@ -58,9 +58,7 @@ enum aorai_OpStatusList { accept_S2_tmp = 0; accept_S1_tmp = 0; T0_init_tmp = 0; - if (T0_S2 == 1) T0_S2_tmp = 1; - else - if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; + if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; T0_init = T0_init_tmp; accept_S1 = accept_S1_tmp; @@ -254,14 +252,10 @@ int countOne(char *argv) T0_init_tmp = T0_init; accept_S1_tmp = accept_S1; accept_S2_tmp = accept_S2; - if (T0_S2 == 1) accept_S2_tmp = 1; - else - if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0; - if (T0_S2 == 1) accept_S1_tmp = 1; - else - if (accept_S1 == 1) accept_S1_tmp = 1; - else - if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0; + if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1; + else accept_S2_tmp = 0; + if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1; + else accept_S1_tmp = 0; T0_init_tmp = 0; if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0; T0_S2 = T0_S2_tmp; diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle index 6e0517bda1c07bff22106dd567c40ef03029419d..0cf6aa042e89216a12267f75a00f12f7900d45ec 100644 --- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle @@ -4,5 +4,5 @@ [aorai] Welcome to the Aorai plugin [kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing) [wp] Warning: Missing RTE guards -[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:81: Warning: +[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:85: Warning: Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i new file mode 100644 index 0000000000000000000000000000000000000000..26744167705ea93e49e38818c96dcb32d17b623b --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i @@ -0,0 +1,6 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + +void main(void) {} + diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.ya b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya new file mode 100644 index 0000000000000000000000000000000000000000..059f0d555ba7fa97e2d82f9988a895f06b968132 --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya @@ -0,0 +1,9 @@ +%init: a; +%accept: b; +%deterministic; + +$x : int; + +a : { CALL(main)* } -> b; + +b : -> b; diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i new file mode 100644 index 0000000000000000000000000000000000000000..cff3994c1017f532d1d44db092abb5be27d1dcb8 --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-right.i @@ -0,0 +1,27 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + +void f(int x) {} +void g(void) {} +void h(int x) {} +void i(void) {} + +void main(int t) +{ + if (t) { + f(42); + } + else { + g(); + goto L; + } + + int x = 0; + while (x < 100) + { + h(x); + L: i(); + x++; + } +} diff --git a/src/plugins/aorai/tests/ya/metavariables-right.ya b/src/plugins/aorai/tests/ya/metavariables-right.ya new file mode 100644 index 0000000000000000000000000000000000000000..d2d2715062e30d62397f34ea2bf4b43769a667e7 --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-right.ya @@ -0,0 +1,30 @@ +%init: a; +%accept: i; +%deterministic; + +$x : int; +$y : int; + +a : { CALL(main) } -> b; + +b : + { CALL(f) } $x := f().x; $y := $x -> c +| { CALL(g) } -> d +; + +c : { RETURN(f) } -> e; + +d : { RETURN(g) } -> g; + +e : + { CALL(h) && $x > 0 } -> f +| { RETURN(main) } -> i +; + +f : { RETURN(h) } -> g; + +g : { CALL(i) } -> h; + +h : { RETURN(i) } $y := 0; $x := 1; -> e; + +i : -> i; diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i new file mode 100644 index 0000000000000000000000000000000000000000..09ea4b6c4bcfc15e83ef2c2a676be84c00ca294b --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i @@ -0,0 +1,22 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + +void f(int x) {} +void g(void) {} +void h(void) {} + +void main(void) +{ + int x = 0; + while (x < 100) + { + if (x % 2) + f(x); + else + g(); + h(); + x++; + } +} + diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.ya b/src/plugins/aorai/tests/ya/metavariables-wrong.ya new file mode 100644 index 0000000000000000000000000000000000000000..8a29440dfddb6667409bae53438c9366df9eb77d --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-wrong.ya @@ -0,0 +1,23 @@ +%init: a; +%accept: g; +%deterministic; + +$x : int; + +a : { CALL(main) } -> b; + +b : + { CALL(f) } $x := f().x -> c +| { CALL(g) } -> d +| { RETURN(main) } -> g +; + +c : { RETURN(f) } -> e; + +d : { RETURN(g) } -> e; + +e : { CALL(h) && $x > 0 } -> f; + +f : { RETURN(h) } -> b; + +g : -> g; diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle index 7b3833fb8c530be00f93100df610e7986540081f..fd7526444df55abd2c128af76809b32c0a411955 100644 --- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle @@ -60,12 +60,9 @@ int X; @/ void f_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (3 == aorai_CurStates) aorai_CurStates_tmp = S_in_f; - aorai_CurStates = aorai_CurStates_tmp; + if (3 == aorai_CurStates) aorai_CurStates = S_in_f; return; } @@ -99,12 +96,9 @@ int X; @/ void f_post_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (2 == aorai_CurStates) aorai_CurStates_tmp = in_main; - aorai_CurStates = aorai_CurStates_tmp; + if (2 == aorai_CurStates) aorai_CurStates = in_main; return; } @@ -151,12 +145,9 @@ void f(void) @/ void main_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (0 == aorai_CurStates) aorai_CurStates_tmp = Sf; - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates) aorai_CurStates = Sf; return; } @@ -190,12 +181,9 @@ void f(void) @/ void main_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (4 == aorai_CurStates) aorai_CurStates_tmp = S2; - aorai_CurStates = aorai_CurStates_tmp; + if (4 == aorai_CurStates) aorai_CurStates = S2; return; } diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle index ab55916b9af828248a4309cdc6424442f8027441..7141a6e19585342e2f1f9571efaa71e68c2ba704 100644 --- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle @@ -61,12 +61,9 @@ check lemma I_deterministic_trans{L}: @/ void main_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (0 == aorai_CurStates) aorai_CurStates_tmp = I; - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates) aorai_CurStates = I; return; } @@ -88,12 +85,9 @@ check lemma I_deterministic_trans{L}: @/ void main_post_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (0 == aorai_CurStates) aorai_CurStates_tmp = I; - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates) aorai_CurStates = I; return; } diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle index 5a30e59e7d5e51dd0849a5f48c908fbe5493e073..6b9c9095bc9917c070ddd1dbf2ec9d73de8d75c4 100644 --- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle @@ -105,15 +105,11 @@ check lemma S0_deterministic_trans{L}: @/ void g_pre_func(int x) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_g; - aorai_CurStates_tmp = aorai_CurStates; - if (3 == aorai_CurStates) - if (x == 5) aorai_CurStates_tmp = S5; - if (3 == aorai_CurStates) - if (x == 4) aorai_CurStates_tmp = S4; - aorai_CurStates = aorai_CurStates_tmp; + if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4; + else + if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5; return; } @@ -161,13 +157,11 @@ check lemma S0_deterministic_trans{L}: @/ void g_post_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_g; - aorai_CurStates_tmp = aorai_CurStates; - if (4 == aorai_CurStates) aorai_CurStates_tmp = S3; - if (5 == aorai_CurStates) aorai_CurStates_tmp = S1; - aorai_CurStates = aorai_CurStates_tmp; + if (5 == aorai_CurStates) aorai_CurStates = S1; + else + if (4 == aorai_CurStates) aorai_CurStates = S3; return; } @@ -230,13 +224,9 @@ void g(int x) @/ void f_pre_func(int x) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (1 == aorai_CurStates) - if (x == 4) aorai_CurStates_tmp = S3; - aorai_CurStates = aorai_CurStates_tmp; + if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3; return; } @@ -280,14 +270,9 @@ void g(int x) @/ void f_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (1 == aorai_CurStates) - if (res == 0) - if (X == 5) aorai_CurStates_tmp = S2; - aorai_CurStates = aorai_CurStates_tmp; + if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2; return; } @@ -356,15 +341,11 @@ int f(int x) @/ void real_main_pre_func(int c) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_real_main; - aorai_CurStates_tmp = aorai_CurStates; - if (0 == aorai_CurStates) - if (c == 0) aorai_CurStates_tmp = S2; - if (0 == aorai_CurStates) - if (c != 0) aorai_CurStates_tmp = S1; - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1; + else + if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2; return; } @@ -407,12 +388,9 @@ int f(int x) @/ void real_main_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_real_main; - aorai_CurStates_tmp = aorai_CurStates; - if (2 == aorai_CurStates) aorai_CurStates_tmp = Sf; - aorai_CurStates = aorai_CurStates_tmp; + if (2 == aorai_CurStates) aorai_CurStates = Sf; return; } @@ -471,12 +449,9 @@ int real_main(int c) @/ void main_pre_func(int c) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (7 == aorai_CurStates) aorai_CurStates_tmp = S0; - aorai_CurStates = aorai_CurStates_tmp; + if (7 == aorai_CurStates) aorai_CurStates = S0; return; } @@ -519,12 +494,9 @@ int real_main(int c) @/ void main_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (6 == aorai_CurStates) aorai_CurStates_tmp = Sf; - aorai_CurStates = aorai_CurStates_tmp; + if (6 == aorai_CurStates) aorai_CurStates = Sf; return; } diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle index 3fa9613a782d0cd189af5fb61fae70e89db84d9f..52323f131b74b603bc960c19408f6ea80930453f 100644 --- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle @@ -95,7 +95,6 @@ check lemma aorai_intermediate_state_deterministic_trans{L}: behavior buch_state_aorai_intermediate_state_out: assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 1); ensures aorai_CurStates ≢ aorai_intermediate_state; - ensures aorai_x ≡ \old(aorai_x); behavior buch_state_aorai_intermediate_state_0_out: ensures aorai_CurStates ≢ aorai_intermediate_state_0; @@ -111,7 +110,6 @@ check lemma aorai_intermediate_state_deterministic_trans{L}: behavior buch_state_aorai_intermediate_state_2_out: assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 3); ensures aorai_CurStates ≢ aorai_intermediate_state_2; - ensures aorai_x_0 ≡ \old(aorai_x_0); behavior buch_state_aorai_reject_out: ensures aorai_CurStates ≢ aorai_reject; @@ -121,24 +119,28 @@ check lemma aorai_intermediate_state_deterministic_trans{L}: behavior buch_state_main_0_out: ensures aorai_CurStates ≢ main_0; + + behavior aorai_x_0_unchanged: + assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 3); + ensures aorai_x_0 ≡ \old(aorai_x_0); + + behavior aorai_x_unchanged: + assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 1); + ensures aorai_x ≡ \old(aorai_x); @/ void f_pre_func(int x) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (7 == aorai_CurStates) - if (x == 3) { - aorai_CurStates_tmp = aorai_intermediate_state_2; + if (7 == aorai_CurStates && x == 1) { + aorai_CurStates = aorai_intermediate_state; + aorai_x = x; + } + else + if (7 == aorai_CurStates && x == 3) { + aorai_CurStates = aorai_intermediate_state_2; aorai_x_0 = x; } - if (7 == aorai_CurStates) - if (x == 1) { - aorai_CurStates_tmp = aorai_intermediate_state; - aorai_x = x; - } - aorai_CurStates = aorai_CurStates_tmp; return; } @@ -209,24 +211,15 @@ check lemma aorai_intermediate_state_deterministic_trans{L}: @/ void f_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (4 == aorai_CurStates) { - if (aorai_x_0 != 3) aorai_CurStates_tmp = aorai_reject; - else goto _LAND; - } - else { - _LAND: ; - if (1 == aorai_CurStates) - if (aorai_x != 1) aorai_CurStates_tmp = aorai_reject; - } - if (1 == aorai_CurStates) - if (aorai_x == 1) aorai_CurStates_tmp = aorai_intermediate_state_0; - if (4 == aorai_CurStates) - if (aorai_x_0 == 3) aorai_CurStates_tmp = OK; - aorai_CurStates = aorai_CurStates_tmp; + if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK; + else + if (1 == aorai_CurStates && aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0; + else + if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject; + else + if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject; return; } @@ -326,7 +319,6 @@ int f(int x) behavior buch_state_aorai_intermediate_state_1_out: assumes aorai_CurStates ≢ aorai_intermediate_state_0; ensures aorai_CurStates ≢ aorai_intermediate_state_1; - ensures aorai_y ≡ \old(aorai_y); behavior buch_state_aorai_intermediate_state_2_out: ensures aorai_CurStates ≢ aorai_intermediate_state_2; @@ -344,20 +336,23 @@ int f(int x) behavior buch_state_main_0_out: ensures aorai_CurStates ≢ main_0; + + behavior aorai_y_unchanged: + assumes aorai_CurStates ≢ aorai_intermediate_state_0; + ensures aorai_y ≡ \old(aorai_y); @/ void g_pre_func(int y) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_g; - aorai_CurStates_tmp = aorai_CurStates; - if (5 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject; - if (2 == aorai_CurStates) { - aorai_CurStates_tmp = aorai_intermediate_state_1; - aorai_y = y; - } - if (0 == aorai_CurStates) aorai_CurStates_tmp = OK; - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates) aorai_CurStates = OK; + else + if (2 == aorai_CurStates) { + aorai_CurStates = aorai_intermediate_state_1; + aorai_y = y; + } + else + if (5 == aorai_CurStates) aorai_CurStates = aorai_reject; return; } @@ -420,22 +415,15 @@ int f(int x) @/ void g_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_g; - aorai_CurStates_tmp = aorai_CurStates; - if (5 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject; + if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK; else - if (3 == aorai_CurStates) - if (aorai_y != 2) aorai_CurStates_tmp = aorai_reject; - if (3 == aorai_CurStates) { - if (aorai_y == 2) aorai_CurStates_tmp = OK; else goto _LAND; - } - else { - _LAND: ; - if (0 == aorai_CurStates) aorai_CurStates_tmp = OK; - } - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates) aorai_CurStates = OK; + else + if (5 == aorai_CurStates) aorai_CurStates = aorai_reject; + else + if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject; return; } @@ -514,12 +502,9 @@ int g(int y) @/ void main_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (6 == aorai_CurStates) aorai_CurStates_tmp = main_0; - aorai_CurStates = aorai_CurStates_tmp; + if (6 == aorai_CurStates) aorai_CurStates = main_0; return; } @@ -567,13 +552,11 @@ int g(int y) @/ void main_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - if (5 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject; - if (0 == aorai_CurStates) aorai_CurStates_tmp = OK; - aorai_CurStates = aorai_CurStates_tmp; + if (0 == aorai_CurStates) aorai_CurStates = OK; + else + if (5 == aorai_CurStates) aorai_CurStates = aorai_reject; return; } diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle index ebd409ed392d15619f4c8d0f79e744425eb21ad0..ea603b7e865bbc3a1982b4512166a5ed8cf48eb7 100644 --- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle @@ -315,14 +315,10 @@ int main_bhv_bhv(int c); */ aorai_reject_tmp = 0; aorai_intermediate_state_2_tmp = 0; aorai_intermediate_state_1_tmp = 0; - if (S0 == 1) - if (c <= 0) aorai_intermediate_state_0_tmp = 1; - else aorai_intermediate_state_0_tmp = 0; + if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1; else aorai_intermediate_state_0_tmp = 0; bhv_aux = main_bhv_bhv(c); - if (S0 == 1) - if (bhv_aux) aorai_intermediate_state_tmp = 1; - else aorai_intermediate_state_tmp = 0; + if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1; else aorai_intermediate_state_tmp = 0; Sf_tmp = 0; S0_tmp = 0; @@ -410,25 +406,17 @@ int main_bhv_bhv(int c); */ aorai_intermediate_state_1_tmp = aorai_intermediate_state_1; aorai_intermediate_state_2_tmp = aorai_intermediate_state_2; aorai_reject_tmp = aorai_reject; - if (aorai_intermediate_state_0 == 1) aorai_reject_tmp = 1; - else - if (aorai_intermediate_state_2 == 1) { - if (res != 0) aorai_reject_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (aorai_reject == 1) aorai_reject_tmp = 1; - else aorai_reject_tmp = 0; - } + if ((aorai_intermediate_state_0 == 1 || aorai_intermediate_state_2 == 1 && + res != 0) || aorai_reject == 1) + aorai_reject_tmp = 1; + else aorai_reject_tmp = 0; aorai_intermediate_state_2_tmp = 0; aorai_intermediate_state_1_tmp = 0; aorai_intermediate_state_0_tmp = 0; aorai_intermediate_state_tmp = 0; - if (aorai_intermediate_state == 1) Sf_tmp = 1; - else - if (aorai_intermediate_state_2 == 1) - if (res == 0) Sf_tmp = 1; else Sf_tmp = 0; - else Sf_tmp = 0; + if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 && + res == 0) Sf_tmp = 1; + else Sf_tmp = 0; S0_tmp = 0; S0 = S0_tmp; Sf = Sf_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle index 3913f00e2f485fad13453eb892e7fcc28f412f75..ccfb249eba5eb4f3b759bba09f44a869117caa21 100644 --- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle @@ -33,11 +33,8 @@ int f(void); @/ void main_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - aorai_CurStates = aorai_CurStates_tmp; return; } @@ -54,11 +51,8 @@ int f(void); @/ void main_post_func(int res) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - aorai_CurStates = aorai_CurStates_tmp; return; } diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle index 04b434bbf6da11f31a874aaceca1c219eb90348e..ccc98a41d83d4339cb70a182bed8396973f9d901 100644 --- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle @@ -63,13 +63,17 @@ enum aorai_OpStatusList { (0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5)) ∧ 0 ≡ aorai_intermediate_state; ensures 0 ≡ aorai_intermediate_state_1; - ensures aorai_counter ≡ \old(aorai_counter); behavior buch_state_aorai_intermediate_state_2_out: ensures 0 ≡ aorai_intermediate_state_2; behavior buch_state_aorai_intermediate_state_3_out: ensures 0 ≡ aorai_intermediate_state_3; + + behavior aorai_counter_unchanged: + assumes 0 ≡ aorai_intermediate_state; + assumes 0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5); + ensures aorai_counter ≡ \old(aorai_counter); @/ void f_pre_func(void) { @@ -91,14 +95,10 @@ enum aorai_OpStatusList { aorai_intermediate_state_3_tmp = aorai_intermediate_state_3; aorai_intermediate_state_3_tmp = 0; aorai_intermediate_state_2_tmp = 0; - if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1; - else - if (aorai_intermediate_state_0 == 1) - if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1; - else aorai_intermediate_state_1_tmp = 0; - else aorai_intermediate_state_1_tmp = 0; - if (aorai_intermediate_state_0 == 1) - if (aorai_counter < 5) aorai_counter ++; + if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 && + aorai_counter < 5) aorai_intermediate_state_1_tmp = 1; + else aorai_intermediate_state_1_tmp = 0; + if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++; if (aorai_intermediate_state == 1) aorai_counter = 1; aorai_intermediate_state_0_tmp = 0; aorai_intermediate_state_tmp = 0; @@ -539,9 +539,9 @@ void g(void) aorai_intermediate_state_1_tmp = 0; aorai_intermediate_state_0_tmp = 0; aorai_intermediate_state_tmp = 0; - if (aorai_intermediate_state == 1) Sf_tmp = 1; - else - if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0; + if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1) + Sf_tmp = 1; + else Sf_tmp = 0; S0_tmp = 0; S0 = S0_tmp; Sf = Sf_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..57c2d7eed1ca61046277d1cbf5d005a9fde10a52 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions. +[kernel] Plug-in aorai aborted: invalid user input. diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..39843d1a28ef389cbcc34ab6095bff3f80d0ec8a --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle @@ -0,0 +1,684 @@ +[kernel] Parsing tests/ya/metavariables-right.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing) +/* Generated by Frama-C */ +enum aorai_States { + aorai_reject_state = -2, + a = 0, + b = 1, + c = 2, + d = 3, + e = 4, + f_0 = 5, + g_0 = 6, + h_0 = 7, + i_0 = 8 +}; +enum aorai_ListOper { + op_f = 4, + op_g = 3, + op_h = 2, + op_i = 1, + op_main = 0 +}; +enum aorai_OpStatusList { + aorai_Terminated = 1, + aorai_Called = 0 +}; +/*@ check lemma i_0_deterministic_trans{L}: \true; + */ +/*@ check lemma h_0_deterministic_trans{L}: \true; + */ +/*@ check lemma g_0_deterministic_trans{L}: \true; + */ +/*@ check lemma f_0_deterministic_trans{L}: \true; + */ +/*@ check lemma d_deterministic_trans{L}: \true; + */ +/*@ check lemma c_deterministic_trans{L}: \true; + */ +/*@ check lemma a_deterministic_trans{L}: \true; + */ +/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */ +/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */ +/*@ +check lemma b_deterministic_trans{L}: + ¬(\at(aorai_CurOperation,L) ≡ op_g ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ + \at(aorai_CurOperation,L) ≡ op_f ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Called); + */ +/*@ ghost int aorai_CurStates = a; */ +/*@ ghost int aorai_x = 0; */ +/*@ +check lemma e_deterministic_trans{L}: + ¬(\at(aorai_CurOperation,L) ≡ op_main ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ + \at(aorai_CurOperation,L) ≡ op_h ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ \at(aorai_x,L) > 0); + */ +/*@ ghost int aorai_y = 0; */ +/*@ ghost + /@ requires aorai_CurStates ≡ b; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_f; + assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation, + aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_in_0: + assumes aorai_CurStates ≡ b; + ensures aorai_CurStates ≡ c; + ensures aorai_x ≡ \old(x); + ensures aorai_y ≡ aorai_x; + + behavior buch_state_c_out: + assumes aorai_CurStates ≢ b; + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + + behavior aorai_y_unchanged: + assumes aorai_CurStates ≢ b; + ensures aorai_y ≡ \old(aorai_y); + + behavior aorai_x_unchanged: + assumes aorai_CurStates ≢ b; + ensures aorai_x ≡ \old(aorai_x); + @/ + void f_pre_func(int x) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_f; + if (1 == aorai_CurStates) { + aorai_CurStates = c; + aorai_x = x; + aorai_y = aorai_x; + } + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ c; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_f; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_in: + assumes aorai_CurStates ≡ c; + ensures aorai_CurStates ≡ e; + + behavior buch_state_e_out: + assumes aorai_CurStates ≢ c; + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void f_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_f; + if (2 == aorai_CurStates) aorai_CurStates = e; + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ b; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ e; + ensures + \at(aorai_CurStates ≡ b,Pre) ∧ aorai_CurStates ≡ e ⇒ + aorai_y ≡ \at(aorai_x,Pre) + 0; + ensures + \at(aorai_CurStates ≡ b,Pre) ∧ aorai_CurStates ≡ e ⇒ + aorai_x ≡ \at(x,Pre) + 0; + */ +void f(int x) +{ + /*@ ghost f_pre_func(x); */ + /*@ ghost f_post_func(); */ + return; +} + +/*@ ghost + /@ requires aorai_CurStates ≡ b; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_g; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_in: + assumes aorai_CurStates ≡ b; + ensures aorai_CurStates ≡ d; + + behavior buch_state_d_out: + assumes aorai_CurStates ≢ b; + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void g_pre_func(void) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_g; + if (1 == aorai_CurStates) aorai_CurStates = d; + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ d; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_g; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_in: + assumes aorai_CurStates ≡ d; + ensures aorai_CurStates ≡ g_0; + + behavior buch_state_g_0_out: + assumes aorai_CurStates ≢ d; + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void g_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_g; + if (3 == aorai_CurStates) aorai_CurStates = g_0; + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ b; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ g_0; + */ +void g(void) +{ + /*@ ghost g_pre_func(); */ + /*@ ghost g_post_func(); */ + return; +} + +/*@ ghost + /@ requires aorai_CurStates ≡ e; + requires aorai_CurStates ≡ e ⇒ aorai_x > 0; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_h; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_in: + assumes aorai_CurStates ≡ e ∧ aorai_x > 0; + ensures aorai_CurStates ≡ f_0; + + behavior buch_state_f_0_out: + assumes aorai_CurStates ≢ e ∨ ¬(aorai_x > 0); + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void h_pre_func(int x) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_h; + if (4 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0; + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ f_0; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_h; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_in: + assumes aorai_CurStates ≡ f_0; + ensures aorai_CurStates ≡ g_0; + + behavior buch_state_g_0_out: + assumes aorai_CurStates ≢ f_0; + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void h_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_h; + if (5 == aorai_CurStates) aorai_CurStates = g_0; + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ e; + requires aorai_CurStates ≡ e ⇒ aorai_x > 0; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ g_0; + */ +void h(int x) +{ + /*@ ghost h_pre_func(x); */ + /*@ ghost h_post_func(); */ + return; +} + +/*@ ghost + /@ requires aorai_CurStates ≡ g_0; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_i; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_in: + assumes aorai_CurStates ≡ g_0; + ensures aorai_CurStates ≡ h_0; + + behavior buch_state_h_0_out: + assumes aorai_CurStates ≢ g_0; + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void i_pre_func(void) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_i; + if (6 == aorai_CurStates) aorai_CurStates = h_0; + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ h_0; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_i; + assigns aorai_y, aorai_x, aorai_CurOpStatus, aorai_CurOperation, + aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_in_0: + assumes aorai_CurStates ≡ h_0; + ensures aorai_CurStates ≡ e; + ensures aorai_y ≡ 0; + ensures aorai_x ≡ 1; + + behavior buch_state_e_out: + assumes aorai_CurStates ≢ h_0; + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + + behavior aorai_y_unchanged_0: + assumes aorai_CurStates ≢ h_0; + ensures aorai_y ≡ \old(aorai_y); + + behavior aorai_x_unchanged_0: + assumes aorai_CurStates ≢ h_0; + ensures aorai_x ≡ \old(aorai_x); + @/ + void i_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_i; + if (7 == aorai_CurStates) { + aorai_CurStates = e; + aorai_y = 0; + aorai_x = 1; + } + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ g_0; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ e; + ensures + \at(aorai_CurStates ≡ g_0,Pre) ∧ aorai_CurStates ≡ e ⇒ + aorai_y ≡ 0; + ensures + \at(aorai_CurStates ≡ g_0,Pre) ∧ aorai_CurStates ≡ e ⇒ + aorai_x ≡ \at(1,Pre) + 0; + */ +void i(void) +{ + /*@ ghost i_pre_func(); */ + /*@ ghost i_post_func(); */ + return; +} + +/*@ ghost + /@ requires aorai_CurStates ≡ a; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_main; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_in: + assumes aorai_CurStates ≡ a; + ensures aorai_CurStates ≡ b; + + behavior buch_state_b_out: + assumes aorai_CurStates ≢ a; + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_out: + ensures aorai_CurStates ≢ i_0; + @/ + void main_pre_func(int t) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_main; + if (0 == aorai_CurStates) aorai_CurStates = b; + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ e; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_main; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior buch_state_d_out: + ensures aorai_CurStates ≢ d; + + behavior buch_state_e_out: + ensures aorai_CurStates ≢ e; + + behavior buch_state_f_0_out: + ensures aorai_CurStates ≢ f_0; + + behavior buch_state_g_0_out: + ensures aorai_CurStates ≢ g_0; + + behavior buch_state_h_0_out: + ensures aorai_CurStates ≢ h_0; + + behavior buch_state_i_0_in: + assumes aorai_CurStates ≡ e; + ensures aorai_CurStates ≡ i_0; + + behavior buch_state_i_0_out: + assumes aorai_CurStates ≢ e; + ensures aorai_CurStates ≢ i_0; + @/ + void main_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_main; + if (4 == aorai_CurStates) aorai_CurStates = i_0; + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ a; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ i_0; + ensures + \at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ i_0 ⇒ + aorai_y ≡ 0 ∨ aorai_y ≡ \at(aorai_x,Pre) + 0; + ensures + \at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ i_0 ⇒ + aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at((int)42,Pre) + 0; + */ +void main(int t) +{ + /*@ ghost int aorai_Loop_Init_15; */ + /*@ ghost main_pre_func(t); */ + if (t) f(42); + else { + g(); + goto L; + } + int x = 0; + /*@ ghost aorai_Loop_Init_15 = 1; */ + aorai_loop_15: + /*@ loop invariant Aorai: aorai_CurStates ≢ a; + loop invariant Aorai: aorai_CurStates ≢ b; + loop invariant Aorai: aorai_CurStates ≢ c; + loop invariant Aorai: aorai_CurStates ≢ d; + loop invariant Aorai: aorai_CurStates ≡ e; + loop invariant Aorai: aorai_CurStates ≢ f_0; + loop invariant Aorai: aorai_CurStates ≢ g_0; + loop invariant Aorai: aorai_CurStates ≢ h_0; + loop invariant Aorai: aorai_CurStates ≢ i_0; + loop invariant + Aorai: + \at(aorai_CurStates ≡ e,aorai_loop_15) ∧ aorai_CurStates ≡ e ⇒ + aorai_y ≡ 0; + loop invariant + Aorai: + \at(aorai_CurStates ≡ e,aorai_loop_15) ∧ aorai_CurStates ≡ e ⇒ + aorai_x ≡ \at(1,Pre) + 0; + */ + while (x < 100) { + /*@ ghost aorai_Loop_Init_15 = 0; */ + h(x); + L: i(); + x ++; + } + /*@ ghost main_post_func(); */ + return; +} + + diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..44c1487fcf7693e627a38f17cea95e7cd8e7b492 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle @@ -0,0 +1,5 @@ +[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0: + { (Call(h)) and ((aorai_x) > (0)) } +[kernel] Plug-in aorai aborted: invalid user input. diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle index 5df73b9c95c31edffe2319c7c773b93acfa13b23..86ceb3e991278c964faf62706c167f6710087817 100644 --- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle @@ -64,14 +64,11 @@ check lemma Init_deterministic_trans{L}: @/ void f_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (2 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject; + if (2 == aorai_CurStates) aorai_CurStates = aorai_reject; else - if (1 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject; - aorai_CurStates = aorai_CurStates_tmp; + if (1 == aorai_CurStates) aorai_CurStates = aorai_reject; return; } @@ -99,12 +96,9 @@ check lemma Init_deterministic_trans{L}: @/ void f_post_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_f; - aorai_CurStates_tmp = aorai_CurStates; - if (2 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject; - aorai_CurStates = aorai_CurStates_tmp; + if (2 == aorai_CurStates) aorai_CurStates = aorai_reject; return; } @@ -145,11 +139,8 @@ void f(void) @/ void main_pre_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Called; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - aorai_CurStates = aorai_CurStates_tmp; return; } @@ -172,11 +163,8 @@ void f(void) @/ void main_post_func(void) { - int aorai_CurStates_tmp; aorai_CurOpStatus = aorai_Terminated; aorai_CurOperation = op_main; - aorai_CurStates_tmp = aorai_CurStates; - aorai_CurStates = aorai_CurStates_tmp; return; } diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle index fb6b465a2256fcbac162429a15459d215ef802d0..1d964840b06fc2869b27dc1f9ff1115c052861fc 100644 --- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle @@ -39,9 +39,7 @@ enum aorai_OpStatusList { aorai_CurOperation = op_f; S0_tmp = S0; Sf_tmp = Sf; - if (S0 == 1) - if (x >= 4) Sf_tmp = 1; else Sf_tmp = 0; - else Sf_tmp = 0; + if (S0 == 1 && x >= 4) Sf_tmp = 1; else Sf_tmp = 0; S0_tmp = 0; S0 = S0_tmp; Sf = Sf_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle index 80809ada84f52d13998c0490ccf20da3bad3ce0f..8f230ecadb224c890456d0ef3ef0415fa9db4e9a 100644 --- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle @@ -65,42 +65,13 @@ int x = 0; init_tmp = init; last_tmp = last; step1_tmp = step1; - if (init == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (last == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (step1 == 1) - if (x != 4) step1_tmp = 1; else step1_tmp = 0; - else step1_tmp = 0; - } - } - if (last == 1) { - if (x != 4) { - if (x != 3) last_tmp = 1; else goto _LAND_1; - } - else goto _LAND_1; - } - else { - _LAND_1: ; - if (step1 == 1) - if (x == 4) last_tmp = 1; else last_tmp = 0; - else last_tmp = 0; - } - if (init == 1) { - if (x != 3) init_tmp = 1; else goto _LAND_2; - } - else { - _LAND_2: ; - if (last == 1) - if (x == 4) init_tmp = 1; else init_tmp = 0; - else init_tmp = 0; - } + if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) + step1_tmp = 1; + else step1_tmp = 0; + if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1; + else last_tmp = 0; + if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1; + else init_tmp = 0; init = init_tmp; last = last_tmp; step1 = step1_tmp; @@ -157,42 +128,13 @@ int x = 0; init_tmp = init; last_tmp = last; step1_tmp = step1; - if (init == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (last == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (step1 == 1) - if (x != 4) step1_tmp = 1; else step1_tmp = 0; - else step1_tmp = 0; - } - } - if (last == 1) { - if (x != 4) { - if (x != 3) last_tmp = 1; else goto _LAND_1; - } - else goto _LAND_1; - } - else { - _LAND_1: ; - if (step1 == 1) - if (x == 4) last_tmp = 1; else last_tmp = 0; - else last_tmp = 0; - } - if (init == 1) { - if (x != 3) init_tmp = 1; else goto _LAND_2; - } - else { - _LAND_2: ; - if (last == 1) - if (x == 4) init_tmp = 1; else init_tmp = 0; - else init_tmp = 0; - } + if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) + step1_tmp = 1; + else step1_tmp = 0; + if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1; + else last_tmp = 0; + if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1; + else init_tmp = 0; init = init_tmp; last = last_tmp; step1 = step1_tmp; @@ -313,42 +255,13 @@ void f(void) init_tmp = init; last_tmp = last; step1_tmp = step1; - if (init == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (last == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (step1 == 1) - if (x != 4) step1_tmp = 1; else step1_tmp = 0; - else step1_tmp = 0; - } - } - if (last == 1) { - if (x != 4) { - if (x != 3) last_tmp = 1; else goto _LAND_1; - } - else goto _LAND_1; - } - else { - _LAND_1: ; - if (step1 == 1) - if (x == 4) last_tmp = 1; else last_tmp = 0; - else last_tmp = 0; - } - if (init == 1) { - if (x != 3) init_tmp = 1; else goto _LAND_2; - } - else { - _LAND_2: ; - if (last == 1) - if (x == 4) init_tmp = 1; else init_tmp = 0; - else init_tmp = 0; - } + if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) + step1_tmp = 1; + else step1_tmp = 0; + if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1; + else last_tmp = 0; + if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1; + else init_tmp = 0; init = init_tmp; last = last_tmp; step1 = step1_tmp; @@ -405,42 +318,13 @@ void f(void) init_tmp = init; last_tmp = last; step1_tmp = step1; - if (init == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (last == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (step1 == 1) - if (x != 4) step1_tmp = 1; else step1_tmp = 0; - else step1_tmp = 0; - } - } - if (last == 1) { - if (x != 4) { - if (x != 3) last_tmp = 1; else goto _LAND_1; - } - else goto _LAND_1; - } - else { - _LAND_1: ; - if (step1 == 1) - if (x == 4) last_tmp = 1; else last_tmp = 0; - else last_tmp = 0; - } - if (init == 1) { - if (x != 3) init_tmp = 1; else goto _LAND_2; - } - else { - _LAND_2: ; - if (last == 1) - if (x == 4) init_tmp = 1; else init_tmp = 0; - else init_tmp = 0; - } + if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) + step1_tmp = 1; + else step1_tmp = 0; + if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1; + else last_tmp = 0; + if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1; + else init_tmp = 0; init = init_tmp; last = last_tmp; step1 = step1_tmp; @@ -548,13 +432,9 @@ void g(void) init_tmp = init; last_tmp = last; step1_tmp = step1; - if (init == 1) - if (x == 3) step1_tmp = 1; else step1_tmp = 0; - else step1_tmp = 0; + if (init == 1 && x == 3) step1_tmp = 1; else step1_tmp = 0; last_tmp = 0; - if (init == 1) - if (x != 3) init_tmp = 1; else init_tmp = 0; - else init_tmp = 0; + if (init == 1 && x != 3) init_tmp = 1; else init_tmp = 0; init = init_tmp; last = last_tmp; step1 = step1_tmp; @@ -611,42 +491,13 @@ void g(void) init_tmp = init; last_tmp = last; step1_tmp = step1; - if (init == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (last == 1) { - if (x == 3) step1_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (step1 == 1) - if (x != 4) step1_tmp = 1; else step1_tmp = 0; - else step1_tmp = 0; - } - } - if (last == 1) { - if (x != 4) { - if (x != 3) last_tmp = 1; else goto _LAND_1; - } - else goto _LAND_1; - } - else { - _LAND_1: ; - if (step1 == 1) - if (x == 4) last_tmp = 1; else last_tmp = 0; - else last_tmp = 0; - } - if (init == 1) { - if (x != 3) init_tmp = 1; else goto _LAND_2; - } - else { - _LAND_2: ; - if (last == 1) - if (x == 4) init_tmp = 1; else init_tmp = 0; - else init_tmp = 0; - } + if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) + step1_tmp = 1; + else step1_tmp = 0; + if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1; + else last_tmp = 0; + if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1; + else init_tmp = 0; init = init_tmp; last = last_tmp; step1 = step1_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle index ef2675cd7f075668a39ea9d309c2c53fe921c317..506dca121a3f23b957ced47740eee807cff752ec 100644 --- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle @@ -253,6 +253,11 @@ void f(void) (0 ≡ aorai_intermediate_state_2 ∨ ¬(aorai_counter < 2)) ∧ 0 ≡ aorai_intermediate_state_0 ∧ 0 ≡ aorai_intermediate_state; ensures 0 ≡ aorai_intermediate_state_3; + + behavior aorai_counter_unchanged: + assumes 0 ≡ aorai_intermediate_state; + assumes 0 ≡ aorai_intermediate_state_0; + assumes 0 ≡ aorai_intermediate_state_2 ∨ ¬(aorai_counter < 2); ensures aorai_counter ≡ \old(aorai_counter); @/ void g_pre_func(void) @@ -273,16 +278,10 @@ void f(void) aorai_intermediate_state_1_tmp = aorai_intermediate_state_1; aorai_intermediate_state_2_tmp = aorai_intermediate_state_2; aorai_intermediate_state_3_tmp = aorai_intermediate_state_3; - if (aorai_intermediate_state == 1) aorai_intermediate_state_3_tmp = 1; - else - if (aorai_intermediate_state_0 == 1) aorai_intermediate_state_3_tmp = 1; - else - if (aorai_intermediate_state_2 == 1) - if (aorai_counter < 2) aorai_intermediate_state_3_tmp = 1; - else aorai_intermediate_state_3_tmp = 0; - else aorai_intermediate_state_3_tmp = 0; - if (aorai_intermediate_state_2 == 1) - if (aorai_counter < 2) aorai_counter ++; + if ((aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1) || + aorai_intermediate_state_2 == 1 && aorai_counter < 2) aorai_intermediate_state_3_tmp = 1; + else aorai_intermediate_state_3_tmp = 0; + if (aorai_intermediate_state_2 == 1 && aorai_counter < 2) aorai_counter ++; if (aorai_intermediate_state_0 == 1) aorai_counter = 1; if (aorai_intermediate_state == 1) aorai_counter = 1; aorai_intermediate_state_2_tmp = 0; @@ -563,8 +562,7 @@ void g(void) aorai_intermediate_state_1_tmp = 0; aorai_intermediate_state_0_tmp = 0; aorai_intermediate_state_tmp = 0; - if (aorai_intermediate_state_2 == 1) - if (1 <= aorai_counter) Sf_tmp = 1; else Sf_tmp = 0; + if (aorai_intermediate_state_2 == 1 && 1 <= aorai_counter) Sf_tmp = 1; else Sf_tmp = 0; S0_tmp = 0; S0 = S0_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle index 3e600a02555ac40005422af1968c929809712c56..91097fdf88b9aa56ad5e7d32f14521e41cb9cbd8 100644 --- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle @@ -63,13 +63,17 @@ enum aorai_OpStatusList { (0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5)) ∧ 0 ≡ aorai_intermediate_state; ensures 0 ≡ aorai_intermediate_state_1; - ensures aorai_counter ≡ \old(aorai_counter); behavior buch_state_aorai_intermediate_state_2_out: ensures 0 ≡ aorai_intermediate_state_2; behavior buch_state_aorai_intermediate_state_3_out: ensures 0 ≡ aorai_intermediate_state_3; + + behavior aorai_counter_unchanged: + assumes 0 ≡ aorai_intermediate_state; + assumes 0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5); + ensures aorai_counter ≡ \old(aorai_counter); @/ void f_pre_func(void) { @@ -91,14 +95,10 @@ enum aorai_OpStatusList { aorai_intermediate_state_3_tmp = aorai_intermediate_state_3; aorai_intermediate_state_3_tmp = 0; aorai_intermediate_state_2_tmp = 0; - if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1; - else - if (aorai_intermediate_state_0 == 1) - if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1; - else aorai_intermediate_state_1_tmp = 0; - else aorai_intermediate_state_1_tmp = 0; - if (aorai_intermediate_state_0 == 1) - if (aorai_counter < 5) aorai_counter ++; + if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 && + aorai_counter < 5) aorai_intermediate_state_1_tmp = 1; + else aorai_intermediate_state_1_tmp = 0; + if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++; if (aorai_intermediate_state == 1) aorai_counter = 1; aorai_intermediate_state_0_tmp = 0; aorai_intermediate_state_tmp = 0; @@ -539,9 +539,9 @@ void g(void) aorai_intermediate_state_1_tmp = 0; aorai_intermediate_state_0_tmp = 0; aorai_intermediate_state_tmp = 0; - if (aorai_intermediate_state == 1) Sf_tmp = 1; - else - if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0; + if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1) + Sf_tmp = 1; + else Sf_tmp = 0; S0_tmp = 0; S0 = S0_tmp; Sf = Sf_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..47bd37cf3ee9430554f51b2119e5f95c25f49990 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle @@ -0,0 +1,140 @@ +[kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing) +/* Generated by Frama-C */ +enum aorai_States { + aorai_reject_state = -2, + a = 0, + b = 1, + c = 2 +}; +enum aorai_ListOper { + op_main = 0 +}; +enum aorai_OpStatusList { + aorai_Terminated = 1, + aorai_Called = 0 +}; +/*@ check lemma c_deterministic_trans{L}: \true; + */ +/*@ check lemma b_deterministic_trans{L}: \true; + */ +/*@ check lemma a_deterministic_trans{L}: \true; + */ +/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */ +/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */ +/*@ ghost int aorai_CurStates = a; */ +/*@ ghost int aorai_x = 0; */ +/*@ ghost int aorai_y = 0; */ +/*@ ghost + /@ requires aorai_CurStates ≡ a; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_main; + assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation, + aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_in_0: + assumes aorai_CurStates ≡ a; + ensures aorai_CurStates ≡ b; + ensures aorai_x ≡ \old(*x); + ensures aorai_y ≡ \old(*y); + + behavior buch_state_b_out: + assumes aorai_CurStates ≢ a; + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_out: + ensures aorai_CurStates ≢ c; + + behavior aorai_y_unchanged: + assumes aorai_CurStates ≢ a; + ensures aorai_y ≡ \old(aorai_y); + + behavior aorai_x_unchanged: + assumes aorai_CurStates ≢ a; + ensures aorai_x ≡ \old(aorai_x); + @/ + void main_pre_func(int *x, int *y) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_main; + if (0 == aorai_CurStates) { + aorai_CurStates = b; + aorai_x = *x; + aorai_y = *y; + } + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ b; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_main; + assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation, + aorai_CurStates; + + behavior buch_state_a_out: + ensures aorai_CurStates ≢ a; + + behavior buch_state_b_out: + ensures aorai_CurStates ≢ b; + + behavior buch_state_c_in_0: + assumes aorai_CurStates ≡ b; + ensures aorai_CurStates ≡ c; + ensures aorai_x ≡ \old(aorai_y); + ensures aorai_y ≡ aorai_x; + + behavior buch_state_c_out: + assumes aorai_CurStates ≢ b; + ensures aorai_CurStates ≢ c; + + behavior aorai_y_unchanged_0: + assumes aorai_CurStates ≢ b; + ensures aorai_y ≡ \old(aorai_y); + + behavior aorai_x_unchanged_0: + assumes aorai_CurStates ≢ b; + ensures aorai_x ≡ \old(aorai_x); + @/ + void main_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_main; + if (1 == aorai_CurStates) { + aorai_CurStates = c; + aorai_x = aorai_y; + aorai_y = aorai_x; + } + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ a; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ c; + ensures + \at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ c ⇒ + aorai_y ≡ \at(*x,Pre) + 0; + ensures + \at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ c ⇒ + aorai_x ≡ \at(*y,Pre) + 0; + */ +void main(int *x, int *y) +{ + /*@ ghost main_pre_func(x,y); */ + int t = *x; + *x = *y; + *y = t; + /*@ ghost main_post_func(); */ + return; +} + + diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..a24943fca9867c96902f607deaafe3a12f1a2e71 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle @@ -0,0 +1,6 @@ +[kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The metavariable aorai_x is assigned several times during the transition from a to b: + { Call(main) } aorai_x <- x + aorai_x <- aorai_x + 1 +[kernel] Plug-in aorai aborted: invalid user input. diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6ca094fa00c5447876ad01b5e9f2b6297b9ecbcd --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle @@ -0,0 +1,412 @@ +[kernel] Parsing tests/ya/stack.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing) +/* Generated by Frama-C */ +enum aorai_States { + aorai_reject_state = -2, + accept = 0, + empty_stack = 1, + emptying_stack = 2, + filled_stack = 3, + filling_stack = 4, + init = 5 +}; +enum aorai_ListOper { + op_main = 2, + op_pop = 1, + op_push = 0 +}; +enum aorai_OpStatusList { + aorai_Terminated = 1, + aorai_Called = 0 +}; +/*@ check lemma init_deterministic_trans{L}: \true; + */ +/*@ check lemma filling_stack_deterministic_trans{L}: \true; + */ +/*@ check lemma accept_deterministic_trans{L}: \true; + */ +int g = 0; +/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */ +/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */ +/*@ +check lemma empty_stack_deterministic_trans{L}: + ¬(\at(aorai_CurOperation,L) ≡ op_push ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ + \at(aorai_CurOperation,L) ≡ op_main ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Terminated); + */ +/*@ ghost int aorai_CurStates = init; */ +/*@ ghost int aorai_n = 0; */ +/*@ +check lemma filled_stack_deterministic_trans{L}: + ¬(\at(aorai_CurOperation,L) ≡ op_pop ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ \at(aorai_n,L) > 0 ∧ + \at(aorai_CurOperation,L) ≡ op_push ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Called); + */ +/*@ +check lemma emptying_stack_deterministic_trans{L}: + ¬(\at(aorai_CurOperation,L) ≡ op_pop ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ + \at(aorai_n,L) ≡ 1 ∧ \at(aorai_CurOperation,L) ≡ op_pop ∧ + \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_n,L) > 1); + */ +/*@ ghost + /@ requires + aorai_CurStates ≡ empty_stack ∨ aorai_CurStates ≡ filled_stack; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_push; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_accept_out: + ensures aorai_CurStates ≢ accept; + + behavior buch_state_empty_stack_out: + ensures aorai_CurStates ≢ empty_stack; + + behavior buch_state_emptying_stack_out: + ensures aorai_CurStates ≢ emptying_stack; + + behavior buch_state_filled_stack_out: + ensures aorai_CurStates ≢ filled_stack; + + behavior buch_state_filling_stack_in: + assumes + aorai_CurStates ≡ filled_stack ∨ aorai_CurStates ≡ empty_stack; + ensures aorai_CurStates ≡ filling_stack; + + behavior buch_state_filling_stack_out: + assumes + aorai_CurStates ≢ filled_stack ∧ aorai_CurStates ≢ empty_stack; + ensures aorai_CurStates ≢ filling_stack; + + behavior buch_state_init_out: + ensures aorai_CurStates ≢ init; + @/ + void push_pre_func(void) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_push; + if (3 == aorai_CurStates) aorai_CurStates = filling_stack; + else + if (1 == aorai_CurStates) aorai_CurStates = filling_stack; + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ filling_stack; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_push; + assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_accept_out: + ensures aorai_CurStates ≢ accept; + + behavior buch_state_empty_stack_out: + ensures aorai_CurStates ≢ empty_stack; + + behavior buch_state_emptying_stack_out: + ensures aorai_CurStates ≢ emptying_stack; + + behavior buch_state_filled_stack_in_0: + assumes aorai_CurStates ≡ filling_stack; + ensures aorai_CurStates ≡ filled_stack; + ensures aorai_n ≡ \old(aorai_n) + 1; + + behavior buch_state_filled_stack_out: + assumes aorai_CurStates ≢ filling_stack; + ensures aorai_CurStates ≢ filled_stack; + + behavior buch_state_filling_stack_out: + ensures aorai_CurStates ≢ filling_stack; + + behavior buch_state_init_out: + ensures aorai_CurStates ≢ init; + + behavior aorai_n_unchanged: + assumes aorai_CurStates ≢ filling_stack; + assumes aorai_CurStates ≢ filling_stack; + ensures aorai_n ≡ \old(aorai_n); + @/ + void push_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_push; + if (4 == aorai_CurStates) { + aorai_CurStates = filled_stack; + aorai_n ++; + } + return; + } + +*/ + +/*@ requires + aorai_CurStates ≡ empty_stack ∨ aorai_CurStates ≡ filled_stack; + requires + aorai_CurStates ≡ filled_stack ∨ aorai_CurStates ≢ filled_stack; + requires + aorai_CurStates ≡ empty_stack ∨ aorai_CurStates ≢ empty_stack; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ filled_stack; + ensures + \at(aorai_CurStates ≡ filled_stack,Pre) ∧ + aorai_CurStates ≡ filled_stack ⇒ + aorai_n ≡ \at(aorai_n + 1,Pre) + 0; + ensures + \at(aorai_CurStates ≡ empty_stack,Pre) ∧ + aorai_CurStates ≡ filled_stack ⇒ + aorai_n ≡ \at(aorai_n + 1,Pre) + 0; + */ +void push(void) +{ + /*@ ghost push_pre_func(); */ + g ++; + /*@ ghost push_post_func(); */ + return; +} + +/*@ ghost + /@ requires aorai_CurStates ≡ filled_stack; + requires aorai_CurStates ≡ filled_stack ⇒ aorai_n > 0; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_pop; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_accept_out: + ensures aorai_CurStates ≢ accept; + + behavior buch_state_empty_stack_out: + ensures aorai_CurStates ≢ empty_stack; + + behavior buch_state_emptying_stack_in: + assumes aorai_CurStates ≡ filled_stack ∧ aorai_n > 0; + ensures aorai_CurStates ≡ emptying_stack; + + behavior buch_state_emptying_stack_out: + assumes aorai_CurStates ≢ filled_stack ∨ ¬(aorai_n > 0); + ensures aorai_CurStates ≢ emptying_stack; + + behavior buch_state_filled_stack_out: + ensures aorai_CurStates ≢ filled_stack; + + behavior buch_state_filling_stack_out: + ensures aorai_CurStates ≢ filling_stack; + + behavior buch_state_init_out: + ensures aorai_CurStates ≢ init; + @/ + void pop_pre_func(void) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_pop; + if (3 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack; + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ emptying_stack; + requires + aorai_CurStates ≡ emptying_stack ⇒ aorai_n > 1 ∨ aorai_n ≡ 1; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_pop; + assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_accept_out: + ensures aorai_CurStates ≢ accept; + + behavior buch_state_empty_stack_in_0: + assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n ≡ 1; + ensures aorai_CurStates ≡ empty_stack; + ensures aorai_n ≡ \old(aorai_n) - 1; + + behavior buch_state_empty_stack_out: + assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n ≡ 1); + ensures aorai_CurStates ≢ empty_stack; + + behavior buch_state_emptying_stack_out: + ensures aorai_CurStates ≢ emptying_stack; + + behavior buch_state_filled_stack_in_0: + assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n > 1; + ensures aorai_CurStates ≡ filled_stack; + ensures aorai_n ≡ \old(aorai_n) - 1; + + behavior buch_state_filled_stack_out: + assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n > 1); + ensures aorai_CurStates ≢ filled_stack; + + behavior buch_state_filling_stack_out: + ensures aorai_CurStates ≢ filling_stack; + + behavior buch_state_init_out: + ensures aorai_CurStates ≢ init; + + behavior aorai_n_unchanged_0: + assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n > 1); + assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n ≡ 1); + ensures aorai_n ≡ \old(aorai_n); + @/ + void pop_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_pop; + if (2 == aorai_CurStates && aorai_n == 1) { + aorai_CurStates = empty_stack; + aorai_n --; + } + else + if (2 == aorai_CurStates && aorai_n > 1) { + aorai_CurStates = filled_stack; + aorai_n --; + } + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ filled_stack; + requires aorai_CurStates ≡ filled_stack ⇒ aorai_n > 0; + + behavior Buchi_property_behavior: + ensures + (aorai_CurStates ≡ empty_stack ⇒ aorai_n ≡ 1) ∧ + (aorai_CurStates ≡ filled_stack ⇒ aorai_n > 1); + ensures + aorai_CurStates ≡ empty_stack ∨ aorai_CurStates ≡ filled_stack; + ensures + \at(aorai_CurStates ≡ filled_stack,Pre) ∧ + aorai_CurStates ≡ filled_stack ⇒ + aorai_n ≡ \at(aorai_n - 1,Pre) + 0; + ensures + \at(aorai_CurStates ≡ filled_stack,Pre) ∧ + aorai_CurStates ≡ empty_stack ⇒ + aorai_n ≡ \at(aorai_n - 1,Pre) + 0; + */ +void pop(void) +{ + /*@ ghost pop_pre_func(); */ + /*@ assert g > 0; */ ; + g --; + /*@ ghost pop_post_func(); */ + return; +} + +/*@ ghost + /@ requires aorai_CurStates ≡ init; + ensures aorai_CurOpStatus ≡ aorai_Called; + ensures aorai_CurOperation ≡ op_main; + assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_accept_out: + ensures aorai_CurStates ≢ accept; + + behavior buch_state_empty_stack_in_0: + assumes aorai_CurStates ≡ init; + ensures aorai_CurStates ≡ empty_stack; + ensures aorai_n ≡ 0; + + behavior buch_state_empty_stack_out: + assumes aorai_CurStates ≢ init; + ensures aorai_CurStates ≢ empty_stack; + + behavior buch_state_emptying_stack_out: + ensures aorai_CurStates ≢ emptying_stack; + + behavior buch_state_filled_stack_out: + ensures aorai_CurStates ≢ filled_stack; + + behavior buch_state_filling_stack_out: + ensures aorai_CurStates ≢ filling_stack; + + behavior buch_state_init_out: + ensures aorai_CurStates ≢ init; + + behavior aorai_n_unchanged_1: + assumes aorai_CurStates ≢ init; + ensures aorai_n ≡ \old(aorai_n); + @/ + void main_pre_func(void) + { + aorai_CurOpStatus = aorai_Called; + aorai_CurOperation = op_main; + if (5 == aorai_CurStates) { + aorai_CurStates = empty_stack; + aorai_n = 0; + } + return; + } + +*/ + +/*@ ghost + /@ requires aorai_CurStates ≡ empty_stack; + ensures aorai_CurOpStatus ≡ aorai_Terminated; + ensures aorai_CurOperation ≡ op_main; + assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; + + behavior buch_state_accept_in: + assumes aorai_CurStates ≡ empty_stack; + ensures aorai_CurStates ≡ accept; + + behavior buch_state_accept_out: + assumes aorai_CurStates ≢ empty_stack; + ensures aorai_CurStates ≢ accept; + + behavior buch_state_empty_stack_out: + ensures aorai_CurStates ≢ empty_stack; + + behavior buch_state_emptying_stack_out: + ensures aorai_CurStates ≢ emptying_stack; + + behavior buch_state_filled_stack_out: + ensures aorai_CurStates ≢ filled_stack; + + behavior buch_state_filling_stack_out: + ensures aorai_CurStates ≢ filling_stack; + + behavior buch_state_init_out: + ensures aorai_CurStates ≢ init; + @/ + void main_post_func(void) + { + aorai_CurOpStatus = aorai_Terminated; + aorai_CurOperation = op_main; + if (1 == aorai_CurStates) aorai_CurStates = accept; + return; + } + +*/ + +/*@ requires aorai_CurStates ≡ init; + + behavior Buchi_property_behavior: + ensures aorai_CurStates ≡ accept; + ensures + \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ accept ⇒ + aorai_n ≡ \at(aorai_n - 1,Pre) + 0; + */ +void main(void) +{ + /*@ ghost main_pre_func(); */ + push(); + pop(); + push(); + push(); + pop(); + push(); + push(); + pop(); + pop(); + pop(); + /*@ ghost main_post_func(); */ + return; +} + + diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle index 2f0841a21006211b9a4f313bf10bf689d197d285..89553036d1a684d71bccedc4dc525fe7dbcb2ed1 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle @@ -76,9 +76,7 @@ int rr = 1; SF_tmp = 0; S4_tmp = 0; S3_tmp = 0; - if (S1 == 1) - if (i >= 0) S2_tmp = 1; else S2_tmp = 0; - else S2_tmp = 0; + if (S1 == 1 && i >= 0) S2_tmp = 1; else S2_tmp = 0; S1_tmp = 0; S1 = S1_tmp; S2 = S2_tmp; @@ -293,9 +291,7 @@ void opa(int i, int j) SF_tmp = SF; mainst_tmp = mainst; mainst_tmp = 0; - if (S4 == 1) - if (res > 0) SF_tmp = 1; else SF_tmp = 0; - else SF_tmp = 0; + if (S4 == 1 && res > 0) SF_tmp = 1; else SF_tmp = 0; S4_tmp = 0; S3_tmp = 0; S2_tmp = 0; diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle index 14191d7f00b8e8d5cd13f1a5f7842b00c44a3c4b..16997723976399ec7e581375b99d0be6dc37e33e 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle @@ -82,9 +82,7 @@ int rr = 1; S6_tmp = 0; S5_tmp = 0; S4_tmp = 0; - if (S2 == 1) - if (r >= 0) S3_tmp = 1; else S3_tmp = 0; - else S3_tmp = 0; + if (S2 == 1 && r >= 0) S3_tmp = 1; else S3_tmp = 0; S2_tmp = 0; S1_tmp = 0; S1 = S1_tmp; @@ -156,9 +154,7 @@ int rr = 1; S7_tmp = 0; S6_tmp = 0; S5_tmp = 0; - if (S3 == 1) - if (res <= 5000) S4_tmp = 1; else S4_tmp = 0; - else S4_tmp = 0; + if (S3 == 1 && res <= 5000) S4_tmp = 1; else S4_tmp = 0; S3_tmp = 0; S2_tmp = 0; S1_tmp = 0; diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle index 862eecf00b3d95eabb6ff90430a634d16d8f3a2d..6bd1a0b39b8010458503b8e83ae36ac33f416ecf 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle @@ -97,13 +97,9 @@ enum aorai_OpStatusList { End_tmp = End; Idle_tmp = Idle; WillDoFoo_tmp = WillDoFoo; - if (Idle == 1) - if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0; - else WillDoFoo_tmp = 0; + if (Idle == 1 && res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0; Idle_tmp = 0; - if (Idle == 1) - if (res != -1) End_tmp = 1; else End_tmp = 0; - else End_tmp = 0; + if (Idle == 1 && res != -1) End_tmp = 1; else End_tmp = 0; End = End_tmp; Idle = Idle_tmp; WillDoFoo = WillDoFoo_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle index d3c59bb4befd891ca4a21f07b24c760adc8df894..43699ce9ec7abf7b39c5d535b758c4b7e908d813 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle @@ -216,9 +216,7 @@ int decode_int(char *s) S2_tmp = S2; main_0_tmp = main_0; main_0_tmp = 0; - if (S1 == 1) S2_tmp = 1; - else - if (S2 == 1) S2_tmp = 1; else S2_tmp = 0; + if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0; S1_tmp = 0; S1 = S1_tmp; S2 = S2_tmp; @@ -264,12 +262,8 @@ int decode_int(char *s) S2_tmp = S2; main_0_tmp = main_0; main_0_tmp = 0; - if (S1 == 1) S2_tmp = 1; - else - if (S2 == 1) S2_tmp = 1; else S2_tmp = 0; - if (S1 == 1) S1_tmp = 1; - else - if (S2 == 1) S1_tmp = 1; else S1_tmp = 0; + if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0; + if (S1 == 1 || S2 == 1) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; S2 = S2_tmp; main_0 = main_0_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle index 6652049d8dd0807628419b6c351661b2da4ea857..cdfe4aba74bff1e589436adad382f28f9967766a 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle @@ -100,25 +100,11 @@ enum aorai_OpStatusList { End_tmp = End; Idle_tmp = Idle; WillDoFoo_tmp = WillDoFoo; - if (Idle == 1) { - if (res == -1) WillDoFoo_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (WillDoFoo == 1) - if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0; - else WillDoFoo_tmp = 0; - } + if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1; + else WillDoFoo_tmp = 0; Idle_tmp = 0; - if (End == 1) { - if (res != -1) End_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (Idle == 1) - if (res != -1) End_tmp = 1; else End_tmp = 0; - else End_tmp = 0; - } + if (End == 1 && res != -1 || Idle == 1 && res != -1) End_tmp = 1; + else End_tmp = 0; End = End_tmp; Idle = Idle_tmp; WillDoFoo = WillDoFoo_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle index 059961889707d7edefa1fd55d1593761b0b071c2..bc9334eec11d7af2e8fcb00eb21f5fb24d1a832f 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle @@ -123,24 +123,10 @@ enum aorai_OpStatusList { Idle_tmp = Idle; IgnoreFoo_tmp = IgnoreFoo; WillDoFoo_tmp = WillDoFoo; - if (Idle == 1) { - if (res == -1) WillDoFoo_tmp = 1; else goto _LAND; - } - else { - _LAND: ; - if (WillDoFoo == 1) - if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0; - else WillDoFoo_tmp = 0; - } - if (Idle == 1) { - if (res != -1) IgnoreFoo_tmp = 1; else goto _LAND_0; - } - else { - _LAND_0: ; - if (IgnoreFoo == 1) - if (res != -1) IgnoreFoo_tmp = 1; else IgnoreFoo_tmp = 0; - else IgnoreFoo_tmp = 0; - } + if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1; + else WillDoFoo_tmp = 0; + if (Idle == 1 && res != -1 || IgnoreFoo == 1 && res != -1) IgnoreFoo_tmp = 1; + else IgnoreFoo_tmp = 0; Idle_tmp = 0; End_tmp = 0; End = End_tmp; @@ -292,14 +278,11 @@ int isPresentRec(int *t, int i, int max, int val) Idle_tmp = Idle; IgnoreFoo_tmp = IgnoreFoo; WillDoFoo_tmp = WillDoFoo; - if (WillDoFoo == 1) - if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0; + if (WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0; IgnoreFoo_tmp = 0; Idle_tmp = 0; - if (IgnoreFoo == 1) - if (res != -1) End_tmp = 1; else End_tmp = 0; - else End_tmp = 0; + if (IgnoreFoo == 1 && res != -1) End_tmp = 1; else End_tmp = 0; End = End_tmp; Idle = Idle_tmp; IgnoreFoo = IgnoreFoo_tmp; diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle index 0916e902014b3cb6b3c85b722d2a0b894c791b12..0e102ceda9633ce37d9262207c569e610ce0a69b 100644 --- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle @@ -47,9 +47,7 @@ int myAge = 0; S1_tmp = S1; main_0_tmp = main_0; main_0_tmp = 0; - if (S1 == 1) - if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0; - else S1_tmp = 0; + if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; main_0 = main_0_tmp; return; @@ -84,9 +82,7 @@ int myAge = 0; S1_tmp = S1; main_0_tmp = main_0; main_0_tmp = 0; - if (S1 == 1) - if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0; - else S1_tmp = 0; + if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; main_0 = main_0_tmp; return; @@ -138,9 +134,7 @@ void increment(void) S1_tmp = S1; main_0_tmp = main_0; main_0_tmp = 0; - if (main_0 == 1) - if (nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0; - else S1_tmp = 0; + if (main_0 == 1 && nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; main_0 = main_0_tmp; return; @@ -175,9 +169,7 @@ void increment(void) S1_tmp = S1; main_0_tmp = main_0; main_0_tmp = 0; - if (S1 == 1) - if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0; - else S1_tmp = 0; + if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0; S1 = S1_tmp; main_0 = main_0_tmp; return; diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle index 950cae9f7c78b63bcd69aa8acf18cd4a83ecf3d2..e5437b11cf441f0122b9d89b3ba1147984506890 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle @@ -3,5 +3,5 @@ [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead [kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing) [wp] Warning: Missing RTE guards -[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:61: Warning: +[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:62: Warning: Neither code nor specification for function f, generating default assigns from the prototype diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..57c2d7eed1ca61046277d1cbf5d005a9fde10a52 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions. +[kernel] Plug-in aorai aborted: invalid user input. diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6803c149a7b942ab01ffcff164c2ae40bf6aca0d --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/ya/metavariables-right.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing) +[wp] Warning: Missing RTE guards diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..44c1487fcf7693e627a38f17cea95e7cd8e7b492 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle @@ -0,0 +1,5 @@ +[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0: + { (Call(h)) and ((aorai_x) > (0)) } +[kernel] Plug-in aorai aborted: invalid user input. diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..79c1ae490e64e6a010e1842eec97bd6062a2cf0d --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing) +[wp] Warning: Missing RTE guards diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..a24943fca9867c96902f607deaafe3a12f1a2e71 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle @@ -0,0 +1,6 @@ +[kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The metavariable aorai_x is assigned several times during the transition from a to b: + { Call(main) } aorai_x <- x + aorai_x <- aorai_x + 1 +[kernel] Plug-in aorai aborted: invalid user input. diff --git a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..ad8ddcef2ca5c41625a8a4dec207a6a71cdf6be6 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/ya/stack.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing) +[wp] Warning: Missing RTE guards diff --git a/src/plugins/aorai/tests/ya/singleassignment-right.i b/src/plugins/aorai/tests/ya/singleassignment-right.i new file mode 100644 index 0000000000000000000000000000000000000000..943c3e5e67cf9c02fde3be2c6dc73b2fbaa07b7d --- /dev/null +++ b/src/plugins/aorai/tests/ya/singleassignment-right.i @@ -0,0 +1,10 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + +void main(int *x, int *y) +{ + int t = *x; + *x = *y; + *y = t; +} diff --git a/src/plugins/aorai/tests/ya/singleassignment-right.ya b/src/plugins/aorai/tests/ya/singleassignment-right.ya new file mode 100644 index 0000000000000000000000000000000000000000..91d6e8715b9e43dcac25e104bbf2c19a72606373 --- /dev/null +++ b/src/plugins/aorai/tests/ya/singleassignment-right.ya @@ -0,0 +1,12 @@ +%init: a; +%accept: c; +%deterministic; + +$x : int; +$y : int; + +a : { CALL(main) } $x := *x; $y := *y -> b; + +b : { RETURN(main) } $x := $y; $y := $x -> c; + +c : -> c; diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.i b/src/plugins/aorai/tests/ya/singleassignment-wrong.i new file mode 100644 index 0000000000000000000000000000000000000000..c983ce03e455dd3ac55c8baa1c76fc0785a8028f --- /dev/null +++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.i @@ -0,0 +1,8 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + +int main(int x) +{ + return x; +} diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.ya b/src/plugins/aorai/tests/ya/singleassignment-wrong.ya new file mode 100644 index 0000000000000000000000000000000000000000..d44ce4687b03b387e066cc7e16dc476373dbe37d --- /dev/null +++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.ya @@ -0,0 +1,11 @@ +%init: a; +%accept: c; +%deterministic; + +$x : int; + +a : { CALL(main) } $x := x; $x := $x + 1 -> b; + +b : { RETURN(main) } -> c; + +c : -> c; diff --git a/src/plugins/aorai/tests/ya/stack.i b/src/plugins/aorai/tests/ya/stack.i new file mode 100644 index 0000000000000000000000000000000000000000..b3a734178295ace67bf450f577e757095db612b1 --- /dev/null +++ b/src/plugins/aorai/tests/ya/stack.i @@ -0,0 +1,31 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + + +int g = 0; + +void push(void) +{ + g++; +} + +void pop(void) +{ + //@ assert g > 0; + g--; +} + +void main(void) +{ + push(); + pop(); + push(); + push(); + pop(); + push(); + push(); + pop(); + pop(); + pop(); +} diff --git a/src/plugins/aorai/tests/ya/stack.ya b/src/plugins/aorai/tests/ya/stack.ya new file mode 100644 index 0000000000000000000000000000000000000000..29c24e7847e8d44f1517c2fcbe3d683ed8ea6866 --- /dev/null +++ b/src/plugins/aorai/tests/ya/stack.ya @@ -0,0 +1,30 @@ +%init: init; +%accept: accept; +%deterministic; + +$n : int; + +init: + { CALL(main) } $n := 0 -> empty_stack +; + +empty_stack: + { RETURN(main) } -> accept +| { CALL(push) } -> filling_stack +; + +filling_stack: + { RETURN(push) } $n := $n + 1 -> filled_stack +; + +filled_stack: + { CALL(push) } -> filling_stack +| { CALL(pop) && $n > 0 } -> emptying_stack +; + +emptying_stack: + { RETURN(pop) && $n > 1 } $n := $n - 1 -> filled_stack +| { RETURN(pop) && $n == 1 } $n := $n - 1 -> empty_stack +; + +accept: -> accept; diff --git a/src/plugins/aorai/yalexer.mll b/src/plugins/aorai/yalexer.mll index b6809baf2e0f74566fa9d51d6817ede1ba36f1a4..54a238bc93472fcd1af25d2b8457082aa8d4be8c 100644 --- a/src/plugins/aorai/yalexer.mll +++ b/src/plugins/aorai/yalexer.mll @@ -27,18 +27,13 @@ { open Yaparser open Lexing - exception Eof + exception Lexing_error of string let new_line lexbuf = let lcp = lexbuf.lex_curr_p in lexbuf.lex_curr_p <- { lcp with pos_lnum = lcp.pos_lnum + 1; pos_bol = lcp.pos_cnum; } ;; - - exception Error of (Lexing.position * Lexing.position) * string - let loc lexbuf = (lexeme_start_p lexbuf, lexeme_end_p lexbuf) - let raise_located loc e = raise (Error (loc, e)) - } let num = ['0'-'9'] @@ -59,6 +54,7 @@ rule token = parse | "false" { FALSE } | "\\result" as lxm { IDENTIFIER(lxm) } | ident as lxm { IDENTIFIER(lxm) } + | '$' (ident as lxm){ METAVAR(lxm) } | ',' { COMMA } | '+' { PLUS } | '-' { MINUS } @@ -92,30 +88,7 @@ rule token = parse | '^' { CARET } | '?' { QUESTION } | eof { EOF } - | _ { raise_located (loc lexbuf) "Unknown token" } - -{ - let parse c = - let lb = from_channel c in - try - Yaparser.main token lb - with - Parsing.Parse_error - | Invalid_argument _ -> - (* [VP]: Does not contain more information than - what is in the exn. *) - (*let (a,b)=(loc lb) in - Format.print_string "Syntax error (" ; - Format.print_string "l" ; - Format.print_int a.pos_lnum ; - Format.print_string "c" ; - Format.print_int (a.pos_cnum-a.pos_bol) ; - Format.print_string " -> l" ; - Format.print_int b.pos_lnum ; - Format.print_string "c" ; - Format.print_int (b.pos_cnum-b.pos_bol) ; - Format.print_string ")\n" ; - *) - raise_located (loc lb) "Syntax error" - -} + | ":=" { AFF } + | _ { + raise (Lexing_error ("unexpected character '" ^ Lexing.lexeme lexbuf ^ "'")) + } diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly index cbecc1a0c520961f4909372a77339fa8bbc4cdea..3b92c647abb385e2a2c06cc7514490ef902575b0 100644 --- a/src/plugins/aorai/yaparser.mly +++ b/src/plugins/aorai/yaparser.mly @@ -27,10 +27,13 @@ /* Originated from http://www.ltl2dstar.de/down/ltl2dstar-0.4.2.zip */ %{ +open Cil_types open Logic_ptree open Promelaast open Bool3 +type options = Deterministic | Init of string list | Accept of string list + let to_seq c = [{ condition = Some c; nested = []; @@ -50,37 +53,99 @@ let fetch_and_create_state name = try Hashtbl.find observed_states name with - Not_found -> + Not_found -> let s = Data_for_aorai.new_state name in Hashtbl.add observed_states name s; s ;; let prefetch_and_create_state name = - if (Hashtbl.mem prefetched_states name) || - not (Hashtbl.mem observed_states name) + if (Hashtbl.mem prefetched_states name) || + not (Hashtbl.mem observed_states name) then begin - let s= fetch_and_create_state name in + let s= fetch_and_create_state name in Hashtbl.add prefetched_states name name; s - end + end else (fetch_and_create_state name) ;; +let set_init_state id = + try + let state = Hashtbl.find observed_states id in + state.init <- True + with Not_found -> + Aorai_option.abort "no state '%s'" id + +let set_accept_state id = + try + let state = Hashtbl.find observed_states id in + state.acceptation <- True + with Not_found -> + Aorai_option.abort "no state '%s'" id + +let add_metavariable map (name,typename) = + let ty = match typename with + | "int" -> TInt(IInt, []) + | "char" -> TInt(IChar, []) + | "long" -> TInt(ILong, []) + | _ -> + Aorai_option.abort "Unrecognized type %s for metavariable %s" + typename name + in + if Datatype.String.Map.mem name map then + Aorai_option.abort "The metavariable %s is declared twice" name; + let vi = Cil.makeGlobalVar (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty in + Datatype.String.Map.add name vi map + +let check_state st = + if st.acceptation=Undefined || st.init=Undefined then + Aorai_option.abort + "Error: the state '%s' is used but never defined." st.name + +let interpret_option = function + | Init states -> + List.iter set_init_state states + | Accept states -> + List.iter set_accept_state states + | Deterministic -> + Aorai_option.Deterministic.set true + +let build_automaton options metavariables trans = + let htable_to_list table = Hashtbl.fold (fun _ st l -> st :: l) table [] in + let states = htable_to_list observed_states + and undefined_states = htable_to_list prefetched_states + and metavariables = + List.fold_left add_metavariable Datatype.String.Map.empty metavariables + in + List.iter interpret_option options; + List.iter check_state states; + if not (List.exists (fun st -> st.init=True) states) then + Aorai_option.abort "Automaton does not declare an initial state"; + if undefined_states <> [] then + Aorai_option.abort "Error: the state(s) %a are used but never defined." + (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) undefined_states; + { states; trans; metavariables } + + type pre_cond = Behavior of string | Pre of Promelaast.condition + %} %token CALL_OF RETURN_OF CALLORRETURN_OF %token <string> IDENTIFIER +%token <string> METAVAR %token <string> INT +%token AFF %token LCURLY RCURLY LPAREN RPAREN LSQUARE RSQUARE LBRACELBRACE RBRACERBRACE %token RARROW %token TRUE FALSE %token NOT DOT AMP -%token COLON SEMI_COLON COMMA PIPE CARET QUESTION COMMA COLUMNCOLUMN +%token COLON SEMI_COLON COMMA PIPE CARET QUESTION COLUMNCOLUMN %token EQ LT GT LE GE NEQ PLUS MINUS SLASH STAR PERCENT OR AND +%token INIT ACCEPT DETERMINISTIC METAVAR %token OTHERWISE %token EOF @@ -93,75 +158,28 @@ type pre_cond = Behavior of string | Pre of Promelaast.condition %left DOT %nonassoc NOT TRUE FALSE %nonassoc QUESTION -%right SEMICOLON +%right SEMI_COLON %nonassoc lowest %type <Promelaast.parsed_automaton> main %start main %% -main - : options states { - List.iter - (fun(key, ids) -> - match key with - "init" -> - List.iter - (fun id -> - try - (Hashtbl.find observed_states id).init <- True - with - Not_found -> - Aorai_option.abort "Error: no state '%s'\n" id) - ids - | "accept" -> - List.iter - (fun id -> try - (Hashtbl.find observed_states id).acceptation <- True - with Not_found -> - Aorai_option.abort "no state '%s'\n" id) ids - | "deterministic" -> Aorai_option.Deterministic.set true; - | oth -> Aorai_option.abort "unknown option '%s'\n" oth - ) $1; - let states= - Hashtbl.fold - (fun _ st l -> - if st.acceptation=Undefined || st.init=Undefined then - begin - Aorai_option.abort - "Error: the state '%s' is used but never defined.\n" st.name - end; - st::l) - observed_states [] - in - (try - Hashtbl.iter - (fun _ st -> if st.init=True then raise Exit) observed_states; - Aorai_option.abort "Automaton does not declare an initial state" - with Exit -> ()); - if Hashtbl.length prefetched_states >0 then - begin - let r = Hashtbl.fold - (fun s n _ -> - s^"Error: the state '"^n^"' is used but never defined.\n") - prefetched_states - "" - in - Aorai_option.abort "%s" r - end; - (states, $2) - } - ; - +main : options metavars states { build_automaton $1 $2 $3 } options - : options option { $1@[$2] } + : options option { $1 @ [$2] } | option { [$1] } ; option - : PERCENT IDENTIFIER opt_identifiers SEMI_COLON { ($2, $3) } - ; + : PERCENT IDENTIFIER opt_identifiers SEMI_COLON { + match $2 with + | "init" -> Init $3 + | "accept" -> Accept $3 + | "deterministic" -> Deterministic + | _ -> Aorai_option.abort "unknown option: '%s'" $2 + } opt_identifiers : /* empty */ { [] } @@ -169,10 +187,23 @@ opt_identifiers ; id_list - : id_list COMMA IDENTIFIER { $1@[$3] } + : id_list COMMA IDENTIFIER { $1 @ [$3] } | IDENTIFIER { [$1] } ; +metavars + : /* epsilon */ { [] } + | non_empty_metavars { $1 } + +non_empty_metavars + : non_empty_metavars metavar { $1 @ [$2] } + | metavar { [$1] } + ; + +metavar + : METAVAR COLON IDENTIFIER SEMI_COLON { $1,$3 } + ; + states : states state { $1@$2 } | state { $1 } @@ -183,7 +214,7 @@ state let start_state = fetch_and_create_state $1 in let (_, transitions) = List.fold_left - (fun (otherwise, transitions) (cross,stop_state) -> + (fun (otherwise, transitions) (cross,actions,stop_state) -> if otherwise then Aorai_option.abort "'other' directive in definition of %s \ @@ -191,11 +222,11 @@ state else begin let trans = { start=start_state; stop=stop_state; - cross=cross; numt=(-1) }::transitions + cross; actions; numt=(-1) }::transitions in - let otherwise = - match cross with - | Otherwise -> true + let otherwise = + match cross with + | Otherwise -> true | Seq _ -> false in otherwise, trans end) @@ -211,10 +242,12 @@ transitions /*=> [transition; ...] */ transition: /*=> (guard, state) */ - | LCURLY seq_elt RCURLY RARROW IDENTIFIER - { (Seq $2, prefetch_and_create_state $5) } - | OTHERWISE RARROW IDENTIFIER {(Otherwise, prefetch_and_create_state $3) } - | RARROW IDENTIFIER { (Seq (to_seq PTrue), prefetch_and_create_state $2) } + | LCURLY seq_elt RCURLY actions RARROW IDENTIFIER + { (Seq $2, $4, prefetch_and_create_state $6) } + | OTHERWISE actions RARROW IDENTIFIER + { (Otherwise, $2, prefetch_and_create_state $4) } + | actions RARROW IDENTIFIER + { (Seq (to_seq PTrue), $1, prefetch_and_create_state $3) } ; non_empty_seq: @@ -231,28 +264,28 @@ guard: | single_cond { to_seq $1 } | LSQUARE non_empty_seq RSQUARE { $2 } | IDENTIFIER pre_cond LPAREN seq RPAREN post_cond - { let pre_cond = + { let pre_cond = match $2 with | Behavior b -> PCall($1,Some b) | Pre c -> PAnd (PCall($1,None), c) in - let post_cond = + let post_cond = match $6 with | None -> PReturn $1 | Some c -> PAnd (PReturn $1,c) in - (to_seq pre_cond) @ $4 @ to_seq post_cond + (to_seq pre_cond) @ $4 @ to_seq post_cond } | IDENTIFIER LPAREN non_empty_seq RPAREN post_cond - { let post_cond = + { let post_cond = match $5 with | None -> PReturn $1 | Some c -> PAnd (PReturn $1,c) in - (to_seq (PCall ($1, None))) @ $3 @ to_seq post_cond + (to_seq (PCall ($1, None))) @ $3 @ to_seq post_cond } | IDENTIFIER LPAREN RPAREN post_cond - { let post_cond = + { let post_cond = match $4 with | None -> PReturn $1 | Some c -> PAnd (PReturn $1,c) @@ -280,7 +313,7 @@ seq_elt: | l -> if is_no_repet (min,max) then l (* [ a; [b;c]; d] is equivalent to [a;b;c;d] *) - else [ { condition = None; nested = l; min_rep = min; max_rep = max } ] + else [ { condition = None; nested = l; min_rep = min; max_rep = max } ] } ; @@ -358,4 +391,24 @@ access_leaf | IDENTIFIER LPAREN RPAREN DOT IDENTIFIER { PPrm($1,$5) } | IDENTIFIER { PVar $1 } | LPAREN access RPAREN { $2 } + | METAVAR { PMetavar $1 } + ; + +actions + : /* epsilon */ { [] } + | non_empty_actions opt_semicolon { $1 } + ; + +non_empty_actions + : non_empty_actions SEMI_COLON action { $1 @ [$3] } + | action { [$1] } + ; + +action + : METAVAR AFF arith_relation { Metavar_assign ($1, $3) } + ; + +opt_semicolon + : /* empty */ {} + | SEMI_COLON {} ;