Commit 2821b923 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] merging the e-acsl-mmodel branch into the main branch

parent 5289a95e
......@@ -54,13 +54,14 @@ PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
PLUGIN_CMO:= local_config \
options \
read_header \
error \
misc \
mpz \
pre_analysis \
env \
typing \
quantif \
translate \
visit \
main
PLUGIN_HAS_MLI:=yes
......@@ -119,7 +120,10 @@ endif
install::
$(PRINT_CP) E-ACSL share files
$(MKDIR) $(FRAMAC_SHARE)/e-acsl
$(CP) $(E_ACSL_DIR)/share/e-acsl/* $(FRAMAC_SHARE)/e-acsl
$(CP) $(E_ACSL_DIR)/share/e-acsl/*.h $(FRAMAC_SHARE)/e-acsl
$(MKDIR) $(FRAMAC_SHARE)/e-acsl/memory_model
$(CP) $(E_ACSL_DIR)/share/e-acsl/memory_model/* \
$(FRAMAC_SHARE)/e-acsl/memory_model
$(MKDIR) $(FRAMAC_SHARE)/manuals
$(CP) $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf \
$(E_ACSL_DIR)/doc/manuals/e-acsl-implementation.pdf \
......
- enlever les skip inutiles
- valid global literal string
################
# MEMORY MODEL #
################
- appel de full_init et consort sur des variables générées par e_acsl (at.i)
- ne générer les instructions que si nécessaire
- traduction constructions logiques modèle mémoire \valid, \init ...
################
# NEXT RELEASE #
################
- updater doc/Changelog
- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
à appeler dès qu'un behavior est activé
- utiliser Rte pour tous les overflows potentiels
......@@ -15,18 +27,28 @@
- grep TODO *.ml*
- gestion des initialiseurs des globals: requiert un main
- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
- variable GMP potentiellement initialisé mais non utilisé en présence de \at
(voir test result.i, cas -e-acsl-gmp-only)
##############
# KNOWN BUGS #
##############
- sizeof("literal_string") (voir sizeof.i)
- Bernard's bug avec un requires global et un ensures dans un behavior
- sizeof("literal_string") (voir test sizeof.i)
- comparaisons qui aboutissent à du C incorrect
==> comparaison de chaînes litérales
(voir tests other_constants.i et comparison.i)
--> dépend de la sémantique d'ACSL non fixée
--> veut-on le transformer en égalité des caractères avec un ordre lexico
ou veut-on générer une erreur (comportement non **spécifié** du C).
==> comparaison de pointeurs --> générer une erreur (merci RTE?)
- \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
- incorrect d'utiliser un \old dans le post-state si pre-state == post-state
(même raison que ci-dessus)
- incorrect d'utiliser Pre, Post, Here, Old dans stmt contract
(même problème que Jessie: cf. BTS #72)
(voir aussi result.i et ./at_stmt_contract.i)
- interprétation des tableaux
#########
# TESTS #
......@@ -35,3 +57,5 @@
- améliorer test "integer_constant.i" quand bug fixed #745
- inclure exemple du E-ACSL Reference Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo
- -val-verbose 0 dans les tests...
- test intensif modèle mémoire
......@@ -22,7 +22,6 @@
open Cil_types
open Cil_datatype
open Cil
let global_state = ref State.dummy
......@@ -46,9 +45,12 @@ type local_env = { block_info: block_info; mpz_tbl: mpz_tbl }
type t =
{ visitor: Visitor.frama_c_visitor;
annotation_kind: Misc.annotation_kind;
new_global_vars: varinfo list; (* generated variables at function level *)
new_global_vars: (varinfo * bool) list;
(* generated variables at function level. The boolean indicates whether
the varinfo must be added to the outermost function block. *)
global_mpz_tbl: mpz_tbl;
env_stack: local_env list;
init_env: local_env;
var_mapping: Varinfo.t Logic_var.Map.t; (* bind logic var to C var *)
cpt: int; (* counter used when generating variables *) }
......@@ -78,15 +80,20 @@ let empty_mpz_tbl =
{ new_exps = Term.Map.empty;
clear_stmts = [] }
let empty_local_env =
{ block_info = { new_block_vars = []; new_stmts = []; pre_stmts = [] };
mpz_tbl = empty_mpz_tbl }
let dummy =
{ visitor =
new Visitor.generic_frama_c_visitor
Project_skeleton.dummy
(inplace_visit ());
(Cil.inplace_visit ());
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
env_stack = [];
init_env = empty_local_env;
var_mapping = Logic_var.Map.empty;
cpt = 0 }
......@@ -96,22 +103,25 @@ let empty v =
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
env_stack = [];
init_env = empty_local_env;
var_mapping = Logic_var.Map.empty;
cpt = 0 }
let top env = match env.env_stack with [] -> assert false | hd :: tl -> hd, tl
let top init env =
if init then env.init_env, []
else match env.env_stack with [] -> assert false | hd :: tl -> hd, tl
(* eta-expansion required for typing generalisation *)
let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
let do_new_var ?(global=false) ?(name="") env t ty mk_stmts =
let local_env, tl_env = top env in
let do_new_var ?loc init ?(global=false) ?(name="") env t ty mk_stmts =
let local_env, tl_env = top init env in
let local_block = local_env.block_info in
let is_t = Mpz.is_t ty in
if is_t then Mpz.is_now_referenced ();
let n = succ env.cpt in
let v =
makeVarinfo
Cil.makeVarinfo
~logic:false
~generated:true
false (* is a global? *)
......@@ -119,8 +129,9 @@ let do_new_var ?(global=false) ?(name="") env t ty mk_stmts =
(Varname.get ("__e_acsl" ^ if name = "" then "" else "_" ^ name))
ty
in
v.vreferenced <- true;
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let e = Misc.new_lval v in
let e = Cil.evar v in
let stmts = mk_stmts v e in
let new_stmts = acc_list_rev local_block.new_stmts stmts in
let new_block_vars =
......@@ -134,12 +145,13 @@ let do_new_var ?(global=false) ?(name="") env t ty mk_stmts =
in
v,
e,
if is_t then
if is_t then begin
assert (not init); (* only char* in initializers *)
let extend_tbl tbl =
(* Options.feedback "memoizing %a for term %a"
Varinfo.pretty v (fun fmt t -> match t with None -> Format.fprintf fmt
"NONE" | Some t -> Term.pretty fmt t) t;*)
{ clear_stmts = Mpz.clear e :: tbl.clear_stmts;
{ clear_stmts = Mpz.clear ?loc e :: tbl.clear_stmts;
new_exps = match t with
| None -> tbl.new_exps
| Some t -> Term.Map.add t (v, e) tbl.new_exps }
......@@ -149,35 +161,41 @@ let do_new_var ?(global=false) ?(name="") env t ty mk_stmts =
(* also memoise the new variable, but must never be used *)
{ env with
cpt = n;
new_global_vars = v :: env.new_global_vars;
new_global_vars = (v, true) :: env.new_global_vars;
global_mpz_tbl = extend_tbl env.global_mpz_tbl;
env_stack = local_env :: tl_env }
else
let local_env =
{ block_info = new_block; mpz_tbl = extend_tbl local_env.mpz_tbl }
in
{ env with cpt = n; env_stack = local_env :: tl_env }
else
{ env with
cpt = n;
env_stack = local_env :: tl_env;
new_global_vars = (v, false) :: env.new_global_vars }
end else
let new_global_vars =
if global then v :: env.new_global_vars
else env.new_global_vars
if global then (v, true) :: env.new_global_vars
else (v, false) :: env.new_global_vars
in
let local_env = { local_env with block_info = new_block } in
{ env with
new_global_vars = new_global_vars;
cpt = n;
env_stack = { local_env with block_info = new_block } :: tl_env }
init_env = if init then local_env else env.init_env;
env_stack = if init then env.env_stack else local_env :: tl_env }
exception No_term
let new_var ?(global=false) ?name env t ty mk_stmts =
let local_env, _ = top env in
if global then
let new_var ?loc ?(init=false) ?(global=false) ?name env t ty mk_stmts =
let local_env, _ = top init env in
if global then begin
assert (not init);
(* do not use memoisation here: it is incorrect for terms corresponding to
impure expressions
[JS 2011/11/23] actually it is correct now since globals are only use for
\at *)
do_new_var ~global ?name env t ty mk_stmts
else
do_new_var ?loc false ~global ?name env t ty mk_stmts
end else
try
match t with
| None -> raise No_term
......@@ -185,18 +203,20 @@ let new_var ?(global=false) ?name env t ty mk_stmts =
let v, e = Term.Map.find t local_env.mpz_tbl.new_exps in
if Typ.equal ty v.vtype then v, e, env else raise No_term
with Not_found | No_term ->
do_new_var ~global ?name env t ty mk_stmts
do_new_var ?loc ~global init ?name env t ty mk_stmts
let new_var_and_mpz_init ?global ?name env t mk_stmts =
new_var ?global ?name env t Mpz.t (fun v e -> Mpz.init e :: mk_stmts v e)
let new_var_and_mpz_init ?loc ?init ?global ?name env t mk_stmts =
new_var
?loc ?init ?global ?name env t (Mpz.t ())
(fun v e -> Mpz.init ?loc e :: mk_stmts v e)
module Logic_binding = struct
let add env logic_v =
let ty = match logic_v.lv_type with
| Ctype ty -> ty
| Linteger -> Mpz.t
| Ltype _ as ty when Logic_const.is_boolean_type ty -> charType
| Linteger -> Mpz.t ()
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
Pretty_utils.sfprintf
......@@ -204,7 +224,9 @@ module Logic_binding = struct
in
Error.not_yet msg
in
let v, e, env = new_var env ~name:logic_v.lv_name None ty (fun _ _ -> []) in
let v, e, env =
new_var env ~name:logic_v.lv_name None ty (fun ?loc:_ _ _ -> [])
in
v,
e,
{ env with var_mapping = Logic_var.Map.add logic_v v env.var_mapping }
......@@ -227,10 +249,11 @@ let current_kf env =
| Some kf -> Some (Cil.get_kernel_function v#behavior kf)
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
let emitter =
Emitter.create
"E-ACSL"
"E_ACSL"
[ Emitter.Code_annot ]
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
......@@ -243,18 +266,21 @@ let add_assert env stmt annot =
(fun () -> Annotations.add_assert emitter ~kf stmt annot)
env.visitor#get_filling_actions
let add_stmt env stmt =
let local_env, tl = top env in
let add_stmt ?(init=false) env stmt =
let local_env, tl = top init env in
let block = local_env.block_info in
let block = { block with new_stmts = stmt :: block.new_stmts } in
{ env with env_stack = { local_env with block_info = block } :: tl }
let local_env = { local_env with block_info = block } in
{ env with
init_env = if init then local_env else env.init_env;
env_stack = if init then env.env_stack else local_env :: tl }
let extend_stmt_in_place env stmt ~pre block =
let new_stmt = mkStmt ~valid_sid:true (Block block) in
let new_stmt = Cil.mkStmt ~valid_sid:true (Block block) in
let sk = stmt.skind in
stmt.skind <- Block (mkBlock [ new_stmt; mkStmt ~valid_sid:true sk ]);
stmt.skind <- Block (Cil.mkBlock [ new_stmt; Cil.mkStmt ~valid_sid:true sk ]);
if pre then
let local_env, tl_env = top env in
let local_env, tl_env = top false env in
let b_info = local_env.block_info in
let b_info = { b_info with pre_stmts = new_stmt :: b_info.pre_stmts } in
{ env with env_stack = { local_env with block_info = b_info } :: tl_env }
......@@ -268,13 +294,13 @@ let push env =
let pop env =
(* Options.feedback "pop";*)
let _, tl = top env in
let _, tl = top false env in
{ env with env_stack = tl }
type where = Before | Middle | After
let pop_and_get env stmt ~global_clear where =
(* Options.feedback "pop_and_get (%d)" (List.length env.env_stack); *)
let local_env, tl = top env in
let local_env, tl = top false env in
let clear =
if global_clear then begin
Varname.clear ();
......@@ -291,23 +317,22 @@ let pop_and_get env stmt ~global_clear where =
| [] -> acc, stmt
| _ :: tl ->
match stmt.skind with
| Block { bstmts = [ fst; snd ] } ->
(* [JS 2011/11/23] stmts look the same as expected; but sid are
different and I don't know why ==> thus the assertion does not
hold :-( *)
(* assert (Stmt.equal stmt' fst);*)
extract snd (fst :: acc) tl
| Block { bstmts = [ fst; snd ] } -> extract snd (fst :: acc) tl
| _ -> assert false
in
extract stmt [] block.pre_stmts
in
let new_s = block.new_stmts in
let cat stmt l = match stmt.skind with
| Instr(Skip _) -> l
| _ -> stmt :: l
in
let stmts = match where with
| Before -> stmt :: acc_list_rev (List.rev clear) new_s
| Middle -> acc_list_rev (stmt :: List.rev clear) new_s
| After -> acc_list_rev (acc_list_rev [ stmt ] clear) new_s
| Before -> cat stmt (acc_list_rev (List.rev clear) new_s)
| Middle -> acc_list_rev (cat stmt (List.rev clear)) new_s
| After -> acc_list_rev (acc_list_rev (cat stmt []) clear) new_s
in
mkBlock (acc_list_rev stmts pre_stmts)
Cil.mkBlock (acc_list_rev stmts pre_stmts)
in
b.blocals <- acc_list_rev b.blocals block.new_block_vars;
b, { env with env_stack = tl }
......
......@@ -36,20 +36,22 @@ val dummy: t
val empty: Visitor.frama_c_visitor -> t
val new_var:
?global:bool -> ?name:string -> t -> term option -> typ ->
(varinfo -> exp (* the var as exp *) -> stmt list)
-> varinfo * exp * t
?loc:location -> ?init:bool -> ?global:bool -> ?name:string ->
t -> term option -> typ ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
(** [new_var env t ty mk_stmts] extends [env] with a fresh variable of type
[ty] corresponding to [t]. [global] indicates whether the new variable is
global to the current function or local to the local block (default is
[false], i.e. local).
[false], i.e. local). [init] indicates if the initial env must be used.
@return this variable as both a C variable and a C expression already
initialized by applying it to [mk_stmts]. *)
val new_var_and_mpz_init:
?global:bool -> ?name:string -> t -> term option ->
(varinfo -> exp (* the var as exp *) -> stmt list)
-> varinfo * exp * t
?loc:location -> ?init:bool -> ?global:bool -> ?name:string ->
t -> term option ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
(** Same as [new_var], but dedicated to mpz_t variables initialized by
{!Mpz.init}. *)
......@@ -63,7 +65,7 @@ val add_assert: t -> stmt -> predicate named -> unit
(** [add_assert kf s p] extends the global environment with an assertion [p]
associated to the statement [s] in function [kf]. *)
val add_stmt: t -> stmt -> t
val add_stmt: ?init:bool -> t -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s] *)
val extend_stmt_in_place: t -> stmt -> pre:bool -> block -> t
......@@ -86,10 +88,13 @@ val pop_and_get: t -> stmt -> global_clear:bool -> where -> block * t
val pop: t -> t
(** Pop the last local context (ignore the corresponding new block if any *)
val get_generated_variables: t -> varinfo list
(** All the new variables local to the visited function. *)
val get_generated_variables: t -> (varinfo * bool) 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_visitor: t -> Visitor.generic_frama_c_visitor
val get_behavior: t -> Cil.visitor_behavior
val stmt_of_label: t -> logic_label -> stmt
......
#!/bin/sh
gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
......@@ -58,11 +58,9 @@ let () = Env.global_state := Resulting_projects.self
let generate_code =
Resulting_projects.memo
(fun name ->
let visit prj =
Project.on prj Kernel.Keep_unused_specified_functions.off ();
Visit.do_visit ~prj true;
in
File.create_rebuilt_project_from_visitor ~preprocess:false name visit)
Pre_analysis.reset ();
let visit prj = Visit.do_visit ~prj true in
File.create_project_from_visitor(* ~preprocess:false*) name visit)
let generate_code =
Dynamic.register
......@@ -72,8 +70,25 @@ let generate_code =
(Datatype.func Datatype.string Project.ty)
generate_code
let add_e_acsl_library () =
if Options.must_visit () then begin
Kernel.CppExtraArgs.add (Pretty_utils.sfprintf " -I%s/libc" Config.datadir);
Kernel.Keep_unused_specified_functions.off ();
let register s =
File.pre_register
(File.NeedCPP
(s,
File.get_preprocessor_command ()
^ Pretty_utils.sfprintf " -I%s" (Options.Share.dir ~error:true ())))
in
List.iter register (Misc.library_files ())
end
let () = Cmdline.run_after_configuring_stage add_e_acsl_library
let main () =
if Options.Run.get () then
if Options.must_visit () then Pre_analysis.init_mpz ();
if Options.Run.get () then
ignore (generate_code (Options.Project_name.get ()))
else
if Options.Check.get () then ignore (check ())
......
......@@ -24,21 +24,55 @@ open Cil_types
open Cil_datatype
open Cil
let library_files () =
List.map
(Options.Share.file ~error:true)
[ "e_acsl_gmp_types.h";
"e_acsl_gmp.h";
"e_acsl.h";
"memory_model/e_acsl_mmodel_api.h";
"memory_model/e_acsl_bittree.h";
"memory_model/e_acsl_mmodel.h" ]
(* ************************************************************************** *)
(** {2 Builders} *)
(* ************************************************************************** *)
let e_acsl_header () = GText (Read_header.text ())
let library_functions = Datatype.String.Hashtbl.create 17
let register_library_function vi =
Datatype.String.Hashtbl.add library_functions vi.vname vi
let new_lval ?(loc=Location.unknown) v = new_exp ~loc (Lval (var v))
let reset () = Datatype.String.Hashtbl.clear library_functions
let mk_call ?(loc=Location.unknown) ?result fname args =
(* the type is incorrect, but it doesn't matter *)
(* [JS 2011/04/12] should not generate a new variable by function name *)
(* [TODO] require a projectified table to associate an lval to each name *)
let ty = TFun(voidType, None, false, []) in
let f = new_lval ~loc (makeGlobalVar fname ty) in
mkStmt ~valid_sid:true (Instr(Call(result, f, args, loc)))
let vi =
try Datatype.String.Hashtbl.find library_functions fname
with Not_found -> Options.fatal "unregistered library function `%s'" fname
in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let ty_params = match vi.vtype with
| TFun(_, Some l, _, _) -> l
| _ -> assert false
in
let args =
List.map2
(fun (_, ty, _) arg ->
match ty, unrollType (typeOf arg), arg.enode with
| TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
| TPtr _, TArray _, _ -> assert false
| _, ty_arg, _ -> Cil.mkCastT ~force:false ~e:arg ~newt:ty ~oldt:ty_arg)
ty_params
args
in
mkStmtOneInstr ~valid_sid:true (Call(result, f, args, loc))
let mk_debug_mmodel_stmt stmt =
if Options.debug_atleast 2 then
let debug = mk_call "__debug" [] in
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
else
stmt
type annotation_kind = Assertion | Precondition | Postcondition | Invariant
......@@ -65,6 +99,19 @@ let mk_e_acsl_guard ?(reverse=false) kind e p =
"e_acsl_assert"
[ e; kind_to_string loc kind; mkString loc msg; Cil.integer loc line ]
let result_lhost kf =
let stmt =
try Kernel_function.find_return kf
with Kernel_function.No_Statement -> assert false
in
match stmt.skind with
| Return(Some { enode = Lval (lhost, NoOffset) }, _) -> lhost
| _ -> assert false
let result_vi kf = match result_lhost kf with
| Var vi -> vi
| Mem _ -> assert false
(*
Local Variables:
compile-command: "make"
......
......@@ -29,17 +29,23 @@ open Cil_datatype
(** {2 Builders} *)
(* ************************************************************************** *)
val new_lval: ?loc:Location.t -> varinfo -> exp
(* [TODO] put it in the Frama-C kernel? *)
val mk_call: ?loc:Location.t -> ?result:lval -> string -> exp list -> stmt
val mk_debug_mmodel_stmt: stmt -> stmt
type annotation_kind = Assertion | Precondition | Postcondition | Invariant
val mk_e_acsl_guard:
?reverse:bool -> annotation_kind -> exp -> predicate named -> stmt
val e_acsl_header: unit -> global
val library_files: unit -> string list
val register_library_function: varinfo -> unit
val reset: unit -> unit
val result_lhost: kernel_function -> lhost
(** @return the lhost corresponding to \result in the given function *)
val result_vi: kernel_function -> varinfo
(** @return the varinfo corresponding to \result in the given function *)
(*
Local Variables:
......
......@@ -24,20 +24,23 @@ open Cil_types
open Cil_datatype
open Cil
let t_torig =
{ torig_name = "mpz_t";
tname = "mpz_t";
ttype = TVoid [] (* incorrect but does not matter *);
treferenced = false }
let t_torig_ref =
ref
{ torig_name = "";
tname = "";
ttype = TVoid [];
treferenced = false }
let is_now_referenced () = t_torig.treferenced <- true
let set_t ty = t_torig_ref := ty
let t = TNamed(t_torig, [])
let is_t ty = Cil_datatype.Typ.equal ty t
let is_now_referenced () = !t_torig_ref.treferenced <- true
let apply_on_var funname e = Misc.mk_call ("__gmpz_" ^ funname) [ e ]
let init = apply_on_var "init"
let clear = apply_on_var "clear"
let t () = TNamed(!t_torig_ref, [])
let is_t ty = Cil_datatype.Typ.equal ty (t ())
let apply_on_var ?loc funname e = Misc.mk_call ?loc ("__gmpz_" ^ funname) [ e ]
let init ?loc e = apply_on_var "init" ?loc e
let clear ?loc e = apply_on_var "clear" ? loc e
let get_set_suffix_and_arg e =
let ty = typeOf e in
......@@ -56,16 +59,16 @@ let get_set_suffix_and_arg e =
[ e; integer ~<