Commit 2feca4a1 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'feature/fonenantsoa/functions' into 'stable/potassium'

Support for logic functions and predicates without labels

See merge request frama-c/e-acsl!215
parents 072e3647 6461ea99
......@@ -79,6 +79,7 @@ PLUGIN_CMO:= local_config \
quantif \
at_with_lscope \
mmodel_translate \
logic_functions \
translate \
temporal \
prepare_ast \
......
......@@ -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,8 @@
# configure configure
###############################################################################
- 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.
......
......@@ -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
......
......@@ -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 [];
treferenced = false }
let set_t ty = t_torig_ref := ty
let set_t_struct ty = t_struct_torig_ref := ty
let is_now_referenced () = !t_torig_ref.treferenced <- true
let t () = TNamed(!t_torig_ref, [])
let is_t ty = Cil_datatype.Typ.equal ty (t ())
let t_ptr () = TNamed(
{
torig_name = "";
tname = "__e_acsl_mpz_struct *";
ttype = TArray(
TNamed(!t_struct_torig_ref, []),
Some (Cil.one ~loc:Cil_datatype.Location.unknown),
{scache = Not_Computed},
[]);
treferenced = true;
},
[])
let is_t ty =
Cil_datatype.Typ.equal ty (t ()) || Cil_datatype.Typ.equal ty (t_ptr ())
let apply_on_var ~loc funname e = Misc.mk_call ~loc ("__gmpz_" ^ funname) [ e ]
let init ~loc e = apply_on_var "init" ~loc e
......@@ -106,6 +127,9 @@ let init_t () =
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
set_t info;
Cil.SkipChildren
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_struct" ->
set_t_struct info;
Cil.SkipChildren
| _ ->
Cil.SkipChildren
end in
......
......@@ -31,6 +31,8 @@ val set_t: typeinfo -> unit
val t: unit -> typ
(** type "mpz_t" *)
val t_ptr: unit -> typ
(** type "_mpz_struct *" *)
val is_now_referenced: unit -> unit
(** Should be called once one variable of type "mpz_t" exists *)
......
......@@ -39,6 +39,8 @@ literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
local_config.ml: .ignore
local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
......
......@@ -25,16 +25,24 @@ open Cil_types
(* Implement Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince". *)
exception Not_an_integer
(* ********************************************************************* *)
(* Basic datatypes and operations *)
(* ********************************************************************* *)
exception Not_an_integer
(* constructors *)
let singleton_of_int n = Ival.inject_singleton (Integer.of_int n)
let interv_of_unknown_block =
(* since we have no idea of the size of this block, we take the largest
possible one which is unfortunately quite large *)
lazy
(Ival.inject_range
(Some Integer.zero)
(Some (Bit_utils.max_byte_address ())))
let rec interv_of_typ ty = match Cil.unrollType ty with
| TInt (k,_) as ty ->
let n = Cil.bitsSizeOf ty in
......@@ -47,22 +55,118 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
| _ ->
raise Not_an_integer
let interv_of_unknown_block =
(* since we have no idea of the size of this block, we take the largest
possible one which is unfortunately quite large *)
lazy
(Ival.inject_range (Some Integer.zero) (Some (Bit_utils.max_byte_address ())))
let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ ty
| Linteger -> Ival.inject_range None None
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
| Lreal -> Error.not_yet "real number"
| Larrow _ -> Error.not_yet "functional type"
(* imperative environments *)
let ikind_of_interv i =
if Ival.is_bottom i then IInt
else match Ival.min_and_max i with
| Some l, Some u ->
let is_pos = Integer.ge l Integer.zero in
let lkind = Cil.intKindForValue l is_pos in
let ukind = Cil.intKindForValue u is_pos in
(* kind corresponding to the interval *)
let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
(* convert the kind to [IInt] whenever smaller. *)
if Cil.intTypeIncluded kind IInt then IInt else kind
| None, None -> raise Cil.Not_representable (* GMP *)
| None, Some _ | Some _, None ->
Kernel.fatal ~current:true "ival: %a" Ival.pretty i
module Env = struct
(* Imperative environments *)
module rec Env: sig
val clear: unit -> unit
val add: Cil_types.logic_var -> Ival.t -> unit
val find: Cil_types.logic_var -> Ival.t
val remove: Cil_types.logic_var -> unit
val replace: Cil_types.logic_var -> Ival.t -> unit
end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
let clear () = Logic_var.Hashtbl.clear tbl
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
let replace = Logic_var.Hashtbl.replace tbl
let find = Logic_var.Hashtbl.find tbl
let clear () =
Logic_var.Hashtbl.clear tbl;
Logic_function_env.clear ()
end
(* Environment for handling recursive logic functions *)
and Logic_function_env: sig
val widen: infer:(term -> Ival.t) -> term -> Ival.t -> bool * Ival.t
val clear: unit -> unit
end = struct
module Profile =
Datatype.List_with_collections
(Ival)
(struct
let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
end)
module LF =
Datatype.Pair_with_collections
(Datatype.String)
(Profile)
(struct
let module_name = "E_ACSL.Interval.Logic_function_env.LF"
end)
let tbl = LF.Hashtbl.create 7
let clear () = LF.Hashtbl.clear tbl
let interv_of_typ_containing_interv i =
try
let kind = ikind_of_interv i in
interv_of_typ (TInt(kind, []))
with Cil.Not_representable ->
(* infinity *)
Ival.inject_range None None
let extract_profile ~infer t = match t.term_node with
| Tapp(li, _, args) ->
li.l_var_info.lv_name,
List.map2
(fun param arg ->
try
let i = infer arg in
(* over-approximation of the interval to reach the fixpoint
faster, and to generate fewer specialized functions *)
let larger_i = interv_of_typ_containing_interv i in
Env.add param larger_i;
larger_i
with Not_an_integer ->
(* no need to add [param] to the environment *)
Ival.bottom)
li.l_profile
args
| _ ->
assert false
let widen ~infer t i =
let p = extract_profile ~infer t in
try
let old_i = LF.Hashtbl.find tbl p in
if Ival.is_included i old_i then true, old_i
else begin
let j = Ival.join i old_i in
LF.Hashtbl.replace tbl p j;
false, j
end
with Not_found ->
LF.Hashtbl.add tbl p i;
false, i
end
(* ********************************************************************* *)
......@@ -183,11 +287,28 @@ let rec infer t =
Ival.meet i1 i2
| Tapp (li, _, _args) ->
(match li.l_type with
| None -> assert false (* [None] only possible for predicates *)
| Some Linteger -> Error.not_yet "logic function returning an integer"
| Some (Ctype ty) -> interv_of_typ ty
| Some _ -> raise Not_an_integer)
(match li.l_body with
| LBpred _ ->
Ival.zero_or_one
| LBterm t' ->
let rec fixpoint i =
let is_included, new_i = Logic_function_env.widen ~infer t i in
if is_included then begin
List.iter (fun lv -> Env.remove lv) li.l_profile;
new_i
end else
let i = infer t' in
List.iter (fun lv -> Env.remove lv) li.l_profile;
fixpoint i
in
fixpoint Ival.bottom
| LBnone
| LBreads _ ->
(match li.l_type with
| None -> assert false