Skip to content
Snippets Groups Projects
Commit b8aa9be2 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Dive] Also compute integer intervals

parent c000871d
Branches
Tags
No related merge requests found
...@@ -47,7 +47,7 @@ let fkind_limits = ...@@ -47,7 +47,7 @@ let fkind_limits =
| FDouble -> double | FDouble -> double
| FLongDouble -> assert false | FLongDouble -> assert false
let precision_limits = let float_grade_limits =
let single = float_of_string "0x1p+120" let single = float_of_string "0x1p+120"
and double = float_of_string "0x1p+960" and double = float_of_string "0x1p+960"
and long_double = float_of_string "0x1p+15360" and long_double = float_of_string "0x1p+15360"
...@@ -56,39 +56,83 @@ let precision_limits = ...@@ -56,39 +56,83 @@ let precision_limits =
| FDouble -> double | FDouble -> double
| FLongDouble -> long_double | FLongDouble -> long_double
let is_large_range fkind (min,max) = let is_large_float_range fkind (min,max) =
let limit = precision_limits fkind in let limit = float_grade_limits fkind in
if (min < 0.0) = (max < 0.0) then (* if bounds have same sign *) if (min < 0.0) = (max < 0.0) then (* if bounds have same sign *)
max -. min >= limit max -. min >= limit
else else
min <= -.limit || max >= limit min <= -.limit || max >= limit
let qualify_range fkind (min,max) = let float_grade fkind (min,max) =
if min = max then if min = max then
Singleton Singleton
else if is_large_range fkind (min,max) then else if is_large_float_range fkind (min,max) then
Wide Wide
else else
Normal Normal
let ikind_limits ikind =
let open Cil in
let bits = bitsSizeOfInt ikind in
if isSigned ikind then
{ min=min_signed_number bits; max=max_signed_number bits }
else
{ min=Integer.zero; max=max_unsigned_number bits }
let int_grade_limits ikind =
let bits = Cil.bitsSizeOfInt ikind in
Integer.(pred (two_power_of_int (bits - bits / 8)))
let is_large_int_range ikind (l,u) =
let limit = int_grade_limits ikind in
if Integer.(lt l zero) = Integer.(lt u zero) then (* if bounds have same sign *)
Integer.(ge (sub u l) limit)
else
Integer.(le l (neg limit)) || Integer.(ge u limit)
let int_grade ikind (min,max) =
if min = max then
Singleton
else if is_large_int_range ikind (min,max) then
Wide
else
Normal
let update_node_values node kinstr lval = let update_node_values node kinstr lval =
let typ = Cil.typeOfLval lval in let typ = Cil.typeOfLval lval in
let state = Db.Value.get_state kinstr in let state = Db.Value.get_state kinstr in
let _,cvalue = !Db.Value.eval_lval None state lval in let _,cvalue = !Db.Value.eval_lval None state lval in
try match typ with try
let ival = Cvalue.V.project_ival cvalue in
match typ with
| TInt (ikind,_) ->
let size = Integer.of_int (Cil.bitsSizeOfInt ikind)
and signed = Cil.isSigned ikind in
let ival = Ival.reinterpret_as_int ~size ~signed ival in
let min, max = match Ival.min_and_max ival with
| Some min, Some max -> min, max
| _, _ -> assert false (* ival have been reinterpreted *)
in
Imprecision_graph.update_node_int_values node {
values_interval = {min;max};
values_limits = ikind_limits ikind;
values_grade = int_grade ikind (min,max)
}
| TFloat (fkind,_) -> | TFloat (fkind,_) ->
begin match Ival.min_and_max_float (Cvalue.V.project_ival cvalue) with begin match Ival.min_and_max_float ival with
| None, _can_be_nan -> () | None, _can_be_nan -> ()
| Some (min, max), _can_be_nan -> | Some (min, max), _can_be_nan ->
let min = Fval.F.to_float min and max = Fval.F.to_float max in let min = Fval.F.to_float min and max = Fval.F.to_float max in
Imprecision_graph.update_node_values node { Imprecision_graph.update_node_float_values node {
values_interval = {min;max}; values_interval = {min;max};
values_limits = fkind_limits fkind; values_limits = fkind_limits fkind;
values_grade = qualify_range fkind (min,max); values_grade = float_grade fkind (min,max);
} }
end end
| _ -> () | _ -> Self.result "node %a has type %a" Node_kind.pretty node.node_kind Cil_printer.pp_typ typ
with Cvalue.V.Not_based_on_null -> () with Cvalue.V.Not_based_on_null -> Self.result "node %a is not numeric" Node_kind.pretty node.node_kind
(* --- Locations handling --- *) (* --- Locations handling --- *)
......
...@@ -31,13 +31,13 @@ type node_locality = { ...@@ -31,13 +31,13 @@ type node_locality = {
loc_callstack : Callstack.t; loc_callstack : Callstack.t;
} }
type float_interval = {min: float; max: float} type 'a interval = {min: 'a; max: 'a}
type precision_grade = Singleton | Normal | Wide type precision_grade = Singleton | Normal | Wide
type node_values = { type 'a node_values = {
values_interval : float_interval; values_interval : 'a interval;
values_limits : float_interval; values_limits : 'a interval;
values_grade : precision_grade; values_grade : precision_grade;
} }
...@@ -46,7 +46,8 @@ type node = { ...@@ -46,7 +46,8 @@ type node = {
node_kind : node_kind; node_kind : node_kind;
node_locality : node_locality; node_locality : node_locality;
mutable node_hidden : bool; mutable node_hidden : bool;
mutable node_values : node_values option; mutable node_int_values : (Integer.t node_values) option;
mutable node_float_values : (float node_values) option;
mutable node_deps_computed : bool; mutable node_deps_computed : bool;
} }
......
...@@ -55,13 +55,14 @@ let edges g = ...@@ -55,13 +55,14 @@ let edges g =
let next_key = ref 0 let next_key = ref 0
let create_node ?node_values ~node_kind ~node_locality g = let create_node ~node_kind ~node_locality g =
let node = { let node = {
node_key = !next_key; node_key = !next_key;
node_kind; node_kind;
node_locality; node_locality;
node_hidden = false; node_hidden = false;
node_values; node_int_values = None;
node_float_values = None;
node_deps_computed = false; node_deps_computed = false;
} }
in in
...@@ -71,7 +72,10 @@ let create_node ?node_values ~node_kind ~node_locality g = ...@@ -71,7 +72,10 @@ let create_node ?node_values ~node_kind ~node_locality g =
let remove_node = remove_vertex let remove_node = remove_vertex
let union_interval i1 i2 = let union_int_interval i1 i2 =
{ min = Integer.min i1.min i2.min ; max = Integer.max i1.max i2.max }
let union_float_interval i1 i2 =
{ min = min i1.min i2.min ; max = max i1.max i2.max } { min = min i1.min i2.min ; max = max i1.max i2.max }
let worst_precision_grade q1 q2 = let worst_precision_grade q1 q2 =
...@@ -80,18 +84,32 @@ let worst_precision_grade q1 q2 = ...@@ -80,18 +84,32 @@ let worst_precision_grade q1 q2 =
| Normal, _ | _, Normal -> Normal | Normal, _ | _, Normal -> Normal
| Singleton, Singleton -> Singleton | Singleton, Singleton -> Singleton
let merge_precisions p1 p2 = let merge_int_values p1 p2 =
(* TODO: prevent assertion failure *)
assert (Integer.equal p1.values_limits.min p2.values_limits.min);
assert (Integer.equal p1.values_limits.max p2.values_limits.max);
{
values_interval = union_int_interval p1.values_interval p2.values_interval;
values_limits = p1.values_limits;
values_grade = worst_precision_grade p1.values_grade p2.values_grade;
}
let merge_float_values p1 p2 =
(* TODO: prevent assertion failure *) (* TODO: prevent assertion failure *)
assert (p1.values_limits = p2.values_limits); assert (p1.values_limits = p2.values_limits);
{ {
values_interval = union_interval p1.values_interval p2.values_interval; values_interval = union_float_interval p1.values_interval p2.values_interval;
values_limits = p1.values_limits; values_limits = p1.values_limits;
values_grade = worst_precision_grade p1.values_grade p2.values_grade; values_grade = worst_precision_grade p1.values_grade p2.values_grade;
} }
let update_node_values node new_values = let update_node_int_values node new_values =
node.node_values <- node.node_int_values <-
Some (Extlib.opt_fold merge_precisions node.node_values new_values) Some (Extlib.opt_fold merge_int_values node.node_int_values new_values)
let update_node_float_values node new_values =
node.node_float_values <-
Some (Extlib.opt_fold merge_float_values node.node_float_values new_values)
let create_dependency ~allow_folding g v1 dependency_kind v2 = let create_dependency ~allow_folding g v1 dependency_kind v2 =
...@@ -178,6 +196,13 @@ let ouptput_to_dot out_channel g = ...@@ -178,6 +196,13 @@ let ouptput_to_dot out_channel g =
let default_vertex_attributes _g = [] let default_vertex_attributes _g = []
let vertex_name v = "cp" ^ (string_of_int v.node_key) let vertex_name v = "cp" ^ (string_of_int v.node_key)
let vertex_attributes v = let vertex_attributes v =
let grade = match v.node_int_values, v.node_float_values with
| Some v1, Some v2 ->
Some (worst_precision_grade v1.values_grade v2.values_grade)
| Some v, _ -> Some v.values_grade
| _, Some v -> Some v.values_grade
| None, None -> None
in
let l = ref [] in let l = ref [] in
let text = Pretty_utils.to_string Node_kind.pretty v.node_kind in let text = Pretty_utils.to_string Node_kind.pretty v.node_kind in
if text <> "" then if text <> "" then
...@@ -189,13 +214,13 @@ let ouptput_to_dot out_channel g = ...@@ -189,13 +214,13 @@ let ouptput_to_dot out_channel g =
| Alarm _ -> [ `Shape `Doubleoctagon ; | Alarm _ -> [ `Shape `Doubleoctagon ;
`Style `Bold ; `Color 0xff0000 ; `Style `Bold ; `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xff0000 ] `Style `Filled ; `Fillcolor 0xff0000 ]
and values = match v.node_values with and values = match grade with
| None -> [] | None -> []
| Some ({values_grade=Singleton}) -> | Some Singleton ->
[`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff ] [`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff ]
| Some ({values_grade=Normal}) -> | Some Normal ->
[ `Color 0x004400 ; `Style `Filled ; `Fillcolor 0xeeffee ] [ `Color 0x004400 ; `Style `Filled ; `Fillcolor 0xeeffee ]
| Some ({values_grade=Wide}) -> | Some Wide ->
[ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ] [ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ]
in in
l := values @ kind @ !l; l := values @ kind @ !l;
...@@ -269,13 +294,27 @@ struct ...@@ -269,13 +294,27 @@ struct
in in
Json.of_string s Json.of_string s
let output_int_interval interval =
(* TODO: handle overflow *)
Json.of_fields [
("min", Json.of_int (Integer.to_int interval.min)) ;
("max", Json.of_int (Integer.to_int interval.max)) ;
]
let output_float_interval interval = let output_float_interval interval =
Json.of_fields [ Json.of_fields [
("min", Json.of_float interval.min) ; ("min", Json.of_float interval.min) ;
("max", Json.of_float interval.max) ; ("max", Json.of_float interval.max) ;
] ]
let output_node_values values = let output_node_int_values values =
Json.of_fields [
("computed", output_int_interval values.values_interval) ;
("limits", output_int_interval values.values_limits) ;
("grade", output_node_precision_grade values.values_grade) ;
]
let output_node_float_values values =
Json.of_fields [ Json.of_fields [
("computed", output_float_interval values.values_interval) ; ("computed", output_float_interval values.values_interval) ;
("limits", output_float_interval values.values_limits) ; ("limits", output_float_interval values.values_limits) ;
...@@ -291,11 +330,16 @@ struct ...@@ -291,11 +330,16 @@ struct
("locality", output_node_locality node.node_locality) ; ("locality", output_node_locality node.node_locality) ;
("explored", Json.of_bool node.node_deps_computed) ; ("explored", Json.of_bool node.node_deps_computed) ;
] @ ] @
begin match node.node_values with begin match node.node_int_values with
| None -> []
| Some node_values ->
[("int_values", output_node_int_values node_values)]
end @
begin match node.node_float_values with
| None -> [] | None -> []
| Some node_values -> [("values", output_node_values node_values)] | Some node_values ->
end [("float_values", output_node_float_values node_values)]
@ end @
begin match Node_kind.to_lval node.node_kind with begin match Node_kind.to_lval node.node_kind with
| None -> [] | None -> []
| Some lval -> | Some lval ->
......
...@@ -33,13 +33,13 @@ module Dependency : Graph.Sig.COMPARABLE with type t = dependency ...@@ -33,13 +33,13 @@ module Dependency : Graph.Sig.COMPARABLE with type t = dependency
val create : ?size:int -> unit -> t val create : ?size:int -> unit -> t
val create_node : val create_node :
?node_values:node_values ->
node_kind:node_kind -> node_kind:node_kind ->
node_locality:node_locality -> t -> node node_locality:node_locality -> t -> node
val remove_node : t -> node -> unit val remove_node : t -> node -> unit
val update_node_values : node -> node_values -> unit val update_node_int_values : node -> Integer.t node_values -> unit
val update_node_float_values : node -> float node_values -> unit
val create_dependency : allow_folding:bool -> t -> node -> dependency_kind -> val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
node -> unit node -> unit
......
...@@ -20,8 +20,6 @@ ...@@ -20,8 +20,6 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Graph_types
include Datatype.S with type t = Graph_types.node_kind include Datatype.S with type t = Graph_types.node_kind
val get_base : t -> Cil_types.varinfo option val get_base : t -> Cil_types.varinfo option
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment