From 916538a344351afa29c69457df4a596820888251 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 1 Jul 2020 21:06:26 +0200
Subject: [PATCH] [dive] simplify and generalize the computation of values &
range rating
---
headers/header_spec.txt | 8 +-
ivette/src/renderer/Dive.tsx | 51 +-------
ivette/src/renderer/dive_style.js | 45 ++-----
src/plugins/dive/Makefile.in | 2 +-
src/plugins/dive/build.ml | 98 +-------------
src/plugins/dive/dive_graph.ml | 121 ++++--------------
src/plugins/dive/dive_graph.mli | 3 +-
src/plugins/dive/dive_types.mli | 18 +--
src/plugins/dive/node_range.ml | 103 +++++++++++++++
src/plugins/dive/node_range.mli | 26 ++++
src/plugins/dive/server_interface.ml | 4 +-
src/plugins/dive/tests/dive/oracle/ranges.dot | 62 +++++++++
.../dive/tests/dive/oracle/ranges.res.oracle | 25 ++++
.../dive/tests/dive/oracle/various.dot | 3 +-
src/plugins/dive/tests/dive/ranges.i | 39 ++++++
15 files changed, 315 insertions(+), 293 deletions(-)
create mode 100644 src/plugins/dive/node_range.ml
create mode 100644 src/plugins/dive/node_range.mli
create mode 100644 src/plugins/dive/tests/dive/oracle/ranges.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/ranges.res.oracle
create mode 100644 src/plugins/dive/tests/dive/ranges.i
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7fdecae8316..86d3a36c6be 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -768,14 +768,16 @@ src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/dive_graph.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/dive_graph.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/dive_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/graph_types.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/imprecision_graph.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/imprecision_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_range.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_range.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/ivette/src/renderer/Dive.tsx b/ivette/src/renderer/Dive.tsx
index 1065838cea2..48b76da473c 100644
--- a/ivette/src/renderer/Dive.tsx
+++ b/ivette/src/renderer/Dive.tsx
@@ -1,5 +1,3 @@
-import { strict as assert } from 'assert';
-
import React, { useState, useEffect } from 'react';
import { renderToString } from 'react-dom/server';
import * as Dome from 'dome';
@@ -57,39 +55,6 @@ function callstackToString(callstack: callstack): string {
return callstack.map((cs) => `${cs.fun}:${cs.instr}`).join('/');
}
-function nodeToIntervalString(node: Cytoscape.NodeSingular): string
-{
- const data = node.data();
- let interval;
-
- if (data.float_values) {
- interval = data.float_values.computed;
- }
- else if (data.int_values) {
- interval = data.int_values.computed;
- }
-
- return `[${interval.min} ; ${interval.max}]`;
-}
-
-function range(interval: Interval, limit: Interval): number
-{
- const l = Math.max(Math.abs(limit.min), Math.abs(limit.max));
- const x = Math.max(Math.abs(interval.min), Math.abs(interval.max));
-
- if (x === Infinity) {
- return 100;
- }
-
- if (x <= Math.E) {
- return 1;
- }
-
- const r = Math.log(Math.log(x)) / Math.log(Math.log(l));
- assert(0.0 <= r && r <= 1.0);
- return Math.max(1, Math.min(100, Math.floor(r * 100)));
-}
-
export type mode = 'explore' | 'overview';
@@ -227,10 +192,10 @@ class Dive {
const tips = [];
- if (node.data().float_values || node.data().int_values) {
+ if (node.data().values) {
tips.push(tippy(container, {
...common,
- content: nodeToIntervalString(node),
+ content: node.data().values,
placement: 'top',
distance: 10,
arrow: true,
@@ -275,16 +240,8 @@ class Dive {
for (const node of data.nodes)
{
- if (node.float_values) {
- const { computed, limits } = node.float_values;
- node.float_range = range(computed, limits);
- node.grade = node.float_values.grade;
- }
- else if (node.int_values) {
- const { computed, limits } = node.int_values;
- node.int_range = range(computed, limits);
- node.grade = node.int_values.grade;
- }
+ if (typeof node.range === 'number')
+ node.stops = `0% ${node.range}% ${node.range}% 100%`;
const previous = this.cy.$id(node.id);
if (previous.nonempty()) {
diff --git a/ivette/src/renderer/dive_style.js b/ivette/src/renderer/dive_style.js
index 56a3d286fef..5cc034a89ec 100644
--- a/ivette/src/renderer/dive_style.js
+++ b/ivette/src/renderer/dive_style.js
@@ -74,49 +74,28 @@ export default [
}
},
{
- selector: 'node[float_range]',
+ selector: 'node[stops]',
style: {
+ 'border-color': '#8e6',
+ 'background-gradient-stop-colors': '#5d3 #5d3 #9f7 #9f7',
'background-width-relative-to': 'include-padding',
- backgroundFill: 'linear-gradient',
- backgroundGradientDirection: 'to-left',
- backgroundGradientStopPositions: (ele) => {
- let r = ele.data('float_range') / 2;
- return `0% 0% ${r}% ${100-r}% 100% 100%`;
- }
+ 'background-fill': 'linear-gradient',
+ 'background-gradient-direction': 'to-top',
+ 'background-gradient-stop-positions': 'data(stops)'
}
},
{
- selector: 'node[int_range]',
+ selector: 'node[range="singleton"]',
style: {
- 'background-width-relative-to': 'include-padding',
- backgroundFill: 'linear-gradient',
- backgroundGradientDirection: 'to-left',
- backgroundGradientStopPositions: (ele) => {
- let r = ele.data('int_range') / 2;
- return `0% ${r}% ${r}% ${100-r}% ${100-r}% 100%`;
- }
- }
- },
- {
- selector: 'node[grade="singleton"]',
- style: {
- 'background-gradient-stop-colors': '#acf #acf #acf #acf #acf #acf',
- 'background-color': '#acf',
- 'border-color': '#8af'
- }
- },
- {
- selector: 'node[grade="normal"]',
- style: {
- 'background-gradient-stop-colors': '#4c2 #4c2 #bea #bea #4c2 #4c2',
- 'border-color': '#898'
+ 'border-color': '#8af',
+ 'background-color': '#acf'
}
},
{
- selector: 'node[grade="wide"]',
+ selector: 'node[range="wide"]',
style: {
- 'background-gradient-stop-colors': '#e44 #e44 #faa #faa #e44 #e44',
- 'border-color': '#f88'
+ 'border-color': '#f88',
+ 'background-color': '#e44'
}
},
{
diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
index 564a285aa3c..3847f07858b 100644
--- a/src/plugins/dive/Makefile.in
+++ b/src/plugins/dive/Makefile.in
@@ -39,7 +39,7 @@ endif
PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_DIVE@
PLUGIN_NAME := Dive
-PLUGIN_CMO := self callstack node_kind dive_graph build main \
+PLUGIN_CMO := self callstack node_kind node_range dive_graph build main \
server_interface
PLUGIN_CMI := dive_types
PLUGIN_DEPENDENCIES:= Eva Studia Server
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index bd8b9d01028..80018f10e2d 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -42,107 +42,11 @@ let rec list_break n l =
(* --- Precision evaluation --- *)
-let _fval_contains_maximal_bounds fkind fval =
- let top = Fval.top_finite (Fval.kind fkind) in
- Fval.has_greater_min_bound top fval >= 0 ||
- Fval.has_smaller_max_bound top fval >= 0
-
-let fkind_limits =
- let max_single = float_of_string "0x1.fffffep+127"
- and max_double = float_of_string "0x1.fffffffffffffp+1023" in
- let single_limits = { min = -. max_single ; max = max_single }
- and double_limits = { min = -. max_double ; max = max_double } in
- function
- | FFloat -> single_limits
- | FDouble -> double_limits
- | FLongDouble -> assert false
-
-let float_grade_limits =
- let single = float_of_string "0x1p+120"
- and double = float_of_string "0x1p+960"
- and long_double = float_of_string "0x1p+15360"
- in function
- | FFloat -> single
- | FDouble -> double
- | FLongDouble -> long_double
-
-let is_large_float_range fkind (min,max) =
- let limit = float_grade_limits fkind in
- if (min < 0.0) = (max < 0.0) then (* if bounds have same sign *)
- max -. min >= limit
- else
- min <= -.limit || max >= limit
-
-let float_grade fkind (min,max) =
- if min = max then
- Singleton
- else if is_large_float_range fkind (min,max) then
- Wide
- else
- 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 typ = Cil.typeOfLval lval in
let state = Db.Value.get_state kinstr in
let _,cvalue = !Db.Value.eval_lval None state lval in
- 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
- Graph.update_node_int_values node {
- values_interval = {min;max};
- values_limits = ikind_limits ikind;
- values_grade = int_grade ikind (min,max)
- }
-
- | TFloat (fkind,_) ->
- begin match Ival.min_and_max_float ival with
- | None, _can_be_nan -> ()
- | Some (min, max), _can_be_nan ->
- let min = Fval.F.to_float min and max = Fval.F.to_float max in
- Graph.update_node_float_values node {
- values_interval = {min;max};
- values_limits = fkind_limits fkind;
- values_grade = float_grade fkind (min,max);
- }
- end
- | _ -> ()
- with Cvalue.V.Not_based_on_null -> ()
+ Graph.update_node_values node cvalue typ
(* --- Locations handling --- *)
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index 7b8b8162ad7..c8ecf5d5000 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/src/plugins/dive/dive_graph.ml
@@ -64,8 +64,8 @@ let create_node ~node_kind ~node_locality g =
node_kind;
node_locality;
node_hidden = false;
- node_int_values = None;
- node_float_values = None;
+ node_values = None;
+ node_range = Empty;
node_writes_computation = NotDone;
node_writes_stmts = [];
}
@@ -75,44 +75,11 @@ let create_node ~node_kind ~node_locality g =
let remove_node = remove_vertex
-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 }
-
-let worst_precision_grade q1 q2 =
- match q1, q2 with
- | Wide, _ | _, Wide -> Wide
- | Normal, _ | _, Normal -> Normal
- | Singleton, Singleton -> Singleton
-
-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 *)
- assert (p1.values_limits = p2.values_limits);
- {
- values_interval = union_float_interval p1.values_interval p2.values_interval;
- values_limits = p1.values_limits;
- values_grade = worst_precision_grade p1.values_grade p2.values_grade;
- }
-
-let update_node_int_values node new_values =
- node.node_int_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 update_node_values node new_values typ =
+ node.node_values <-
+ Some (Extlib.opt_fold Cvalue.V.join node.node_values new_values);
+ node.node_range <-
+ Node_range.(upper_bound node.node_range (evaluate new_values typ))
let create_dependency ~allow_folding g kinstr v1 dependency_kind v2 =
let same_kind (_,e,_) =
@@ -237,13 +204,6 @@ let ouptput_to_dot out_channel g =
let default_vertex_attributes _g = []
let vertex_name v = "cp" ^ (string_of_int v.node_key)
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 text = Pretty_utils.to_string Node_kind.pretty v.node_kind in
if text <> "" then
@@ -258,16 +218,16 @@ let ouptput_to_dot out_channel g =
`Style `Filled ; `Fillcolor 0xff0000 ]
| AbsoluteMemory | String _ -> [`Shape `Box3d]
| Error _ -> [`Color 0xff0000]
- and values = match grade with
- | None -> []
- | Some Singleton ->
+ and range = match v.node_range with
+ | Empty -> []
+ | Singleton ->
[`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff ]
- | Some Normal ->
+ | Normal _ ->
[ `Color 0x004400 ; `Style `Filled ; `Fillcolor 0xeeffee ]
- | Some Wide ->
+ | Wide ->
[ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ]
in
- l := values @ kind @ !l;
+ l := range @ kind @ !l;
if v.node_writes_computation <> Done then
l := [ `Style `Dotted ] @ !l;
!l
@@ -329,13 +289,12 @@ struct
in
`Assoc fields
- let output_node_precision_grade grade =
- let s = match grade with
- | Singleton -> "singleton"
- | Normal -> "normal"
- | Wide -> "wide"
- in
- `String s
+ let output_range range =
+ match range with
+ | Empty -> `String "empty"
+ | Singleton -> `String "singleton"
+ | Normal range_grade -> `Int range_grade
+ | Wide -> `String "wide"
let output_dep_kind kind =
let s = match kind with
@@ -347,32 +306,10 @@ struct
in
`String s
- let output_int_interval interval =
- (* TODO: handle overflow *)
- `Assoc [
- ("min", `Int (Integer.to_int interval.min)) ;
- ("max", `Int (Integer.to_int interval.max)) ;
- ]
-
- let output_float_interval interval =
- `Assoc [
- ("min", `Float interval.min) ;
- ("max", `Float interval.max) ;
- ]
-
- let output_node_int_values values =
- `Assoc [
- ("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 =
- `Assoc [
- ("computed", output_float_interval values.values_interval) ;
- ("limits", output_float_interval values.values_limits) ;
- ("grade", output_node_precision_grade values.values_grade) ;
- ]
+ let output_node_values values =
+ match values with
+ | None -> `Null
+ | Some cvalue -> `String (Pretty_utils.to_string Cvalue.V.pretty cvalue)
let output_node node =
let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
@@ -383,17 +320,9 @@ struct
("locality", output_node_locality node.node_locality) ;
("explored", `Bool (node.node_writes_computation = Done)) ;
("writes", `List (List.map output_stmt node.node_writes_stmts)) ;
+ ("values", output_node_values node.node_values) ;
+ ("range", output_range node.node_range) ;
] @
- 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 -> []
- | Some node_values ->
- [("float_values", output_node_float_values node_values)]
- end @
begin match Node_kind.to_lval node.node_kind with
| None -> []
| Some lval ->
diff --git a/src/plugins/dive/dive_graph.mli b/src/plugins/dive/dive_graph.mli
index 24b50766572..e093170794f 100644
--- a/src/plugins/dive/dive_graph.mli
+++ b/src/plugins/dive/dive_graph.mli
@@ -38,8 +38,7 @@ val create_node :
val remove_node : t -> node -> unit
-val update_node_int_values : node -> Integer.t node_values -> unit
-val update_node_float_values : node -> float node_values -> unit
+val update_node_values : node -> Cvalue.V.t -> Cil_types.typ -> unit
val create_dependency : allow_folding:bool -> t -> Cil_types.kinstr ->
node -> dependency_kind -> node -> unit
diff --git a/src/plugins/dive/dive_types.mli b/src/plugins/dive/dive_types.mli
index 1acada506a3..3fcfe0e87c9 100644
--- a/src/plugins/dive/dive_types.mli
+++ b/src/plugins/dive/dive_types.mli
@@ -35,25 +35,21 @@ type node_locality = {
loc_callstack : Callstack.t;
}
-type 'a interval = {min: 'a; max: 'a}
-
-type precision_grade = Singleton | Normal | Wide
+type node_range =
+ | Empty (* No values assigned to the node *)
+ | Singleton (* A unique value ever assigned *)
+ | Normal of int (* From 0 = almost singleton to 100 = almost all possible values *)
+ | Wide (* Too many values for the type to be reasonable *)
type 'a computation = NotDone | Partial of 'a | Done
-type 'a node_values = {
- values_interval : 'a interval;
- values_limits : 'a interval;
- values_grade : precision_grade;
-}
-
type node = {
node_key : int;
node_kind : node_kind;
node_locality : node_locality;
mutable node_hidden : bool;
- mutable node_int_values : (Integer.t node_values) option;
- mutable node_float_values : (float node_values) option;
+ mutable node_values : Cvalue.V.t option;
+ mutable node_range : node_range;
mutable node_writes_computation : (Cil_types.stmt list) computation;
mutable node_writes_stmts : Cil_types.stmt list;
}
diff --git a/src/plugins/dive/node_range.ml b/src/plugins/dive/node_range.ml
new file mode 100644
index 00000000000..f93d3b73ab6
--- /dev/null
+++ b/src/plugins/dive/node_range.ml
@@ -0,0 +1,103 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 Dive_types
+
+type t = node_range
+
+let fkind_limits =
+ let max_single = float_of_string "0x1.fffffep+127"
+ and max_double = float_of_string "0x1.fffffffffffffp+1023" in
+ function
+ | Cil_types.FFloat -> max_single
+ | FDouble | FLongDouble -> max_double
+
+let ikind_limits ikind =
+ let open Cil in
+ let bits = bitsSizeOfInt ikind in
+ if isSigned ikind then
+ (min_signed_number bits, max_signed_number bits)
+ else
+ (Integer.zero, max_unsigned_number bits)
+
+let logscale x limit =
+ Float.(to_int (min 100. (100. *. log (max x 1.) /. log limit)))
+
+let log2scale x limit =
+ assert (x > 0.);
+ assert (limit > 0.);
+ Float.(logscale (log x) (log limit))
+
+let interval_range l u limit =
+ let range =
+ if (l < 0.0) = (u < 0.0) then (* if bounds have same sign *)
+ u -. l
+ else
+ Float.(max (abs u) (abs l))
+ in
+ let s = log2scale range limit in
+ if s > 98 then Wide else Normal s
+
+let integer_range ikind l u =
+ let _, limit = ikind_limits ikind
+ and l = Integer.to_float l
+ and u = Integer.to_float u in
+ interval_range l u (Integer.to_float limit)
+
+let float_range fkind l u =
+ let limit = fkind_limits fkind
+ and l = Fval.F.to_float l
+ and u = Fval.F.to_float u in
+ interval_range l u limit
+
+let default_range n =
+ Normal (logscale (Integer.to_float n) 100.)
+
+let evaluate cvalue typ =
+ try
+ let size = Integer.of_int (Cil.bitsSizeOf typ) in
+ let cardinal = Cvalue.V.cardinal_estimate ~size cvalue in
+ match typ with
+ | _ when Integer.is_zero cardinal -> Empty
+ | _ when Integer.is_one cardinal -> Singleton
+ | TInt (ikind,_) ->
+ begin match Ival.min_and_max (Cvalue.V.project_ival cvalue) with
+ | Some l, Some u -> integer_range ikind l u
+ | _, _ | exception Cvalue.V.Not_based_on_null -> Wide
+ | exception Abstract_interp.Error_Bottom -> Empty
+ end
+ | TFloat (fkind,_) ->
+ begin match Ival.min_and_max_float (Cvalue.V.project_ival cvalue) with
+ | Some (l, u), _can_be_nan -> float_range fkind l u
+ | _, _ | exception Cvalue.V.Not_based_on_null -> Wide
+ | exception Abstract_interp.Error_Bottom -> Empty
+ end
+ | _ ->
+ default_range cardinal
+ with Cil.SizeOfError _ -> Empty
+
+let upper_bound r1 r2 =
+ match r1, r2 with
+ | Empty, r | r, Empty -> r
+ | Singleton, r | r, Singleton -> r
+ | Normal i1, Normal i2 -> Normal (max i1 i2)
+ | Wide, _ | _, Wide -> Wide
diff --git a/src/plugins/dive/node_range.mli b/src/plugins/dive/node_range.mli
new file mode 100644
index 00000000000..1f8f3f24b85
--- /dev/null
+++ b/src/plugins/dive/node_range.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type t = Dive_types.node_range
+
+val evaluate : Cvalue.V.t -> Cil_types.typ -> t
+val upper_bound : t -> t -> t
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 4fe0960a05a..847558a2db7 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -201,8 +201,8 @@ struct
"locality", NodeLocality.syntax;
"explored", Syntax.boolean;
"writes", Syntax.array Kernel_ast.Marker.syntax;
- "int_values", Syntax.any;
- "float_values", Syntax.any;
+ "values", Syntax.option Syntax.string;
+ "range", Syntax.union [ Syntax.string ; Syntax.int ];
"type", Syntax.option Syntax.string
]
diff --git a/src/plugins/dive/tests/dive/oracle/ranges.dot b/src/plugins/dive/tests/dive/oracle/ranges.dot
new file mode 100644
index 00000000000..93374387479
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/ranges.dot
@@ -0,0 +1,62 @@
+digraph G {
+ cp1 [label=<res>, shape=box, ];
+ cp2 [label=<i>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp4 [label=<f>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp6 [label=<i0>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp8 [label=<i1>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp10 [label=<i2>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp12 [label=<i3>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp14 [label=<i4>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp16 [label=<i5>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp18 [label=<i6>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp20 [label=<i7>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp22 [label=<f0>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp24 [label=<f1>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp26 [label=<f2>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp28 [label=<f3>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp30 [label=<f4>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp32 [label=<f5>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp34 [label=<f6>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled", ];
+ cp36 [label=<f7>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp36;cp34;cp32;cp30;cp28;cp26;cp24;cp22;cp20;cp18;cp16;cp14;cp12;cp10;cp8;cp6;cp4;cp2;cp1;
+ };
+
+ cp2 -> cp1;
+ cp4 -> cp1;
+ cp6 -> cp2;
+ cp8 -> cp2;
+ cp10 -> cp2;
+ cp12 -> cp2;
+ cp14 -> cp2;
+ cp16 -> cp2;
+ cp18 -> cp2;
+ cp20 -> cp2;
+ cp22 -> cp4;
+ cp24 -> cp4;
+ cp26 -> cp4;
+ cp28 -> cp4;
+ cp30 -> cp4;
+ cp32 -> cp4;
+ cp34 -> cp4;
+ cp36 -> cp4;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/ranges.res.oracle b/src/plugins/dive/tests/dive/oracle/ranges.res.oracle
new file mode 100644
index 00000000000..8e49661f1ec
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/ranges.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/dive/ranges.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] using specification for function Frama_C_interval
+[eva:alarm] tests/dive/ranges.i:25: Warning:
+ signed overflow.
+ assert
+ (int)((int)((int)((int)((int)((int)(i0 + i1) + i2) + i3) + i4) + i5) + i6) +
+ i7 ≤ 2147483647;
+[eva] using specification for function Frama_C_float_interval
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 20 statements reached (out of 20): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/ranges.dot
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index 019cbcbc7c7..10fcc013eb8 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -18,7 +18,8 @@ digraph G {
style="filled", ];
cp19 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp22 [label=<pf>, shape=box, ];
+ cp22 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
cp24 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp27 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/ranges.i b/src/plugins/dive/tests/dive/ranges.i
new file mode 100644
index 00000000000..221deca7bc7
--- /dev/null
+++ b/src/plugins/dive/tests/dive/ranges.i
@@ -0,0 +1,39 @@
+/* run.config
+STDOPT: +"-dive-from-variables main::res -dive-depth-limit 4 -kernel-warn-key parser:decimal-float=inactive"
+*/
+
+/*@ assigns \result \from min, max;
+ ensures result_bounded: min <= \result <= max ;
+ */
+extern int Frama_C_interval(int min, int max);
+
+/*@ assigns \result \from min, max;
+ ensures result_bounded: \is_finite(\result) && min <= \result <= max;
+ */
+extern float Frama_C_float_interval(float min, float max);
+
+float main()
+{
+ int i0 = 2;
+ int i1 = Frama_C_interval(0, 3);
+ int i2 = Frama_C_interval(0, 12);
+ int i3 = Frama_C_interval(0, 127);
+ int i4 = Frama_C_interval(0, 42000);
+ int i5 = Frama_C_interval(0, 1350000);
+ int i6 = Frama_C_interval(0, 910000000);
+ int i7 = Frama_C_interval(0, 2000000000);
+ int i = i0 + i1 + i2 + i3 + i4 + i5 + i6 + i7;
+
+ float f0 = 0.;
+ float f1 = Frama_C_float_interval(0.f, 0.001f);
+ float f2 = Frama_C_float_interval(0.f, 3.14f);
+ float f3 = Frama_C_float_interval(0.f, 1020.f);
+ float f4 = Frama_C_float_interval(0.f, 1e7f);
+ float f5 = Frama_C_float_interval(0.f, 1e20f);
+ float f6 = Frama_C_float_interval(0.f, 1e36f);
+ float f7 = Frama_C_float_interval(0.f, 1e37f);
+ float f = f0 + f1 + f2 + f3 + f4 + f5 + f6 + f7;
+
+ float res = i + f;
+ return res;
+}
--
GitLab