diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index b463daa3ac3b49fe3278cbb5e441cc55547f1616..9885e91f906753840ce881721d36d571f5f1729e 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -48,16 +48,78 @@ let intraprocedural () = not (Parameters.OctagonCall.get ())
(* Basic types: pair of variables and Ival.t *)
(* -------------------------------------------------------------------------- *)
+type kind = Integer | Float
+
+let typ_kind typ =
+ match Cil.unrollType typ with
+ | TInt _ | TEnum _ -> Integer
+ | TFloat _ -> Float
+ | _ -> assert false
+
+(* Abstract interface for the variables used by the octagons. *)
+module type Variable = sig
+ include Datatype.S_with_collections
+ (* Creates a variable from a varinfo. Should be extended to support more
+ lvalues. *)
+ val make: varinfo -> t
+ val make_int: varinfo -> t
+ (* Returns all variables that may have been created for a varinfo. *)
+ val get_all: varinfo -> t list
+ val kind: t -> kind (* The kind of the variable: integer or float. *)
+ val lval: t -> lval option (* The CIL lval corresponding to the variable. *)
+ val base: t -> Base.t (* Base of the variable. *)
+ val id: t -> int (* Unique id, needed to use variables as hptmap keys. *)
+end
+
(* Variables of the octagons. Should be extended later to also include
symbolic lvalues. *)
-module Variable = struct
- include Cil_datatype.Varinfo
- let id v = v.vid
-end
+module Variable : Variable = struct
+ type var =
+ | Var of varinfo
+ | Int of varinfo
+
+ let id = function
+ | Var vi -> 2 * vi.vid
+ | Int vi -> 2 * vi.vid + 1
+
+ module Datatype_Input = struct
+ include Datatype.Undefined
+ type t = var
+ let name = "Eva.Octagons.Variable"
+ let structural_descr = Structural_descr.t_abstract
+ let reprs = [ Var (List.hd Cil_datatype.Varinfo.reprs) ]
+
+ let compare x y =
+ match x, y with
+ | Var x, Var y
+ | Int x, Int y -> Cil_datatype.Varinfo.compare x y
+ | Var _, Int _ -> -1
+ | Int _, Var _ -> 1
+
+ let equal x y = compare x y = 0
+
+ let hash = id
+ let rehash = Datatype.identity
+
+ let pretty fmt = function
+ | Var vi -> Printer.pp_varinfo fmt vi
+ | Int vi -> Format.fprintf fmt "(integer)%a" Printer.pp_varinfo vi
+ end
-module VariableSet = struct
- include Variable.Set
- let pretty_debug = pretty
+ include Datatype.Make_with_collections (Datatype_Input)
+ let make vi = Var vi
+ let make_int vi = Int vi
+ let get_all vi = [ Var vi; Int vi ]
+
+ let kind = function
+ | Var vi -> typ_kind vi.vtype
+ | Int _ -> Integer
+
+ let lval = function
+ | Var vi -> Some (Cil_types.Var vi, NoOffset)
+ | Int _ -> None
+
+ let base = function Var vi | Int vi -> Base.of_varinfo vi
end
(* Pairs of related variables in an octagon.
@@ -76,11 +138,15 @@ module Pair = struct
(* Creates a pair, and also returns a boolean that is [true] if x, y are
swapped in the pair. *)
let make x y =
- assert (x.vid <> y.vid);
- let pair, swap = if x.vid < y.vid then (x, y), false else (y, x), true in
+ let x_id = Variable.id x
+ and y_id = Variable.id y in
+ assert (x_id <> y_id);
+ if debug then assert (Variable.kind x = Variable.kind y);
+ let pair, swap = if x_id < y_id then (x, y), false else (y, x), true in
hashcons pair, swap
let fst t = fst (get t)
+ let kind t = Variable.kind (fst t)
end
@@ -114,12 +180,11 @@ module Arith = struct
then neg_int ival
else inject_float (Fval.neg (project_float ival))
- let int_or_float_operation i_op f_op = fun typ ->
- match Cil.unrollType typ with
- | TInt _ | TEnum _ -> i_op
- | TFloat _ -> fun i1 i2 ->
- inject_float (f_op Fval.Real (project_float i1) (project_float i2))
- | _ -> assert false
+ let int_or_float_operation i_op f_op = function
+ | Integer -> i_op
+ | Float ->
+ fun i1 i2 ->
+ inject_float (f_op Fval.Real (project_float i1) (project_float i2))
let sub = int_or_float_operation Ival.sub_int Fval.sub
let add = int_or_float_operation Ival.add_int Fval.add
@@ -150,7 +215,7 @@ let _pretty_octagon fmt octagon =
let x, y = Pair.get octagon.variables in
let op = match octagon.operation with Add -> "+" | Sub -> "-" in
Format.fprintf fmt "%a %s %a %s %a"
- Printer.pp_varinfo x op Printer.pp_varinfo y
+ Variable.pretty x op Variable.pretty y
(Unicode.inset_string ()) Ival.pretty octagon.value
(* Transforms Cil expressions into mathematical octagons.
@@ -186,11 +251,11 @@ module Rewriting = struct
(* Simplified form [±X-coeff] for expressions,
where X is a variable and coeff an interval. *)
- type var_coeff = { varinfo: varinfo; sign: bool; coeff: Ival.t; }
+ type var_coeff = { var: Variable.t; sign: bool; coeff: Ival.t; }
(* Negates a simplified form. *)
- let neg { varinfo; sign; coeff } =
- { varinfo; sign = not sign; coeff = Arith.neg coeff }
+ let neg { var; sign; coeff } =
+ { var; sign = not sign; coeff = Arith.neg coeff }
(* Is the interval computed for a variable a singleton? *)
let is_singleton = function
@@ -209,11 +274,11 @@ module Rewriting = struct
let apply_binop f evaluate typ e1 op e2 =
evaluate e1 >> fun v1 ->
evaluate e2 >> fun v2 ->
- let typ_e1 = Cil.typeOf e1 in
- let result = Arith.apply op typ_e1 v1 v2 in
+ let kind = typ_kind (Cil.typeOf e1) in
+ let result = Arith.apply op kind v1 v2 in
if may_overflow typ result
then []
- else f typ_e1 v1 v2
+ else f kind v1 v2
(* Rewrites the Cil expression [expr] into the simplified form [±x-coeff],
where [x] is a non-singleton variable and [coeff] is an interval. The
@@ -230,7 +295,9 @@ module Rewriting = struct
if Cil.isIntegralType varinfo.vtype
&& not (Cil.typeHasQualifier "volatile" varinfo.vtype)
&& not (is_singleton (evaluate expr))
- then [ { varinfo; sign = true; coeff = Ival.zero } ]
+ then
+ let var = Variable.make varinfo in
+ [ { var; sign = true; coeff = Ival.zero } ]
else []
| UnOp (Neg, e, typ) ->
@@ -254,6 +321,15 @@ module Rewriting = struct
in
apply_binop rewrite_binop evaluate typ e1 op e2
+ | CastE (typ, { enode = Lval (Var vi, NoOffset) })
+ when Cil.isIntegralType typ
+ && Cil.isFloatingType vi.vtype
+ && not (Cil.typeHasQualifier "volatile" vi.vtype)
+ && not (is_singleton (evaluate expr)) ->
+ let var = Variable.make_int vi in
+ [ { var; sign = true; coeff = Ival.zero } ]
+
+
| CastE (typ, e) ->
if Cil.(isIntegralType typ && isIntegralType (typeOf e)) then
evaluate e >> fun v ->
@@ -264,20 +340,21 @@ module Rewriting = struct
(* Rewrites the operation [e1 ± e2] into equivalent octagons ±(X±Y-value). *)
let rewrite_binop evaluate e1 binop e2 =
+ let kind = typ_kind (Cil.typeOf e1) in
let vars1 = rewrite evaluate e1 in
let vars2 = rewrite evaluate e2 in
let vars2 = if binop = Sub then List.map neg vars2 else vars2 in
let aux acc var1 var2 =
- if Cil_datatype.Varinfo.equal var1.varinfo var2.varinfo
+ if Variable.equal var1.var var2.var
then acc
else
- let variables, swap = Pair.make var1.varinfo var2.varinfo in
+ let variables, swap = Pair.make var1.var var2.var in
let operation = if var1.sign = var2.sign then Add else Sub in
let sign = match operation with
| Add -> var1.sign
| Sub -> if swap then var2.sign else var1.sign
in
- let value = Arith.add (Cil.typeOf e1) var1.coeff var2.coeff in
+ let value = Arith.add kind var1.coeff var2.coeff in
let value = if sign then value else Arith.neg value in
(sign, { variables; operation; value }) :: acc
in
@@ -297,13 +374,13 @@ module Rewriting = struct
(* Transforms the constraint [expr] ∈ [ival] into a list of octagonal
constraints. *)
let make_octagons evaluate expr ival =
- let make_octagons_from_binop typ e1 op e2 ival =
+ let make_octagons_from_binop kind e1 op e2 ival =
(* equivalent octagonal forms ±(X±Y-v) for [e1 op e2]. *)
let rewritings = rewrite_binop evaluate e1 op e2 in
(* create the final octagon, knowning that [e1 op e2] ∈ [ival]. *)
let make_octagon (sign, octagon) =
let ival = if sign then ival else Arith.neg ival in
- let value = Arith.add typ ival octagon.value in
+ let value = Arith.add kind ival octagon.value in
{ octagon with value }
in
List.map make_octagon rewritings
@@ -324,7 +401,7 @@ module Rewriting = struct
if Ival.is_zero ival then Abstract_interp.Comp.inv comp else comp
in
let range = comparison_range comp in
- make_octagons_from_binop typ e1 Sub e2 range
+ make_octagons_from_binop (typ_kind typ) e1 Sub e2 range
| _ -> []
let overflow_alarms typ expr ival =
@@ -370,10 +447,10 @@ module Rewriting = struct
let octagons = rewrite_binop evaluate_expr e1 op e2 in
let ival = evaluate_octagons octagons in
if Ival.(equal top ival) then default else
- let typ_e1 = Cil.typeOf e1 in
+ let kind = typ_kind (Cil.typeOf e1) in
let ival2 =
match evaluate_expr e1, evaluate_expr e2 with
- | `Value v1, `Value v2 -> Arith.apply op typ_e1 v1 v2
+ | `Value v1, `Value v2 -> Arith.apply op kind v1 v2
| _, _ -> Ival.top
in
let ival = Ival.narrow ival ival2 in
@@ -577,8 +654,8 @@ module Octagons = struct
if Ival.(equal top ival)
then None
else
- let typ = (Pair.fst octagon.variables).vtype in
- let ival = Arith.sub typ ival octagon.value in
+ let kind = Pair.kind octagon.variables in
+ let ival = Arith.sub kind ival octagon.value in
Some ival
with Not_found -> None
end
@@ -592,7 +669,8 @@ module Relations = struct
module Initial_Values = struct let v = [[]] end
module Dependencies = struct let l = [ Ast.self ] end
- include Hptmap.Make (Variable) (VariableSet)
+ include Hptmap.Make (Variable)
+ (struct include Variable.Set let pretty_debug = pretty end)
(Hptmap.Comp_unused) (Initial_Values) (Dependencies)
let inter =
@@ -612,9 +690,9 @@ module Relations = struct
let relate_aux x y t =
let related =
try find x t
- with Not_found -> VariableSet.empty
+ with Not_found -> Variable.Set.empty
in
- let updated = VariableSet.add y related in
+ let updated = Variable.Set.add y related in
add x updated t
(* Marks x and y as mutually related. *)
@@ -623,7 +701,7 @@ module Relations = struct
relate_aux y x (relate_aux x y t)
let add variable set t =
- if VariableSet.is_empty set
+ if Variable.Set.is_empty set
then remove variable t
else add variable set t
end
@@ -725,7 +803,7 @@ module State = struct
let hash t =
Hashtbl.hash (Octagons.hash t.octagons,
- Relations.hash t.relations,
+ Intervals.hash t.intervals,
Zone.hash t.modified)
let pretty fmt { octagons } =
@@ -751,8 +829,8 @@ module State = struct
between them. *)
let check_octagon pair _ =
let x, y = Pair.get pair in
- try VariableSet.mem x (Relations.find y t.relations)
- && VariableSet.mem y (Relations.find x t.relations)
+ try Variable.Set.mem x (Relations.find y t.relations)
+ && Variable.Set.mem y (Relations.find x t.relations)
with Not_found -> false
in
if Octagons.for_all check_octagon t.octagons
@@ -771,7 +849,7 @@ module State = struct
let v1, v2 = Pair.get variables in
let i1 = Intervals.find v1 intervals
and i2 = Intervals.find v2 intervals in
- let i = Arith.apply operation v1.vtype i1 i2 in
+ let i = Arith.apply operation (Variable.kind v1) i1 i2 in
Ival.is_included i value
with Not_found -> false
else false
@@ -809,8 +887,9 @@ module State = struct
try
let i1 = Intervals.find v1 intervals
and i2 = Intervals.find v2 intervals in
- let add = Arith.add v1.vtype i1 i2
- and sub = Arith.sub v1.vtype i1 i2 in
+ let kind = Variable.kind v1 in
+ let add = Arith.add kind i1 i2
+ and sub = Arith.sub kind i1 i2 in
let diamond = Diamond.join diamond { add; sub } in
if Diamond.is_top diamond then None else Some diamond
with Not_found -> None
@@ -841,8 +920,9 @@ module State = struct
try
let i1 = Intervals.find v1 intervals
and i2 = Intervals.find v2 intervals in
- let add = Arith.add v1.vtype i1 i2
- and sub = Arith.sub v1.vtype i1 i2 in
+ let kind = Variable.kind v1 in
+ let add = Arith.add kind i1 i2
+ and sub = Arith.sub kind i1 i2 in
let diamond =
if b
then Diamond.widen { add; sub } diamond
@@ -877,7 +957,7 @@ module State = struct
(* -------------- Transitive closure when adding an octagon --------------- *)
type relation =
- { vars: varinfo * varinfo;
+ { vars: Variable.t * Variable.t;
diamond: diamond; }
let add_diamond state variables diamond =
@@ -899,17 +979,17 @@ module State = struct
if Variable.equal y (fst rel2.vars) then rel2 else inverse rel2
in
(* rel1 is about X±Y, rel2 is about Y±Z. *)
- let typ = y.vtype in
+ let kind = Variable.kind y in
(* X+Z = (X+Y) - (Y-Z) and X+Y = (X-Y) + (Y+Z) *)
let add =
Ival.narrow
- (Arith.sub typ rel1.diamond.add rel2.diamond.sub)
- (Arith.add typ rel1.diamond.sub rel2.diamond.add)
+ (Arith.sub kind rel1.diamond.add rel2.diamond.sub)
+ (Arith.add kind rel1.diamond.sub rel2.diamond.add)
(* X-Z = (X+Y) - (Y+Z) and X-Z = (X-Y) + (Y-Z) *)
and sub =
Ival.narrow
- (Arith.sub typ rel1.diamond.add rel2.diamond.add)
- (Arith.add typ rel1.diamond.sub rel2.diamond.sub)
+ (Arith.sub kind rel1.diamond.add rel2.diamond.add)
+ (Arith.add kind rel1.diamond.sub rel2.diamond.sub)
in
let diamond = {add; sub} in
let pair, swap = Pair.make (fst rel1.vars) (snd rel2.vars) in
@@ -919,7 +999,7 @@ module State = struct
let saturate state x y rel1 =
try
let y_related = Relations.find y state.relations in
- let y_related = VariableSet.remove x y_related in
+ let y_related = Variable.Set.remove x y_related in
let aux z state =
state >>- fun state ->
try
@@ -931,11 +1011,11 @@ module State = struct
add_diamond state pair diamond
with Not_found -> `Value state
in
- VariableSet.fold aux y_related (`Value state)
+ Variable.Set.fold aux y_related (`Value state)
with Not_found -> `Value state
let add_octagon state octagon =
- if is_redundant state.intervals octagon
+ if Ival.(equal top octagon.value) || is_redundant state.intervals octagon
then `Value state
else
let state =
@@ -956,6 +1036,11 @@ module State = struct
let relations = Relations.relate octagon.variables state.relations in
{ state with octagons; relations }
+ let add_diamond state variables diamond =
+ add_octagon state { variables; operation = Add; value = diamond.add }
+ >>- fun state ->
+ add_octagon state { variables; operation = Sub; value = diamond.sub }
+
let remove state x =
let intervals = Intervals.remove x state.intervals in
let state = { state with intervals } in
@@ -964,14 +1049,14 @@ module State = struct
let remove_one y state =
try
let yrelations = Relations.find y state.relations in
- let yrelations = VariableSet.remove x yrelations in
+ let yrelations = Variable.Set.remove x yrelations in
let relations = Relations.add y yrelations state.relations in
let pair, _ = Pair.make x y in
let octagons = Octagons.remove pair state.octagons in
{ state with octagons; relations }
with Not_found -> state
in
- let state = VariableSet.fold remove_one relations state in
+ let state = Variable.Set.fold remove_one relations state in
let relations = Relations.remove x state.relations in
{ state with relations }
with Not_found -> state
@@ -987,7 +1072,7 @@ module State = struct
(y, diamond) :: acc
with Not_found -> acc
in
- VariableSet.fold aux related []
+ Variable.Set.fold aux related []
with Not_found -> []
(* x' = ±x - delta *)
@@ -1007,23 +1092,23 @@ module State = struct
sub = op diamond.add }
else diamond
in
- let typ = x.vtype in
+ let kind = Variable.kind x in
let op = if swap then Arith.add else Arith.sub in
let add =
if Ival.(equal top diamond.add)
then diamond.add
- else Arith.sub typ diamond.add delta
+ else Arith.sub kind diamond.add delta
and sub =
if Ival.(equal top diamond.sub)
then diamond.sub
- else op typ diamond.sub delta
+ else op kind diamond.sub delta
in
let diamond' = { add; sub } in
let octagons = Octagons.unsafe_add pair diamond' state.octagons in
{ state with octagons }
with Not_found -> state
in
- VariableSet.fold aux x_related state
+ Variable.Set.fold aux x_related state
end
(* -------------------------------------------------------------------------- *)
@@ -1067,24 +1152,29 @@ module Domain = struct
begin
try
let x_ival = Cvalue.V.project_ival value in
- let octagons = State.related_octagons state x in
+ let var = Variable.make x in
+ let kind = Variable.kind var in
+ let octagons = State.related_octagons state var in
let reduce acc (y, octagons) =
- let y_ival1 =
- if Ival.(equal top octagons.add)
- then Ival.top
- else Arith.sub x.vtype octagons.add x_ival
- in
- let y_ival2 =
- if Ival.(equal top octagons.sub)
- then Ival.top
- else Arith.sub x.vtype x_ival octagons.sub
- in
- let y_ival = Ival.narrow y_ival1 y_ival2 in
- if Ival.(equal top y_ival) then acc else
- let y_enode = Lval (Var y, NoOffset) in
- let y_expr = Cil.new_exp ~loc:expr.eloc y_enode in
- let y_cvalue = Cvalue.V.inject_ival y_ival in
- (y_expr, y_cvalue) :: acc
+ match Variable.lval y with
+ | None -> acc
+ | Some lval ->
+ let y_ival1 =
+ if Ival.(equal top octagons.add)
+ then Ival.top
+ else Arith.sub kind octagons.add x_ival
+ in
+ let y_ival2 =
+ if Ival.(equal top octagons.sub)
+ then Ival.top
+ else Arith.sub kind x_ival octagons.sub
+ in
+ let y_ival = Ival.narrow y_ival1 y_ival2 in
+ if Ival.(equal top y_ival) then acc else
+ let y_enode = Lval lval in
+ let y_expr = Cil.new_exp ~loc:expr.eloc y_enode in
+ let y_cvalue = Cvalue.V.inject_ival y_ival in
+ (y_expr, y_cvalue) :: acc
in
List.fold_left reduce [] octagons
with Cvalue.V.Not_based_on_null -> []
@@ -1095,7 +1185,8 @@ module Domain = struct
let kill_base base state =
try
let varinfo = Base.to_varinfo base in
- State.remove state varinfo
+ let vars = Variable.get_all varinfo in
+ List.fold_left State.remove state vars
with Base.Not_a_C_variable -> state
let kill zone state =
@@ -1135,7 +1226,8 @@ module Domain = struct
match expr.enode with
| Lval (Var varinfo, NoOffset)
when Cil.isIntegralType varinfo.vtype ->
- let intervals = Intervals.add varinfo ival state.intervals in
+ let var = Variable.make varinfo in
+ let intervals = Intervals.add var ival state.intervals in
{ state with intervals }
| _ -> state
@@ -1157,7 +1249,7 @@ module Domain = struct
try `Value (check "update" (valuation.Abstract_domain.fold aux state))
with EBottom -> `Bottom
- let assign_interval varinfo assigned state =
+ let assign_interval variable assigned state =
if not infer_intervals
then state
else
@@ -1167,7 +1259,7 @@ module Domain = struct
begin
try
let ival = Cvalue.V.project_ival v in
- let intervals = Intervals.add varinfo ival state.intervals in
+ let intervals = Intervals.add variable ival state.intervals in
{ state with intervals }
with Cvalue.V.Not_based_on_null -> state
end
@@ -1177,15 +1269,16 @@ module Domain = struct
let evaluate = evaluation_function valuation in
(* TODO: redundant with rewrite_binop below. *)
let vars = Rewriting.rewrite evaluate expr in
- let equal_varinfo v = Variable.equal varinfo v.Rewriting.varinfo in
+ let variable = Variable.make varinfo in
+ let equal_varinfo v = Variable.equal variable v.Rewriting.var in
let state =
try
let var = List.find equal_varinfo vars in
let inverse = not var.Rewriting.sign in
- State.sub_delta ~inverse state varinfo var.Rewriting.coeff
- with Not_found -> State.remove state varinfo
+ State.sub_delta ~inverse state variable var.Rewriting.coeff
+ with Not_found -> State.remove state variable
in
- let state = assign_interval varinfo assigned state in
+ let state = assign_interval variable assigned state in
let enode = Lval (Var varinfo, NoOffset) in
let left_expr = Cil.new_exp ~loc:expr.eloc enode in
(* On the assignment X = E; if X-E can be rewritten as ±(X±Y-v),
@@ -1216,6 +1309,7 @@ module Domain = struct
let start_recursive_call recursion state =
let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ let vars = List.flatten (List.map Variable.get_all vars) in
List.fold_left State.remove state vars
let start_call _stmt call recursion valuation state =
@@ -1251,7 +1345,8 @@ module Domain = struct
let enter_scope _kind _varinfos state = state
let leave_scope _kf varinfos state =
- let state = List.fold_left State.remove state varinfos in
+ let vars = List.flatten (List.map Variable.get_all varinfos) in
+ let state = List.fold_left State.remove state vars in
check "leave_scope" state
let initialize_variable _lval _location ~initialized:_ _value state = state
@@ -1261,35 +1356,37 @@ module Domain = struct
if intraprocedural ()
then Base.SetLattice.empty
else
+ let add_related_bases acc var =
+ let related = Relations.find var state.relations in
+ Variable.Set.fold
+ (fun var -> Base.Hptset.add (Variable.base var))
+ related acc
+ in
let aux base acc =
try
let varinfo = Base.to_varinfo base in
- let varset = Relations.find varinfo state.relations in
- let baseset =
- VariableSet.fold
- (fun vi acc -> Base.Hptset.add (Base.of_varinfo vi) acc)
- varset Base.Hptset.empty
- in
- Base.SetLattice.(join (inject baseset) acc)
+ let variables = Variable.get_all varinfo in
+ List.fold_left add_related_bases acc variables
with Base.Not_a_C_variable | Not_found -> acc
in
- Base.Hptset.fold aux bases Base.SetLattice.empty
+ let hptset = Base.Hptset.fold aux bases Base.Hptset.empty in
+ Base.SetLattice.inject hptset
let filter _kind bases state =
if intraprocedural ()
then state
else
- let mem_vi varinfo = Base.Hptset.mem (Base.of_varinfo varinfo) bases in
+ let mem_var var = Base.Hptset.mem (Variable.base var) bases in
let mem_pair pair =
let x, y = Pair.get pair in
- mem_vi x && mem_vi y
+ mem_var x && mem_var y
in
let octagons = Octagons.filter mem_pair state.octagons in
- let intervals = Intervals.filter mem_vi state.intervals in
- let relations = Relations.filter mem_vi state.relations in
+ let intervals = Intervals.filter mem_var state.intervals in
+ let relations = Relations.filter mem_var state.relations in
{ state with octagons; intervals; relations; }
- let reuse =
+ let interprocedural_reuse =
let cache = Hptmap_sig.PersistentCache "Octagons.reuse"
and symmetric = false
and idempotent = true
@@ -1297,17 +1394,46 @@ module Domain = struct
let join_oct = Octagons.internal_join ~cache ~symmetric ~idempotent ~decide
and join_itv = Intervals.internal_join ~cache ~symmetric ~idempotent ~decide
and join_rel = Relations.union in
- fun _kf _bases ~current_input ~previous_output ->
- if intraprocedural ()
- then previous_output
+ fun kf ~current_input ~previous_output ->
+ let current_input = kill previous_output.modified current_input in
+ (* We use [add_diamond] to add each relation from the previous output
+ into the current input, in order to benefit from the (partial)
+ saturation of octagons performed by this function. For a maximum
+ precision, a complete saturation would be required.
+ Otherwise, we use instead a more efficient (but less precise) merge
+ of the maps from the previous output and the current input. *)
+ if saturate_octagons
+ then
+ let intervals =
+ join_itv previous_output.intervals current_input.intervals
+ in
+ let state = { current_input with intervals } in
+ let add_diamond variables diamond acc =
+ match add_diamond acc variables diamond with
+ | `Value state -> state
+ | `Bottom ->
+ Self.failure ~current:true ~once:true
+ "Octagon domain: the use of the memexec cache for function %a
+ unexpectedly led to bottom, which could be a bug. The analysis
+ continues by ignoring the relations leading to bottom."
+ Kernel_function.pretty kf;
+ acc
+ in
+ Octagons.fold add_diamond previous_output.octagons state
else
- let current_input = kill previous_output.modified current_input in
- let prev_output = previous_output in
- check "reuse result"
- { octagons = join_oct prev_output.octagons current_input.octagons;
- intervals = join_itv prev_output.intervals current_input.intervals;
- relations = join_rel prev_output.relations current_input.relations;
- modified = current_input.modified }
+ { octagons = join_oct previous_output.octagons current_input.octagons;
+ intervals = join_itv previous_output.intervals current_input.intervals;
+ relations = join_rel previous_output.relations current_input.relations;
+ modified = current_input.modified }
+
+ let reuse kf _bases ~current_input ~previous_output =
+ if intraprocedural ()
+ then previous_output
+ else
+ let t = interprocedural_reuse kf ~current_input ~previous_output in
+ check "reuse result" t
+
+
end
diff --git a/tests/value/octagons.c b/tests/value/octagons.c
index 101dafb7febcfda4bf4d2d67b16d71a76e55aa50..cbc98a770dce506d2b40a7381db9045d56d17f0f 100644
--- a/tests/value/octagons.c
+++ b/tests/value/octagons.c
@@ -223,6 +223,39 @@ void pub301 () {
}
}
+#define MAX 20
+
+void arrays () {
+ int a[MAX], t[MAX];
+ /*@ loop unroll MAX; */ // Unroll to ensure array initialization.
+ for (int i = 0; i < MAX; i++) {
+ a[i] = undet;
+ }
+
+ int x = Frama_C_interval(1, MAX);
+ for (int j = x - 1; j >= 0; j--) {
+ // Need the relation j <= x-1 to prove that index x-1-j >= 0.
+ t[j] = a[x - 1 - j];
+ }
+
+ int y = Frama_C_interval(0, MAX-1);
+ int index = (MAX-1) - y;
+ for (int j = y; j < MAX; j++) {
+ // Need the relation index + j == MAX-1 to prove index >= 0.
+ t[index] = a[j];
+ index --;
+ }
+
+ // Same with a floating-point variable f instead of x.
+ float f = Frama_C_float_interval(0., (float)(MAX-1));
+ index = (MAX-1) - (int)f;
+ for (int j = (int)f; j < MAX; j++) {
+ // Need the relation index + j == MAX-1 to prove index >= 0.
+ t[index] = a[j];
+ index --;
+ }
+}
+
void main () {
demo ();
integer_types ();
@@ -234,4 +267,5 @@ void main () {
interprocedural ();
dump ();
pub301 ();
+ arrays ();
}
diff --git a/tests/value/oracle/octagons.res.oracle b/tests/value/oracle/octagons.res.oracle
index c5865a36e4b056718034bb0d8e4f90972ed6f8ea..a75bd7ade602c5986c22760a15f86ff2cf5c189a 100644
--- a/tests/value/oracle/octagons.res.oracle
+++ b/tests/value/oracle/octagons.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
[eva] computing for function demo <- main.
- Called from octagons.c:227.
+ Called from octagons.c:260.
[eva] computing for function Frama_C_interval <- demo <- main.
Called from octagons.c:12.
[eva] using specification for function Frama_C_interval
@@ -19,7 +19,7 @@
[eva] Recording results for demo
[eva] Done for function demo
[eva] computing for function integer_types <- main.
- Called from octagons.c:228.
+ Called from octagons.c:261.
[eva] computing for function Frama_C_interval <- integer_types <- main.
Called from octagons.c:23.
[eva] octagons.c:23:
@@ -69,7 +69,7 @@
[eva] Recording results for integer_types
[eva] Done for function integer_types
[eva] computing for function arith <- main.
- Called from octagons.c:229.
+ Called from octagons.c:262.
[eva] computing for function Frama_C_interval <- arith <- main.
Called from octagons.c:70.
[eva] octagons.c:70:
@@ -107,7 +107,7 @@
[eva] Recording results for arith
[eva] Done for function arith
[eva] computing for function join <- main.
- Called from octagons.c:230.
+ Called from octagons.c:263.
[eva] computing for function Frama_C_interval <- join <- main.
Called from octagons.c:103.
[eva] octagons.c:103:
@@ -138,7 +138,7 @@
[eva] Recording results for join
[eva] Done for function join
[eva] computing for function loop <- main.
- Called from octagons.c:231.
+ Called from octagons.c:264.
[eva] computing for function Frama_C_interval <- loop <- main.
Called from octagons.c:128.
[eva] octagons.c:128:
@@ -164,7 +164,7 @@
[eva] Recording results for loop
[eva] Done for function loop
[eva] computing for function pointers <- main.
- Called from octagons.c:232.
+ Called from octagons.c:265.
[eva] computing for function Frama_C_interval <- pointers <- main.
Called from octagons.c:151.
[eva] octagons.c:151:
@@ -188,7 +188,7 @@
[eva] Recording results for pointers
[eva] Done for function pointers
[eva] computing for function saturate <- main.
- Called from octagons.c:233.
+ Called from octagons.c:266.
[eva] computing for function Frama_C_interval <- saturate <- main.
Called from octagons.c:169.
[eva] octagons.c:169:
@@ -203,7 +203,7 @@
[eva] Recording results for saturate
[eva] Done for function saturate
[eva] computing for function interprocedural <- main.
- Called from octagons.c:234.
+ Called from octagons.c:267.
[eva] computing for function Frama_C_interval <- interprocedural <- main.
Called from octagons.c:182.
[eva] octagons.c:182:
@@ -218,10 +218,7 @@
Called from octagons.c:184.
[eva] Recording results for neg
[eva] Done for function neg
-[eva] computing for function neg <- interprocedural <- main.
- Called from octagons.c:185.
-[eva] Recording results for neg
-[eva] Done for function neg
+[eva] octagons.c:185: Reusing old results for call to neg
[eva] computing for function diff <- interprocedural <- main.
Called from octagons.c:194.
[eva] Recording results for diff
@@ -234,7 +231,7 @@
[eva] Recording results for interprocedural
[eva] Done for function interprocedural
[eva] computing for function dump <- main.
- Called from octagons.c:235.
+ Called from octagons.c:268.
[eva] computing for function Frama_C_interval <- dump <- main.
Called from octagons.c:206.
[eva] octagons.c:206:
@@ -259,7 +256,7 @@
[eva] Recording results for dump
[eva] Done for function dump
[eva] computing for function pub301 <- main.
- Called from octagons.c:236.
+ Called from octagons.c:269.
[eva] computing for function Frama_C_interval <- pub301 <- main.
Called from octagons.c:216.
[eva] octagons.c:216:
@@ -272,6 +269,31 @@
[eva] Done for function Frama_C_interval
[eva] Recording results for pub301
[eva] Done for function pub301
+[eva] computing for function arrays <- main.
+ Called from octagons.c:270.
+[eva] computing for function Frama_C_interval <- arrays <- main.
+ Called from octagons.c:235.
+[eva] octagons.c:235:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] octagons.c:236: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- arrays <- main.
+ Called from octagons.c:241.
+[eva] octagons.c:241:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] octagons.c:243: starting to merge loop iterations
+[eva] computing for function Frama_C_float_interval <- arrays <- main.
+ Called from octagons.c:250.
+[eva] using specification for function Frama_C_float_interval
+[eva] octagons.c:250:
+ function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] octagons.c:250:
+ function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] octagons.c:252: starting to merge loop iterations
+[eva] Recording results for arrays
+[eva] Done for function arrays
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -283,6 +305,14 @@
x ∈ [-28..0]
y ∈ [1..29]
r ∈ [-29..106]
+[eva:final-states] Values at end of function arrays:
+ Frama_C_entropy_source ∈ [--..--]
+ a[0..19] ∈ [--..--]
+ t[0..19] ∈ [--..--] or UNINITIALIZED
+ x ∈ [1..20]
+ y ∈ [0..19]
+ index ∈ {-1}
+ f ∈ [-0. .. 19.]
[eva:final-states] Values at end of function demo:
Frama_C_entropy_source ∈ [--..--]
y ∈ [--..--]
@@ -364,6 +394,10 @@
[from] Computing for function Frama_C_interval <-arith
[from] Done for function Frama_C_interval
[from] Done for function arith
+[from] Computing for function arrays
+[from] Computing for function Frama_C_float_interval <-arrays
+[from] Done for function Frama_C_float_interval
+[from] Done for function arrays
[from] Computing for function demo
[from] Done for function demo
[from] Computing for function diff
@@ -390,11 +424,16 @@
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_float_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
[from] Function arith:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function arrays:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function demo:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function diff:
@@ -424,6 +463,10 @@
Frama_C_entropy_source; k; a; b; x; y; r
[inout] Inputs for function arith:
Frama_C_entropy_source
+[inout] Out (internal) for function arrays:
+ Frama_C_entropy_source; a[0..19]; t[0..19]; i; x; j; y; index; j_0; f; j_1
+[inout] Inputs for function arrays:
+ Frama_C_entropy_source; undet
[inout] Out (internal) for function demo:
Frama_C_entropy_source; y; k; x; r; t
[inout] Inputs for function demo:
diff --git a/tests/value/oracle_apron/octagons.res.oracle b/tests/value/oracle_apron/octagons.res.oracle
index 431455b54fd064e93b64e9536f2b4b3c53d9326f..7f9960cfff7ded799a7d74f6c577c21859b1d04c 100644
--- a/tests/value/oracle_apron/octagons.res.oracle
+++ b/tests/value/oracle_apron/octagons.res.oracle
@@ -1,4 +1,11 @@
-325,328c325,328
+221c221,224
+< [eva] octagons.c:185: Reusing old results for call to neg
+---
+> [eva] computing for function neg <- interprocedural <- main.
+> Called from octagons.c:185.
+> [eva] Recording results for neg
+> [eva] Done for function neg
+355,358c358,361
< a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647]
diff --git a/tests/value/oracle_equality/octagons.res.oracle b/tests/value/oracle_equality/octagons.res.oracle
index 1917faccaadbc5d43d3e549c0832dba3b8ad3ddb..ef865f5bada6bbb03ae3179c605488277f90829d 100644
--- a/tests/value/oracle_equality/octagons.res.oracle
+++ b/tests/value/oracle_equality/octagons.res.oracle
@@ -2,7 +2,14 @@
< [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-128..127], [-128..127]
---
> [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127]
-312c312
+221c221,224
+< [eva] octagons.c:185: Reusing old results for call to neg
+---
+> [eva] computing for function neg <- interprocedural <- main.
+> Called from octagons.c:185.
+> [eva] Recording results for neg
+> [eva] Done for function neg
+342c345
< ct ∈ [--..--] or UNINITIALIZED
---
> ct ∈ [6..127] or UNINITIALIZED
diff --git a/tests/value/oracle_gauges/octagons.res.oracle b/tests/value/oracle_gauges/octagons.res.oracle
index 37ac2f4f7980b9d318b6577cc9d68019f762f69c..4a7e1f1faba934bd6d5765e66ae10bd237423212 100644
--- a/tests/value/oracle_gauges/octagons.res.oracle
+++ b/tests/value/oracle_gauges/octagons.res.oracle
@@ -11,7 +11,7 @@
< [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
---
> [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1]
-325,328c317,320
+355,358c347,350
< a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647]
@@ -21,7 +21,7 @@
> b ∈ [-181..1867]
> c ∈ [-602..1446]
> d ∈ [-190..1874]
-330c322
+360c352
< d2 ∈ [-2147483648..1]
---
> d2 ∈ [-2468..1]