Commit ea7f06c2 authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica Committed by Julien Signoles
Browse files

Support for user-defined logic functions and predicates without labels

parent 072e3647
......@@ -73,12 +73,14 @@ PLUGIN_CMO:= local_config \
env \
keep_status \
dup_functions \
fixpoint \
interval \
typing \
loops \
quantif \
at_with_lscope \
mmodel_translate \
lfunctions \
translate \
temporal \
prepare_ast \
......
......@@ -314,6 +314,17 @@ module Logic_binding = struct
in
v, e, env
let add_existing_vi env lv vi =
try
let varinfos = Logic_var.Map.find lv 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 lv varinfos env.var_mapping in
{ env with var_mapping = var_mapping }
let get env logic_v =
try
let varinfos = Logic_var.Map.find logic_v env.var_mapping in
......@@ -337,6 +348,10 @@ let current_kf env =
| 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
......
......@@ -68,6 +68,9 @@ 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_existing_vi: t -> logic_var -> varinfo -> t
(* [add_existing_vi env lv vi] defines [vi] as latest C binding for [lv]. *)
val get: t -> logic_var -> varinfo
(* Return the latest C binding. *)
......@@ -142,6 +145,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} *)
(* ************************************************************************** *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
type ival_exp =
| Iconst of Ival.t
| Ivar of string * logic_type list
| Ibinop of ival_binop * ival_exp * ival_exp
| Iunsupported
let equal_ivar ivar1 ivar2 = match ivar1, ivar2 with
| Ivar(str1, ltys1), Ivar(str2, ltys2) ->
str1 = str2 &&
List.fold_left2
(fun b lty1 lty2 -> b && Cil_datatype.Logic_type.equal lty1 lty2)
true
ltys1
ltys2
| _ ->
Options.fatal "not an ivar"
module Ieqs: sig
type t
val empty: t
val add: ival_exp -> ival_exp -> t -> t
val find: ival_exp -> t -> ival_exp
val cardinal: t -> int
val fold: (ival_exp -> ival_exp -> 'a -> 'a) -> t -> 'a -> 'a
val map: (ival_exp -> ival_exp) -> t -> t
end = struct
module H = Map.Make(struct
type t = ival_exp (* an Ivar to be precise *)
let compare ivar1 ivar2 = if equal_ivar ivar1 ivar2 then 0 else 1
end)
type t = ival_exp H.t
let empty = H.empty
let add ivar iexp ieqs = match ivar with
| Ivar _ -> H.add ivar iexp ieqs
| _ -> Options.fatal "left-hand side is NOT an ivar"
let find = H.find
let map = H.map
let fold = H.fold
let cardinal = H.cardinal
end
(* Normalize the expression.
An expression is said to be normalized if it is:
- either Iunsupported
- or an expression that contains no Iunsupported *)
let normalize_iexp iexp =
let rec has_unsupported iexp = match iexp with
| Iunsupported | Ibinop(_, Iunsupported, _) | Ibinop(_, _, Iunsupported) ->
true
| Ibinop(_, (Iconst _ | Ivar _), (Iconst _ | Ivar _))
| Iconst _ | Ivar _ ->
false
| Ibinop(_, iexp1, iexp2) ->
has_unsupported iexp1 || has_unsupported iexp2
in
if has_unsupported iexp then Iunsupported else iexp
let normalize_ieqs ieqs =
Ieqs.map (fun iexp -> normalize_iexp iexp) ieqs
let ivars_contains_ivar ivars ivar =
List.fold_left (fun b ivar' -> b || equal_ivar ivar ivar') false ivars
let get_ival_of_iconst ieqs ivar = match Ieqs.find ieqs ivar with
| Iconst i -> i
| Ivar _ | Ibinop _| Iunsupported -> Options.fatal "not an Iconst"
(*************************************************************************)
(******************************** Solver *********************************)
(*************************************************************************)
(* [iterate indexes max] increases by 1 the leftmost element of [indexes] that
is less or equal to [max].
Eg: from index=[| 0; 0; 0 |] and max=2, the successive iterates
until reaching index=[| max; max; max |] are as follows:
[| 0; 0; 0 |]
[| 1; 0; 0 |]
[| 1; 1; 0 |]
[| 1; 1; 1 |]
[| 2; 1; 1 |]
[| 2; 2; 1 |]
[| 2; 2; 2 |]
Note that the number [N] of iterates is linear in [max*l] where [l] is the
length of [index]: [N=max*l+1].
[int array] (instead of [int list]) is the proper data structure for storing
[indexes], at least because its length is known in advance: the number of
variables. *)
let iterate indexes max =
let min_i = ref 0 in
for indexes_i = 1 to Array.length indexes - 1 do
if indexes.(indexes_i) < indexes.(!min_i) then min_i := indexes_i
done;
if indexes.(!min_i) + 1 <= max then
(* The if-test is because the last iterate cannot be increased *)
indexes.(!min_i) <- indexes.(!min_i) + 1
(* Returns an assignement to each variable of [ieqs] such that:
- the first (resp. the second... the last) element of [indexes] is
associated to the first (resp. the second... the last) variable of [ieqs]
- a variable that is associated to an index [index] ranging in
[0..max-1] will be given the interval of finite bounds:
[-chain_of_ivalmax.(index), chain_of_ivalmax.(index)]
  - a variable that is associated to an index [index] equaling [max] will
be given the whole interval of integers [Z]. *)
let to_iconsts indexes ieqs chain_of_ivalmax =
let max = Array.length chain_of_ivalmax in
let indexes_i = ref 0 in
Ieqs.map
(fun _ ->
let ival =
let index = indexes.(!indexes_i) in
if index < max then
let ivalmax = chain_of_ivalmax.(index) in
Ival.inject_range (Some (Integer.neg ivalmax)) (Some ivalmax)
else if
index = max then Ival.inject_range None None
else
assert false
in
indexes_i := !indexes_i + 1;
Iconst ival)
ieqs
(* Assumes [iexp] to be a normalized [ival_exp] and evaluates it when each of
its variable is replaced by the corresponding interval from [iconsts]. *)
let rec eval_iexp iexp iconsts =
match iexp with
| Iunsupported ->
Iconst (Ival.inject_range None None)
| Iconst _ ->
iexp
| Ivar _ ->
Ieqs.find iexp iconsts
| Ibinop(_, Iunsupported, _) | Ibinop(_, _, Iunsupported) ->
assert false (* because [iexp] has been normalized *)
| Ibinop(ibinop, iexp1, iexp2) ->
let i1 = match eval_iexp iexp1 iconsts with
| Iconst i -> i
| Iunsupported | Ivar _ | Ibinop _ -> assert false
in
let i2 = match eval_iexp iexp2 iconsts with
| Iconst i -> i
| Iunsupported | Ivar _ | Ibinop _ -> assert false
in
match ibinop with
| Ival_add -> Iconst (Ival.add_int i1 i2)
| Ival_min -> Iconst (Ival.sub_int i1 i2)
| Ival_mul -> Iconst (Ival.mul i1 i2)
| Ival_div -> Iconst (Ival.div i1 i2)
| Ival_union -> Iconst (Ival.join i1 i2)
let equal_iconst iconst1 iconst2 =
let i1 = match iconst1 with
| Iconst i -> i
| Iunsupported | Ivar _ | Ibinop _ -> assert false
in
let i2 = match iconst2 with
| Iconst i -> i
| Iunsupported | Ivar _ | Ibinop _ -> assert false
in
Ival.is_included i1 i2
let is_post_fixpoint ieqs iconsts = Ieqs.fold
(fun ivar iexp b ->
let iconst1 = eval_iexp iexp iconsts in
let iconst2 = Ieqs.find ivar iconsts in
b && equal_iconst iconst1 iconst2)
ieqs
true
let rec iterate_till_post_fixpoint ieqs indexes chain_of_ivalmax =
let iconsts = to_iconsts indexes ieqs chain_of_ivalmax in
if is_post_fixpoint ieqs iconsts then
iconsts
else
let index_max = Array.length chain_of_ivalmax in
iterate indexes index_max;
iterate_till_post_fixpoint ieqs indexes chain_of_ivalmax
let solve ieqs ivar chain_of_ivalmax =
let ieqs = normalize_ieqs ieqs in
let dim = Ieqs.cardinal ieqs in
let bottom = Array.make dim 0 in
let post_fixpoint =
iterate_till_post_fixpoint ieqs bottom chain_of_ivalmax
in
get_ival_of_iconst ivar post_fixpoint
\ No newline at end of file
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
(** Fixpoint equation solver for infering intervals of
recursively defined logic functions *)
(**************************************************************************)
(*************************** Constructors *********************************)
(**************************************************************************)
type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
type ival_exp =
| Iconst of Ival.t
| Ivar of string (* function name *) * logic_type list (* args lty *)
(** Example: to the function signature f(int, long) corresponds
the expression Ivar("f", [int; long]) *)
| Ibinop of ival_binop * ival_exp * ival_exp
| Iunsupported
module Ieqs: sig
type t
(** [Ieqs.t] represents systems of equations over [ival_exp] expressions in
which the variables to be found are the [Ivar] constructs.
[Ieqs.t] can be viewed as a fixpoint equation in the sense that the left-
hand side of the equation MUST be an [Ivar]:
solving the system [(S): x1=f1(x1, ..., xn) /\ ... /\ xn=fn(x1, ..., xn)]
is equivalent to solving the fixpoint equation [(E): X=F(X)] where
X=(x1, ..., xn) and F=(f1, ..., fn). *)
val empty: t
val add:
ival_exp (* left-hand side, MUST be an [Ivar] *) -> ival_exp -> t -> t
end
(**************************************************************************)
(***************************** Solver *************************************)
(**************************************************************************)
val solve: Ieqs.t -> ival_exp -> Integer.t array -> Ival.t
(** [solve ieqs ivar chain] finds an interval for the variable [ivar]
that satisfies the fixpoint equation [ieqs]. The solver is parameterized
by the increasingly sorted array [chain] of positive integers.
For chain=[n1; n2; ...; nk] where n1 < ... < nk, [solve] will
consider the following set S of intervals as potential solution:
S={[-n1, n1], [-n2, n2]... [-nk; nk]}. Then [solve] will iteratively
affect intervals from S to the different variables of [ieqs],
starting from the smallest interval [-n1, n1] to the biggest one [-nk,
nk], until finding the smallest combination that satisfies [ieqs].
If no combination is found then [solve] returns Z. *)
(**************************************************************************)
(****************************** Utils *************************************)
(**************************************************************************)
val ivars_contains_ivar: ival_exp list -> ival_exp -> bool
(** [contains ivars ivar] checks whether the list of Ivar [ivars] contains the
Ivar [ivar]. *)
\ No newline at end of file
......@@ -28,12 +28,32 @@ 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 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 ())
let apply_on_var ~loc funname e = Misc.mk_call ~loc ("__gmpz_" ^ funname) [ e ]
......@@ -106,6 +126,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 *)
......
......@@ -47,6 +47,16 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
| _ ->
raise Not_an_integer
(* Return the interval over which ranges the smallest typ containing [i]. *)
let interv_of_typ_containing_interv i =
try
let itv_kind = Misc.itv_kind i in
(* convert the kind to [IInt] whenever smaller. *)
let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
interv_of_typ (TInt(kind, []))
with Cil.Not_representable ->
Ival.inject_range None None
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 *)
......@@ -62,6 +72,7 @@ module Env = struct
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
let replace = Logic_var.Hashtbl.replace tbl
let find_all = Logic_var.Hashtbl.find_all tbl
let find = Logic_var.Hashtbl.find tbl
end
......@@ -185,7 +196,64 @@ let rec infer t =
| 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 Linteger ->
begin match li.l_body with
| LBpred _ ->
Ival.zero_or_one
| LBterm t' ->
let i =
if Misc.is_recursive li then
(* 1) Build a system of interval equations that
constrain the solution:
do so by returning a variable when encoutering
a call of a recursive function instead of
performing the usual interval inference
BEWARE: we might be tempted to memoize the
solution for a given function signature
HOWEVER: it cannot be done in a straightforward
manner due to the cases of functions that use
C (global) variables in their definition (as the values of
those variables can change between two function calls). *)
let ieqs = Fixpoint.Ieqs.empty in
let ivar, ieqs, _ = build_ieqs t ieqs [] in
(* 2) Solve it:
The problem is probably undecidable in the general case.
Thus we just look for reasonably precise approximations
without being too computationally expensive:
simply iterate over a finite set of pre-defined intervals.
See [Fixpoint.solve] for details. *)
let chain_of_ivalmax =
[| Integer.one; Integer.billion_one; Integer.max_int64 |]
(* This set can be changed based on experimental evidences,
but it works fine for now. *)
in
let i = Fixpoint.solve ieqs ivar chain_of_ivalmax in
i
else begin
List.iter2
(fun lv arg ->
try
let i = interv_of_typ_containing_interv (infer arg) in
Env.add lv i
with Not_an_integer -> ())
li.l_profile
_args;
let i =
try infer t'
with Not_an_integer -> Ival.inject_range None None
in
List.iter (fun lv -> Env.remove lv) li.l_profile;
i
end
in
i
| LBnone ->
Error.not_yet "logic functions with no definition nor reads clause"
| LBreads _ ->
Error.not_yet "logic functions performing read accesses"
| LBinductive _ ->
Error.not_yet "logic functions inductively defined"
end
| Some (Ctype ty) -> interv_of_typ ty
| Some _ -> raise Not_an_integer)
| Tunion _ -> Error.not_yet "tset union"
......@@ -227,10 +295,21 @@ and infer_term_lval (host, offset as tlv) =
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
and infer_term_host = function
and infer_term_host h = match h with
| TVar v ->
(try Env.find v
with Not_found -> interv_of_typ (Logic_utils.logicCType v.lv_type))
with Not_found ->
match v.lv_type with
| Linteger ->
Ival.inject_range None None
| Ctype (TFloat _) -> (* TODO: handle in MR !226 *)
raise Not_an_integer
| Lreal ->
Error.not_yet "real numbers"
| Ctype _ ->
interv_of_typ (Logic_utils.logicCType v.lv_type)
| Ltype _ | Lvar _ | Larrow _ ->
Options.fatal "unexpected logic type")
| TResult ty -> interv_of_typ ty
| TMem t ->
let ty = Logic_utils.logicCType t.term_type in
......@@ -241,6 +320,81 @@ and infer_term_host = function
Printer.pp_typ ty
Printer.pp_term t
(* Build the system of interval equations for the logic function called
through [t].
Example: the following function:
f(Z n) = n < 0 ? 1 : f(n - 1) * f(n - 2) / f(n - 3)
when called with f(37)
will generate the following system of equations:
X = [1; 1] U Y*Y/Y /\
Y = [1; 1] U Z*Z/Z /\
Z = [1; 1] U Z*Z/Z
where X is the interval for f(int) (since 37 \in int),
Y the one for f(long) (from int-1, int-2 and int-3)
and Z the for the f(Z) (from long-1, long-2 and long-3) *)
and build_ieqs t ieqs ivars =
match t.term_node with
| Tapp(li, _, args) ->
if li.l_type = Some Linteger && Misc.is_recursive li then begin
let args_lty = List.map2
(fun lv arg ->
try
let i = interv_of_typ_containing_interv (infer arg) in
Env.add lv i;
Ctype (TInt(Misc.itv_kind i, []))
with
| Cil.Not_representable -> Linteger
| Not_an_integer -> lv.lv_type)
li.l_profile
args
in
(* x *)
let ivar = Fixpoint.Ivar(li.l_var_info.lv_name, args_lty) in
(* Adding x = g(x) if it is not yet in the system of equations.
Without this check, the algorithm would not terminate. *)
let ieqs, ivars =
if Fixpoint.ivars_contains_ivar ivars ivar then ieqs, ivars
else
let iexp, ieqs, ivars =
build_ieqs (Misc.term_of_li li) ieqs (ivar :: ivars)
in
let ieqs = Fixpoint.Ieqs.add ivar iexp ieqs in (* Adding x = g(x) *)
ieqs, ivars
in
List.iter (fun lv -> Env.remove lv) li.l_profile;
ivar, ieqs, ivars
end else
(try Fixpoint.Iconst(infer t), ieqs, ivars
with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
| TConst _ ->
(try Fixpoint.Iconst(infer t), ieqs, ivars
with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
| TLval(TVar _, _) ->
(try Fixpoint.Iconst(infer t), ieqs, ivars
with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
| TBinOp (PlusA, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
Fixpoint.Ibinop(Fixpoint.Ival_add, iexp1, iexp2), ieqs, ivars
| TBinOp (MinusA, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
Fixpoint.Ibinop(Fixpoint.Ival_min, iexp1, iexp2), ieqs, ivars
| TBinOp (Mult, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
Fixpoint.Ibinop(Fixpoint.Ival_mul, iexp1, iexp2), ieqs, ivars
| TBinOp (Div, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
Fixpoint.Ibinop(Fixpoint.Ival_div, iexp1, iexp2), ieqs, ivars
| Tif(_, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
Fixpoint.Ibinop(Fixpoint.Ival_union, iexp1, iexp2), ieqs, ivars
| _ ->
Fixpoint.Iunsupported, ieqs, ivars
(*
Local Variables:
compile-command: "make"
......