Commit ce8b3f0d authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'ya_variables' into 'master'

Metavariables in Aorai

See merge request frama-c/frama-c!2098
parents b26af726 32202fd3
......@@ -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
......
......@@ -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
......
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -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
}
......
\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}
\begin{syntax}
directive ::= ... | '$' id ':' type
\\
type::= 'char' | 'int' | 'long'
\\
guard ::= '{' condition '}' action*
\\
action ::= '$' id ':=' lval ';'
\\
lval ::= ... | '$'id
\end{syntax}
......@@ -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
......
......@@ -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);
......
......@@ -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
......
......@@ -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
......@@ -51,6 +51,8 @@ PLUGIN_CMO:= bool3 \
path_analysis \
promelaoutput \
logic_simplification \
aorai_graph \
aorai_metavariables \
data_for_aorai \
aorai_utils \
ltl_output \
......
......@@ -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
......
(**************************************************************************)
(* *)
(* 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 []
(**************************************************************************)
(* *)
(* 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
(**************************************************************************)
(* *)
(* 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