Commit 18eac92b authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'stable/potassium'

Conflicts:
	nix/frama-ci.nix
parents f234aa4b 451dc5eb
......@@ -3,15 +3,16 @@ stages:
- build
- tests
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "stable/potassium"
OCAML: "4_05"
FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
#avoid a nix error https://github.com/NixOS/nix/issues/2087
git-update:
stage: git-update
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "master"
OCAML: "4_05"
FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- nix/frama-ci.sh instantiate --eval -A e-acsl.src.outPath
tags:
......@@ -19,11 +20,6 @@ git-update:
E-ACSL:
stage: build
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "master"
OCAML: "4_05"
FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- nix/frama-ci.sh build -A e-acsl.installed
tags:
......@@ -31,11 +27,6 @@ E-ACSL:
CheckHeaders:
stage: build
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "master"
OCAML: "4_05"
FRAMA_CI_OPT: "--override genassigns:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- nix/frama-ci.sh build -A genassigns.checkHeaders
tags:
......@@ -43,11 +34,6 @@ CheckHeaders:
Tests:
stage: tests
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "master"
OCAML: "4_05"
FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- nix/frama-ci.sh build -A e-acsl.tests
tags:
......@@ -55,11 +41,6 @@ Tests:
Cfp:
stage: tests
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "master"
OCAML: "4_05"
FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- nix/frama-ci.sh build -A context-from-precondition.tests
tags:
......@@ -67,11 +48,6 @@ Cfp:
Security:
stage: tests
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "master"
OCAML: "4_05"
FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- nix/frama-ci.sh build -A security.tests
tags:
......
......@@ -79,6 +79,7 @@ PLUGIN_CMO:= local_config \
quantif \
at_with_lscope \
mmodel_translate \
logic_functions \
translate \
temporal \
prepare_ast \
......
18.0 Argon+dev
19.0
\ No newline at end of file
......@@ -237,46 +237,47 @@ let to_exp ~loc kf env pot label =
end
in
let ty_ptr = TPtr(ty, []) in
let vi_at, e_at, env = Env.new_var
~loc
~name:"at"
~scope:Env.Function
env
None
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_integer_ty t_size with
| Typing.C_type IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
in
malloc_stmt
| Typing.C_type _ | Typing.Gmp ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.Other ->
Options.fatal
"quantification over non-integer type is not part of E-ACSL"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
Thus we need to add [malloc] and [free] through dedicated functions. *)
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
let vi_at, e_at, env =
Env.new_var
~loc
~name:"at"
~scope:Env.Function
env
None
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_integer_ty t_size with
| Typing.C_type IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
in
malloc_stmt
| Typing.C_type _ | Typing.Gmp ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.Other ->
Options.fatal
"quantification over non-integer type is not part of E-ACSL"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var]. Thus we need to add [malloc] and
[free] through dedicated functions. *)
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
in
(* Index *)
let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
......@@ -337,4 +338,4 @@ let to_exp ~loc kf env pot label =
(* Returning *)
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e = Cil.new_exp ~loc (Lval lval_at_index) in
e, env
\ No newline at end of file
e, env
......@@ -39,7 +39,7 @@ let update s vi =
with Not_found ->
()
(* add [vi] in the built-in table if it is an E-ACSL built-in which is not
(* add [vi] in the built-in table if it is an E-ACSL built-in that is not
[already] registered. *)
let add_builtin vi already =
if not already then
......
......@@ -19,6 +19,12 @@
# configure configure
###############################################################################
##############################
Plugin E-ACSL 19.0 (Potassium)
##############################
- E-ACSL [2019/04/29] Support for logic functions and predicates
without labels.
- runtime [2019/02/26] The behavior of __e_acsl_assert now depends on the
runtime value of the global variable __e_acsl_sound_verdict:
if 0, it means that its verdict is possibly incorrect.
......
......@@ -2,6 +2,7 @@
C-compound-statement ::= "{" declaration* statement* assertion+ "}"
\
C-statement ::= assertion statement \
assertion ::= "/*@" "assert" pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" "assert" pred ";" "*/" } ;
assertion-kind ::= "assert" | "check" \
assertion ::= "/*@" assertion-kind pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
\end{syntax}
......@@ -2,6 +2,14 @@
\subsection*{Version \version}
\begin{itemize}
\item Update according to \acsl 1.14:
\begin{itemize}
\item \changeinsection{assertions}{add the keyword \texttt{check}}
\end{itemize}
\end{itemize}
\subsection*{Version 1.13}
\begin{itemize}
\item Update according to \acsl 1.13:
\begin{itemize}
\item \changeinsection{locations}{add syntax for set membership}
......@@ -117,6 +125,11 @@ in \lstinline|\\at|}
\section{Changes in \eacsl Implementation}
\subsection*{Version \eacslversion}
\begin{itemize}
\item \changeinsection{logicspec}{support of logic functions and predicates}
\end{itemize}
\subsection*{Version Argon-18}
\begin{itemize}
\item \changeinsection{at}{support of \lstinline|\\at| on purely
......
\begin{syntax}
C-global-decl ::= { "/*@" logic-def+ "*/" }
C-global-decl ::= "/*@" logic-def+ "*/"
\
[ { logic-def } ] ::= { logic-const-def } ;
| { logic-function-def } ;
| { logic-predicate-def } ;
logic-def ::= { logic-const-def } ;
| logic-function-def ;
| logic-predicate-def ;
\
[ { type-expr } ] ::= { id };
type-expr ::= id;
\
[ { logic-const-def } ] ::= { "logic" type-expr id "=" term ";" }
{ logic-const-def } ::= { "logic" type-expr id "=" term ";" }
\
[ { logic-function-def } ] ::= { "logic" type-expr id parameters "=" term ";" }
logic-function-def ::= "logic" type-expr id parameters "=" term ";"
\
[ { logic-predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
logic-predicate-def ::= "predicate" id parameters? "=" pred ";"
\
{ parameters } ::= { "(" parameter (, parameter)* ")" }
parameters ::= "(" parameter (, parameter)* ")"
\
{ parameter } ::= { type-expr id }
parameter ::= type-expr id
\end{syntax}
......@@ -24,7 +24,7 @@
\usepackage{alltt}
\makeindex
\newcommand{\acslversion}{1.13\xspace}
\newcommand{\acslversion}{1.14\xspace}
\newcommand{\version}{\acslversion\xspace}
\renewcommand{\textfraction}{0.01}
......
......@@ -612,7 +612,7 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{\notimplemented{Predicate and function definitions}}
\subsection{Predicate and function definitions}
\nodiff
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -642,7 +642,7 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{\notimplemented{Recursive logic definitions}}
\subsection{Recursive logic definitions}
\index{recursion}
\nodiff
......
......@@ -123,7 +123,8 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
if vi.vname = "" then
(* unnamed formal parameter: must generate a fresh name since a fundec
cannot have unnamed formals (see bts #2303). *)
Env.Varname.get ~scope:Env.Function
Env.Varname.get
~scope:Env.Function
(Functions.RTL.mk_gen_name "unamed_formal")
else
vi.vname
......@@ -226,6 +227,18 @@ type position = Before_gmp | Gmp | After_gmp | Memory_model | Code
class dup_functions_visitor prj = object (self)
inherit Visitor.frama_c_copy prj
val unduplicable_functions =
let white_list =
[ "__builtin_va_arg";
"__builtin_va_end";
"__builtin_va_start";
"__builtin_va_copy" ]
in
List.fold_left
(fun acc s -> Datatype.String.Set.add s acc)
Datatype.String.Set.empty
white_list
val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
val mutable before_memory_model = Before_gmp
val mutable new_definitions: global list = []
......@@ -287,25 +300,27 @@ class dup_functions_visitor prj = object (self)
| GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
when (* duplicate a function iff: *)
not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
(* it is not already duplicated *)
(* it is not already duplicated *)
&& not (Datatype.String.Set.mem vi.vname unduplicable_functions)
(* it is duplicable *)
&& self#is_unvariadic_function vi (* it is not a variadic function *)
&& not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
&& not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
&&
(let kf =
try Globals.Functions.get vi with Not_found -> assert false
in
not (Functions.instrument kf)
&& not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
&& not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
&&
(let kf =
try Globals.Functions.get vi with Not_found -> assert false
in
not (Functions.instrument kf)
(* either explicitely listed as to be not instrumented *)
||
(* or: *)
(not (Cil.is_empty_funspec
(Annotations.funspec ~populate:false
(Extlib.the self#current_kf)))
(not (Cil.is_empty_funspec
(Annotations.funspec ~populate:false
(Extlib.the self#current_kf)))
(* it has a function contract *)
&& Functions.check kf
(* its annotations must be monitored *)))
->
->
self#next ();
let name = Functions.RTL.mk_gen_name vi.vname in
let new_vi =
......
......@@ -24,6 +24,11 @@ module E_acsl_label = Label
open Cil_types
open Cil_datatype
type localized_scope =
| LGlobal
| LFunction of kernel_function
| LLocal_block of kernel_function
type scope =
| Global
| Function
......@@ -55,7 +60,7 @@ type t =
lscope: Lscope.t;
lscope_reset: bool;
annotation_kind: Misc.annotation_kind;
new_global_vars: (varinfo * scope) list;
new_global_vars: (varinfo * localized_scope) list;
(* generated variables. The scope indicates the level where the variable
should be added. *)
global_mpz_tbl: mpz_tbl;
......@@ -141,6 +146,19 @@ let has_no_new_stmt env =
let local, _ = top env in
local.block_info = empty_block
let current_kf env =
let v = env.visitor in
match v#current_kf with
| None -> None
| Some kf -> Some (Cil.get_kernel_function v#behavior kf)
let set_current_kf env kf =
let v = env.visitor in
v#set_current_kf kf
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
(* ************************************************************************** *)
(** {2 Loop invariants} *)
(* ************************************************************************** *)
......@@ -189,6 +207,11 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
ty
in
v.vreferenced <- true;
let lscope = match scope with
| Global -> LGlobal
| Function -> LFunction (Extlib.the (current_kf env))
| Local_block -> LLocal_block (Extlib.the (current_kf env))
in
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let e = Cil.evar v in
let stmts = mk_stmts v e in
......@@ -222,7 +245,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
(* also memoize the new variable, but must never be used *)
{ env with
cpt = n;
new_global_vars = (v, scope) :: env.new_global_vars;
new_global_vars = (v, lscope) :: env.new_global_vars;
global_mpz_tbl = extend_tbl env.global_mpz_tbl;
env_stack = local_env :: tl_env }
| Local_block ->
......@@ -234,9 +257,9 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
{ env with
cpt = n;
env_stack = local_env :: tl_env;
new_global_vars = (v, scope) :: env.new_global_vars }
new_global_vars = (v, lscope) :: env.new_global_vars }
end else
let new_global_vars = (v, scope) :: env.new_global_vars in
let new_global_vars = (v, lscope) :: env.new_global_vars in
let local_env =
{ local_env with
block_info = new_block;
......@@ -262,10 +285,8 @@ let new_var ~loc ?(scope=Local_block) ?name env t ty mk_stmts =
do_new_var ~loc ~scope ?name env t ty mk_stmts
in
match scope with
| Global | Function ->
memo env.global_mpz_tbl
| Local_block ->
memo local_env.mpz_tbl
| Global | Function -> memo env.global_mpz_tbl
| Local_block -> memo local_env.mpz_tbl
let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
new_var
......@@ -279,19 +300,29 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
module Logic_binding = struct
let add_binding env logic_v vi =
try
let varinfos = Logic_var.Map.find logic_v env.var_mapping in
Stack.push vi varinfos;
env
with Not_found | Stack.Empty ->
let varinfos = Stack.create () in
Stack.push vi varinfos;
let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
{ env with var_mapping = var_mapping }
let add ?ty env logic_v =
let ty = match ty with
| Some ty -> ty
| None -> match logic_v.lv_type with
| Ctype ty -> ty
| Linteger -> Gmpz.t ()
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
Format.asprintf
"logic variable of type %a" Logic_type.pretty lty
in
Error.not_yet msg
| Ctype ty -> ty
| Linteger -> Gmpz.t ()
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
Format.asprintf "logic variable of type %a" Logic_type.pretty lty
in
Error.not_yet msg
in
let v, e, env = new_var
~loc:Location.unknown
......@@ -301,18 +332,7 @@ module Logic_binding = struct
ty
(fun _ _ -> [])
in
let env =
try
let varinfos = Logic_var.Map.find logic_v env.var_mapping in
Stack.push v varinfos;
env
with Not_found ->
let varinfos = Stack.create () in
Stack.push v varinfos;
let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
{ env with var_mapping = var_mapping }
in
v, e, env
v, e, add_binding env logic_v v
let get env logic_v =
try
......@@ -324,22 +344,12 @@ module Logic_binding = struct
let remove env logic_v =
try
let varinfos = Logic_var.Map.find logic_v env.var_mapping in
ignore (Stack.pop varinfos);
env
ignore (Stack.pop varinfos)
with Not_found | Stack.Empty ->
assert false
end
let current_kf env =
let v = env.visitor in
match v#current_kf with
| None -> None
| Some kf -> Some (Cil.get_kernel_function v#behavior kf)
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
module Logic_scope = struct
let get env = env.lscope
let extend env lvs = { env with lscope = Lscope.add lvs env.lscope }
......@@ -508,7 +518,9 @@ module Context = struct
{ env with new_global_vars =
List.filter
(fun (v, scope) ->
(scope = Global || scope = Function)
(match scope with
| LGlobal | LFunction _ -> true
| LLocal_block _ -> false)
&& List.for_all (fun (v', _) -> v != v') vars)
!ctx
@ vars }
......
......@@ -36,6 +36,11 @@ val has_no_new_stmt: t -> bool
(** Assume that a local context has been previously pushed.
@return true iff the given env does not contain any new statement. *)
type localized_scope =
| LGlobal
| LFunction of kernel_function
| LLocal_block of kernel_function
type scope =
| Global
| Function
......@@ -68,11 +73,16 @@ module Logic_binding: sig
val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
val add_binding: t -> logic_var -> varinfo -> t
(* [add_binding env lv vi] defines [vi] as the latest C binding for
[lv]. *)
val get: t -> logic_var -> varinfo
(* Return the latest C binding. *)
val remove: t -> logic_var -> t
val remove: t -> logic_var -> unit
(* Remove the latest C binding. *)
end
val add_assert: t -> stmt -> predicate -> unit
......@@ -111,10 +121,8 @@ val pop: t -> t
val transfer: from:t -> t -> t
(** Pop the last local context of [from] and push it into the other env. *)
val get_generated_variables: t -> (varinfo * scope) list
(** All the new variables local to the visited function.
The boolean indicates whether the varinfo must be added to the outermost
function block. *)
val get_generated_variables: t -> (varinfo * localized_scope) list
(** All the new variables local to the visited function. *)
val get_visitor: t -> Visitor.generic_frama_c_visitor
val get_behavior: t -> Cil.visitor_behavior
......@@ -142,6 +150,9 @@ module Logic_scope: sig
reset at next call to [reset]. *)
end
val set_current_kf: t -> kernel_function -> unit
(* Set current kf of the environment *)
(* ************************************************************************** *)
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
......
......@@ -28,13 +28,34 @@ let t_torig_ref =
tname = "";
ttype = TVoid [];
treferenced = false }
let t_struct_torig_ref =
ref
{ torig_name = "";
tname = "";
ttype = TVoid [];