Commit d3e80f65 authored by Julien Signoles's avatar Julien Signoles
Browse files

restore behavior of -e-acsl-valid which was broken since Jan. 2017 or so

parent 3e9e2686
......@@ -57,6 +57,7 @@
/tests/runtime/*.cm*
/tests/runtime/result/*
/tests/temporal/result/*
/tests/special/result/*
/tests/no-main/result/*
/tests/full-mmodel/result/*
/tests/bts/result/*
......
......@@ -69,6 +69,7 @@ PLUGIN_CMO:= local_config \
exit_points \
label \
env \
keep_status \
dup_functions \
interval \
typing \
......@@ -129,7 +130,7 @@ $(EACSL_PLUGIN_DIR)/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_F
ifeq (@MAY_RUN_TESTS@,yes)
PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main full-mmodel temporal
PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main full-mmodel temporal special
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
E_ACSL_TESTS: $(EACSL_PLUGIN_DIR)/tests/test_config
......
......@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
-* E-ACSL [2017/11/27] Restore behavior of option -e-acsl-valid broken
since Phosphorus (included).
-* E-ACSL [2017/10/25] Fix bug #2303 about unnamed formals in
annotated functions.
- E-ACSL [2017/06/10] Add --free-valid-address option to e-acsl.gcc.sh
......
......@@ -29,7 +29,6 @@ let dkey = Options.dkey_dup
(* ********************************************************************** *)
let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
let is_generated kf = Kernel_function.Hashtbl.mem fct_tbl kf
let actions = Queue.create ()
......@@ -51,51 +50,10 @@ let reset () =
Global.reset ();
Queue.clear actions
(* ********************************************************************** *)
(* Duplicating property statuses *)
(* ********************************************************************** *)
let reemit = function
| Property.IPBehavior _ | Property.IPAxiom _ | Property.IPAxiomatic _
| Property.IPPredicate (Property.PKAssumes _, _, _, _) -> false
| _ -> true
let copy_ppt old_prj new_prj old_ppt new_ppt =
let module P = Property_status in
let selection = State_selection.of_list [ P.self; Emitter.self ] in
let emit s l =
Project.on ~selection new_prj
(fun s ->
let e = match l with [] -> assert false | e :: _ -> e in
let emitter = Emitter.Usable_emitter.get e.P.emitter in
match s with
| P.True | P.False_and_reachable | P.Dont_know ->
P.emit emitter ~hyps:e.P.properties new_ppt s
| P.False_if_reachable ->
(* in that case, the only hypothesis is "Reachable new_ppt" which must
be automatically added by the kernel *)
P.emit emitter ~hyps:[] new_ppt P.False_if_reachable)
s
in
let copy () =
match Project.on ~selection old_prj P.get old_ppt with
| P.Never_tried -> ()
| P.Best(s, l) -> emit s l
| P.Inconsistent i ->
emit P.True i.P.valid;
emit P.False_and_reachable i.P.invalid
in
if reemit old_ppt && not (Options.Valid.get ()) then Queue.add copy actions
(* ********************************************************************** *)
(* Duplicating functions *)
(* ********************************************************************** *)
let dup_spec_status old_prj kf new_kf old_spec new_spec =
let old_ppts = Property.ip_of_spec kf Kglobal ~active:[] old_spec in
let new_ppts = Property.ip_of_spec new_kf Kglobal ~active:[] new_spec in
List.iter2 (copy_ppt old_prj (Project.current ())) old_ppts new_ppts
let dup_funspec tbl bhv spec =
(* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
let o = object
......@@ -205,7 +163,7 @@ let dup_fundec loc spec bhv kf vi new_vi =
sallstmts = [];
sspec = new_spec }
let dup_global loc old_prj spec bhv kf vi new_vi =
let dup_global loc actions spec bhv kf vi new_vi =
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
let fundec = dup_fundec loc spec bhv kf vi new_vi in
......@@ -216,8 +174,34 @@ let dup_global loc old_prj spec bhv kf vi new_vi =
Globals.Functions.register new_kf;
Globals.Functions.replace_by_definition new_spec fundec loc;
Annotations.register_funspec new_kf;
dup_spec_status old_prj kf new_kf spec new_spec;
Options.feedback ~dkey ~level:2 "function %s" name;
(* remove the specs attached to the previous kf iff it is a definition:
it is necessary to keep stable the number of annotations in order to get
[Keep_status] working fine. *)
let kf = Cil.get_kernel_function bhv kf in
if Kernel_function.is_definition kf then begin
Queue.add
(fun () ->
let bhvs =
Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
in
List.iter
(fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
bhvs;
Annotations.iter_decreases
(fun e _ -> Annotations.remove_decreases e kf)
kf;
Annotations.iter_terminates
(fun e _ -> Annotations.remove_terminates e kf)
kf;
Annotations.iter_complete
(fun e l -> Annotations.remove_complete e kf l)
kf;
Annotations.iter_disjoint
(fun e l -> Annotations.remove_disjoint e kf l)
kf)
actions
end;
GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
(* ********************************************************************** *)
......@@ -258,22 +242,7 @@ class dup_functions_visitor prj = object (self)
| Memory_model -> before_memory_model <- Code
| Code -> ()
method !vcode_annot a =
Cil.JustCopyPost
(fun a' ->
let get_ppt kf stmt a = Property.ip_of_code_annot kf stmt a in
let kf = Extlib.the self#current_kf in
let stmt = Extlib.the self#current_stmt in
List.iter2
(fun p p' -> copy_ppt (Project.current ()) prj p p')
(get_ppt kf stmt a)
(get_ppt
(Cil.get_kernel_function self#behavior kf)
(Cil.get_stmt self#behavior stmt)
a');
a')
method !vlogic_info_decl li =
method !vlogic_info_decl li =
Global.add_logic_info li;
Cil.JustCopy
......@@ -338,8 +307,15 @@ if there are memory-related annotations.@]"
let spec = Annotations.funspec ~populate:false kf in
let vi_bhv = Cil.get_varinfo self#behavior vi in
let new_g, new_decl =
Project.on prj
(dup_global loc (Project.current ()) spec self#behavior kf vi_bhv)
Project.on
prj
(dup_global
loc
self#get_filling_actions
spec
self#behavior
kf
vi_bhv)
new_vi
in
(* postpone the introduction of the new function definition to the
......
......@@ -20,10 +20,7 @@
(* *)
(**************************************************************************)
open Cil_types
val dup: unit -> Project.t
val is_generated: kernel_function -> bool
(*
Local Variables:
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(* E-ACSL needs to access to the property status of every property (in
particular for the option -e-acsl-valid). However, the necessary elements for
building a property are copied/modified several times from the original
project to the final project and the property statuses are destroyed when
creating the intermediate projects; so there is no easy way to access to
property statuses from the final project.
This module aims at solving this issue by providing an access to property
statuses from the final project. To work properly, it requires to visit every
property during the final visit in the very same order than during the AST
preparation visit. Indeed, for each function, it associates to each
property an unique integer corresponding to its visit ordering. *)
(* the kind is only used for a few additional consistency checks between [push]
and [must_translate]*)
type kind =
| K_Assert
| K_Invariant
| K_Variant
| K_StmtSpec
| K_Allocation
| K_Assigns
| K_Decreases
| K_Terminates
| K_Complete
| K_Disjoint
| K_Requires
| K_Ensures
let pretty_kind fmt k =
Format.fprintf fmt "%s"
(match k with
| K_Assert -> "assert"
| K_Invariant -> "invariant"
| K_Variant -> "variant"
| K_StmtSpec -> "stmtspec"
| K_Allocation -> "allocation"
| K_Assigns -> "assigns"
| K_Decreases -> "decreases"
| K_Terminates -> "terminates"
| K_Complete -> "complete"
| K_Disjoint -> "disjoint"
| K_Requires -> "requires"
| K_Ensures -> "ensures")
(* information attached to every kernel_function containing an annotation *)
type kf_info =
{ mutable cpt: int; (* counter building the relationship between [push] and
[must_translate *)
mutable statuses: (kind * bool) Datatype.Int.Map.t
(* map associating a property as an integer to its kind and status
([true] = proved) *) }
(* statuses for each function represented by its name (because the [kf] itself
changes from a project to another). *)
let keep_status
: kf_info Datatype.String.Hashtbl.t
= Datatype.String.Hashtbl.create 17
(* will contain the value of a few options from the original project
in order to safely use them from the final project. *)
let option_valid = ref false
let option_check = ref false
let clear () =
Datatype.String.Hashtbl.clear keep_status;
option_valid := Options.Valid.get ();
option_check := Options.Check.get ()
let push kf kind ppt =
(* Options.feedback "PUSHING %a for %a"
pretty_kind kind
Kernel_function.pretty kf;*)
(* no registration when -e-acsl-check or -e-acsl-valid *)
if not (!option_check || !option_valid) then
let keep =
let open Property_status in
match get ppt with
| Never_tried
| Inconsistent _
| Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
true
| Best (True, _) ->
false
in
let status = kind, keep in
let name = Kernel_function.get_name kf in
try
let info = Datatype.String.Hashtbl.find keep_status name in
info.cpt <- info.cpt + 1;
info.statuses <- Datatype.Int.Map.add info.cpt status info.statuses
with Not_found ->
let info = { cpt = 1; statuses = Datatype.Int.Map.singleton 1 status } in
Datatype.String.Hashtbl.add keep_status name info
let before_translation () =
(* reset all counters *)
Datatype.String.Hashtbl.iter (fun _ info -> info.cpt <- 0) keep_status
let must_translate kf kind =
(* Options.feedback "GETTING %a for %a"
pretty_kind kind
Kernel_function.pretty kf;*)
!option_check
||
!option_valid
||
(* function contracts have been moved from the original function to its
duplicate by [Dup_function] but they are still associated to the original
function here *)
let name = Misc.get_original_name kf in
let info =
try Datatype.String.Hashtbl.find keep_status name
with Not_found ->
Options.fatal "[keep_status] unbound function" Datatype.String.pretty kf
in
info.cpt <- info.cpt + 1;
let kind', keep =
try Datatype.Int.Map.find info.cpt info.statuses
with Not_found ->
Options.fatal "[keep_status] unbound annotation (id %d)" info.cpt
in
(* check kind consistency in order to detect more abnormal behaviors *)
if kind <> kind' then
Options.fatal "[keep_status] incorrect kind '%a' (expected: '%a')"
pretty_kind kind
pretty_kind kind';
keep
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(** Make the property statuses of the initial project accessible when
doing the main translation *)
type kind =
| K_Assert
| K_Invariant
| K_Variant
| K_StmtSpec
| K_Allocation
| K_Assigns
| K_Decreases
| K_Terminates (* TODO: should be removed: not part of the E-ACSL subset *)
| K_Complete
| K_Disjoint
| K_Requires
| K_Ensures
val clear: unit -> unit
(** to be called before any program transformation *)
val push: Kernel_function.t -> kind -> Property.t -> unit
(** store the given property of the given kind for the given function *)
val before_translation: unit -> unit
(** to be called just before the main translation *)
val must_translate: Kernel_function.t -> kind -> bool
(** To be called just before transforming a property of the given kind for the
given function.
VERY IMPORTANT: the property of the n-th call to this function exactly
correspond to the n-th pushed property (see {!push}).
@return true if and only if the translation must occur. *)
......@@ -135,7 +135,7 @@ module Resulting_projects =
(struct
let name = "E-ACSL resulting projects"
let size = 7
let dependencies = [ Ast.self ]
let dependencies = Ast.self :: Options.parameter_states
end)
let () =
......@@ -249,6 +249,7 @@ let change_printer =
end
let main () =
Keep_status.clear ();
if Options.Run.get () then begin
change_printer ();
ignore (generate_code (Options.Project_name.get ()))
......
......@@ -138,7 +138,7 @@ let is_generated_kf kf =
let name = Kernel_function.get_vi kf in
is_generated_varinfo name
let get_orig_name kf =
let get_original_name kf =
let name = Kernel_function.get_name kf in
strip_prefix e_acsl_gen_prefix name
......@@ -164,7 +164,7 @@ let mk_e_acsl_guard ?(reverse=false) kind kf e p =
(mk_api_name "assert")
[ e;
kind_to_string loc kind;
Cil.mkString ~loc (get_orig_name kf);
Cil.mkString ~loc (get_original_name kf);
Cil.mkString ~loc msg;
Cil.integer loc line ]
......
......@@ -122,6 +122,10 @@ val is_generated_literal_string_varinfo: varinfo -> bool
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_varinfo] but for kernel functions *)
val get_original_name: kernel_function -> string
(** @return the original basename of a function for generated functions, or the
identify for ungenerated ones. *)
(*
Local Variables:
compile-command: "make"
......
......@@ -119,6 +119,13 @@ let version () =
end
let () = Cmdline.run_after_configuring_stage version
let parameter_states =
[ Valid.self;
Gmp_only.self;
Full_mmodel.self;
Builtins.self;
Temporal_validity.self]
let must_visit () = Run.get () || Check.get ()
let dkey_analysis = register_category "analysis"
......
......@@ -32,6 +32,8 @@ module Project_name: Parameter_sig.String
module Builtins: Parameter_sig.String_set
module Temporal_validity: Parameter_sig.Bool
val parameter_states: State.t list
val must_visit: unit -> bool
val dkey_analysis: Log.category
......
......@@ -58,7 +58,7 @@ let sufficiently_aligned attrs algn =
let require_alignment typ attrs algn =
Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
class prepare_visitor prj = object (_)
class prepare_visitor prj = object (self)
inherit Visitor.frama_c_copy prj
(* Add align attributes to local variables (required by temporal analysis) *)
......@@ -66,32 +66,153 @@ class prepare_visitor prj = object (_)
if Temporal.is_enabled () then
Cil.DoChildrenPost (fun blk ->
List.iter (fun vi ->
(* 4 bytes alignment is required to allow sufficient space for storage
of 32-bit timestamps in a 1:1 shadow. *)
(* 4 bytes alignment is required to allow sufficient space for storage
of 32-bit timestamps in a 1:1 shadow. *)
if require_alignment vi.vtype vi.vattr 4; then begin
vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
end)
blk.blocals;
blk)
blk.blocals;
blk)
else
Cil.DoChildren
(* IMPORTANT: for keeping property statuses, we must preserve the ordering of
translation, see function [Translate.translate_pre_spec] and
[Translate.translate_post_spec]: be careful when modifying it. *)
method private push_pre_spec s =
let kf = Extlib.the self#current_kf in
let kinstr = self#current_kinstr in
let open Keep_status in
Extlib.may
(fun v -> push kf K_Decreases (Property.ip_of_decreases kf kinstr v))
s.spec_variant;
Extlib.may
(fun t -> push kf K_Terminates (Property.ip_of_terminates kf kinstr t))
s.spec_terminates;
List.iter
(fun l ->
push kf K_Complete (Property.ip_of_complete kf kinstr ~active:[] l))
s.spec_complete_behaviors;
List.iter
(fun l ->
push kf K_Disjoint (Property.ip_of_disjoint kf kinstr ~active:[] l))
s.spec_disjoint_behaviors;
List.iter
(fun b ->
List.iter
(fun p -> push kf K_Requires (Property.ip_of_requires kf kinstr b p))
b.b_requires)
s.spec_behavior
method private push_post_spec spec =
let do_behavior b =
let kf = Extlib.the self#current_kf in
let ki = match self#current_stmt with
| None -> Kglobal
| Some stmt -> Kstmt stmt
in
let open Keep_status in
Extlib.may
(push kf K_Assigns)
(Property.ip_of_assigns
kf
ki
(Property.Id_contract (Datatype.String.Set.empty (* TODO *), b))
b.b_assigns);
List.iter
(fun p -> push kf K_Ensures (Property.ip_of_ensures kf ki b p))
b.b_post_cond
in
(* fix ordering of behaviors' iterations *)
let bhvs =
List.sort
(fun b1 b2 -> String.compare b1.b_name b2.b_name)
spec.spec_behavior
in
List.iter do_behavior bhvs
method private push_pre_code_annot a =
let kf = Extlib.the self#current_kf in
let stmt = Extlib.the self#current_stmt in
let push_single k a =
Keep_status.push kf k (Property.ip_of_code_annot_single kf stmt a)
in
let open Keep_status in
match a.annot_content with
| AAssert _ -> push_single K_Assert a
| AStmtSpec(_ (* TODO *), s) -> self#push_pre_spec s
| AInvariant _ -> push_single K_Invariant a
| AVariant v ->
push kf K_Variant (Property.ip_of_decreases kf (Kstmt stmt) v)
| AAssigns _ ->
(* TODO: should be a postcondition, but considered as a unhandled
precondition in translate.ml right now; and we need to preserve the
same ordering *)
Extlib.may
(push kf K_Assigns)
(Property.ip_assigns_of_code_annot kf (Kstmt stmt) a)
| AAllocation(_ (* TODO *), alloc) ->
Extlib.may
(push kf K_Allocation)
(Property.ip_of_allocation kf (Kstmt stmt) (Property.Id_loop a) alloc)
| APragma _ -> () (* not yet translated *)
| AExtended _ -> () (* never translate extensions *)
method private push_post_code_annot a = match a.annot_content with
| AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
| AAssert _
| AInvariant _
| AVariant _
| AAssigns _
| AAllocation _
| APragma _
| AExtended _ -> ()
(* Move variable declared in the body of a switch statement to the outer
scope *)
method !vstmt_aux _ =
Cil.DoChildrenPost (fun stmt ->
match stmt.skind with
| Switch(_,sw_blk,_,_) ->
let new_blk = Cil.mkBlock [ stmt ] in
let new_stmt = Cil.mkStmt (Block new_blk) in
new_blk.blocals <- sw_blk.blocals;
sw_blk.blocals <- [];
new_stmt
| _ -> stmt)
initializer
Project.copy ~selection:(Parameter_state.get_selection ()) prj
end
method !vstmt_aux init_stmt =
Annotations.iter_code_annot
(fun _ a -> self#push_pre_code_annot a)