Commit b71d80ef authored by Correnson Loïc's avatar Correnson Loïc
Browse files

[WP] Added -wp-init-const to control initializers of global const variables ;

     replaces and refines the need for -wp-const previously introduced.
parent e2e9c686
......@@ -384,7 +384,7 @@ module BASE = Model.Generator(Varinfo)
}
let generate x =
let acs_rd = WpStrategy.isGlobalConst x in
let acs_rd = Cil.typeHasQualifier "const" x.vtype in
let prefix =
if x.vglob
then if acs_rd then "K" else "G"
......
......@@ -524,7 +524,7 @@ struct
let valid_base sigma acs x =
if x.vglob then
if acs = RW && WpStrategy.isGlobalConst x
if acs = RW && Cil.typeHasQualifier "const" x.vtype
then p_false
else p_true
else p_bool (ALLOC.value sigma.alloc x)
......
......@@ -668,28 +668,32 @@ module Cfg (W : Mcfg.S) = struct
init_global_variable wenv lv init obj)
implicit_defaults (List.rev initl)
let compute_global_init wenv const obj =
let compute_global_init wenv filter obj =
Globals.Vars.fold
(fun var initinfo obj ->
if var.vstorage = Extern then obj else
if const && not (WpStrategy.isGlobalConst var) then obj else
let old_loc = Cil.CurrentLoc.get () in
Cil.CurrentLoc.set var.vdecl ;
let obj =
match initinfo.init with
| None ->
W.init_value
wenv (Var var,NoOffset) var.vtype None obj
| Some init ->
let lv = Var var, NoOffset in
init_global_variable wenv lv init obj
in Cil.CurrentLoc.set old_loc ; obj
let do_init = match filter with
| `All -> true
| `InitConst -> WpStrategy.isGlobalInitConst var
in if not do_init then obj
else
let old_loc = Cil.CurrentLoc.get () in
Cil.CurrentLoc.set var.vdecl ;
let obj =
match initinfo.init with
| None ->
W.init_value
wenv (Var var,NoOffset) var.vtype None obj
| Some init ->
let lv = Var var, NoOffset in
init_global_variable wenv lv init obj
in Cil.CurrentLoc.set old_loc ; obj
) obj
let process_global_const wenv obj =
Globals.Vars.fold
(fun var _initinfo obj ->
if WpStrategy.isGlobalConst var
if WpStrategy.isGlobalInitConst var
then W.init_const wenv var obj
else obj
) obj
......@@ -699,19 +703,20 @@ module Cfg (W : Mcfg.S) = struct
if WpStrategy.is_main_init kf then
begin
let obj = W.label wenv Clabels.Init obj in
compute_global_init wenv false obj
compute_global_init wenv `All obj
end
else if W.has_init wenv then
begin
let const = WpStrategy.isConstReadonly () in
let obj = if const then process_global_const wenv obj else obj in
let obj =
if WpStrategy.isInitConst ()
then process_global_const wenv obj else obj in
let obj = W.use_assigns wenv None None WpPropId.mk_init_assigns obj in
let obj = W.label wenv Clabels.Init obj in
compute_global_init wenv false obj
compute_global_init wenv `All obj
end
else
let const = WpStrategy.isConstReadonly () in
if const then compute_global_init wenv true obj
if WpStrategy.isInitConst ()
then compute_global_init wenv `InitConst obj
else obj
let get_weakest_precondition cfg ((kf, _g, strategy, res, wenv) as env) =
......
......@@ -42,14 +42,17 @@ Goal Assertion (file tests/wp_bts/bts_1601.c, line 153):
Assume {
(* Domain *)
Type: (is_float32 fCaValue_0) /\ (is_float32 mfAp_0)
/\ (is_float32 mfNewAp_0) /\ (is_uint8 bApAlmC_0)
/\ (is_uint8 bRAp_0) /\ (is_uint8 gbCaMStatus_0)
/\ (is_uint8 gbCaaStatus_0) /\ (is_uint8 mnPb_2)
/\ (is_uint16 F_MIN_R_0) /\ (is_uint16 nApLRL_0)
/\ (is_float32 mfNewAp_0) /\ (is_uint8 RESP_STATE_0)
/\ (is_uint8 bApAlmC_0) /\ (is_uint8 bRAp_0)
/\ (is_uint8 gbCaMStatus_0) /\ (is_uint8 gbCaaStatus_0)
/\ (is_uint8 mnPb_2) /\ (is_uint16 F_MIN_R_0) /\ (is_uint16 nApLRL_0)
/\ (is_uint16 nCaLRL_0).
(* tests/wp_bts/bts_1601.c:64: Conditional *)
If: 1=mnPb_2
Then { (* tests/wp_bts/bts_1601.c:66: Assignment *) Have: 30.=mfAp_0. }
Then {
(* tests/wp_bts/bts_1601.c:66: Assignment *)
Have: mfAp_0=(real_of_int RESP_STATE_0).
}
(* tests/wp_bts/bts_1601.c:74: Conditional *)
If: (real_of_int F_MIN_R_0)<=mfAp_0
Then {
......
/* run.config
OPT: -wp-init-const
*/
/* run.config_qualif
OPT: -wp-init-const
*/
int A[4] = { 1,2,3 } ;
const int B[4] = { 1,2,3 } ;
......
/* run.config
OPT: -wp-init-const
*/
/* run.config_qualif
OPT: -wp-init-const
*/
int x ;
int * const q = &x ;
const int * p = &x ;
......
......@@ -51,7 +51,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'Read' (file tests/wp_plugin/init_const_guard.i, line 23):
Goal Assertion 'Read' (file tests/wp_plugin/init_const_guard.i, line 31):
Let a_0 = (shift (global G_x_761) 0).
Assume {
(* Initializer *)
......@@ -63,15 +63,15 @@ Prove: (valid_rd Malloc_0 a_0 1).
------------------------------------------------------------
Goal Assertion 'Guard_against_Const' (file tests/wp_plugin/init_const_guard.i, line 24):
Goal Assertion 'Guard_against_Const' (file tests/wp_plugin/init_const_guard.i, line 32):
Let a_0 = (shift (global G_x_761) 0).
Assume {
(* Initializer *)
Have: a_0=Mptr_2[(shift (global K_q_762) 0)].
(* Heap *)
Have: (framed Mptr_2) /\ (linked Malloc_0).
(* Assertion 'Read' (file tests/wp_plugin/init_const_guard.i, line 23) *)
(* tests/wp_plugin/init_const_guard.i:23: Assertion 'Read': *)
(* Assertion 'Read' (file tests/wp_plugin/init_const_guard.i, line 31) *)
(* tests/wp_plugin/init_const_guard.i:31: Assertion 'Read': *)
Have: (valid_rd Malloc_0 a_0 1).
}
Prove: not (valid_rw Malloc_0 a_0 1).
......
......@@ -640,12 +640,9 @@ let is_main_init kf =
Kernel_function.pretty kf (if is_main then "" else "NOT ");
is_main
let isConstReadonly () =
Kernel.ConstReadonly.get () && Wp_parameters.Const.get ()
let isInitConst () = Kernel.ConstReadonly.get () && Wp_parameters.Init.get ()
(* Whether the variable is elliligle for global const initializer. *)
let isGlobalConst var =
isConstReadonly () &&
let isGlobalInitConst var =
var.vglob && var.vstorage <> Extern && Cil.typeHasQualifier "const" var.vtype
let mk_variant_properties kf s ca v =
......
......@@ -248,17 +248,19 @@ val pp_info_of_strategy : Format.formatter -> strategy -> unit
(** The function is the main entry point AND it is not a lib entry *)
val is_main_init : Cil_types.kernel_function -> bool
(** Combines ["-const-readonly"] and ["-wp-const"].
@since Neon-20140301+dev
*)
val isConstReadonly : unit -> bool
(** True if [isConstReadonly] returns [true]
(** True if both options [-const-readonly] and [-wp-init] are positionned,
and the variable is global, not extern, with a ["const"] type
(see [hasConstAttribute]).
@since Neon-20140301+dev
*)
val isGlobalConst : varinfo -> bool
val isInitConst : unit -> bool
(** True if the variable is global, not extern, with a ["const"] qualifier type.
{b Should} only apply when [isInitConst] is true.
@since Neon-20140301+dev
*)
val isGlobalInitConst : varinfo -> bool
(** apply [f_normal] on the [Normal] postconditions,
* [f_exits] on the [Exits] postconditions, and warn on the others. *)
......
......@@ -213,10 +213,10 @@ module Literals =
let wp_strategy = add_group "Computation Strategies"
let () = Parameter_customize.set_group wp_strategy
module Const =
True(struct
let option_name = "-wp-const"
let help = "Take into account -const-readonly (by default)"
module Init =
False(struct
let option_name = "-wp-init-const"
let help = "Use initializers for global const variables"
end)
let () = Parameter_customize.set_group wp_strategy
......
......@@ -53,7 +53,7 @@ module Literals : Parameter_sig.Bool
(** {2 Computation Strategies} *)
module Const: Parameter_sig.Bool
module Init: Parameter_sig.Bool
module RTE: Parameter_sig.Bool
module Simpl: Parameter_sig.Bool
module Let: Parameter_sig.Bool
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment