diff --git a/Makefile b/Makefile
index 8bd4ad0cf6397d041cdf7844e9b2450d3b6c0c64..39fc7bd28c567bdb24c40a7030f6ec25174bbfa9 100644
--- a/Makefile
+++ b/Makefile
@@ -829,7 +829,7 @@ PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
- values/numerors domains/numerors
+ api values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
@@ -912,6 +912,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
engine/compute_functions engine/analysis register \
api/general_requests \
utils/unit_tests \
+ api/values_request \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 5d791ad40ee2ce6301155c602be4b5fb34761a11..a412c54e05be8e26a83069fbe6381e14e0c6e32d 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1210,6 +1210,8 @@ src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/api/values_request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/libraries/utils/utf8_logic.ml b/src/libraries/utils/utf8_logic.ml
index 1c2f3a6ddf068d4d24cec065a1d52cbad7f28301..92f594e89998bdcfad518673c529275de25a26e6 100644
--- a/src/libraries/utils/utf8_logic.ml
+++ b/src/libraries/utils/utf8_logic.ml
@@ -78,6 +78,9 @@ let integer = from_unichar 0x2124
let real = from_unichar 0x211D
let pi = from_unichar 0x3C0
+
+let infinity = from_unichar 0x221E
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/libraries/utils/utf8_logic.mli b/src/libraries/utils/utf8_logic.mli
index 449e20476bd3f55a53b09dd0cf143395d1ce5fad..7b6ea13a0da7362607108c23d890ca96d5f34184 100644
--- a/src/libraries/utils/utf8_logic.mli
+++ b/src/libraries/utils/utf8_logic.mli
@@ -49,6 +49,7 @@ val boolean: string
val integer: string
val real: string
val pi: string
+val infinity: string
(*
Local Variables:
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
new file mode 100644
index 0000000000000000000000000000000000000000..06c12aa5b1f4cf44e42cee1e5f180089069e2cbd
--- /dev/null
+++ b/src/plugins/value/api/values_request.ml
@@ -0,0 +1,342 @@
+(**************************************************************************)
+(* *)
+(* 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 Server
+open Data
+open Cil_types
+module Md = Markdown
+
+let chapter = `Plugin "Eva"
+
+let page = Doc.page chapter ~title:"Eva Values" ~filename:"eva.md"
+
+type value =
+ { value: string;
+ alarm: bool; }
+
+type evaluation =
+ | Unreachable
+ | Evaluation of value
+
+type after =
+ | Unchanged
+ | Reduced of evaluation
+
+type before_after =
+ { before: evaluation;
+ after_instr: after option;
+ after_then: after option;
+ after_else: after option; }
+
+type values =
+ { values: before_after;
+ callstack: (Value_util.callstack * before_after) list option; }
+
+let get_value = function
+ | Unreachable -> "Unreachable"
+ | Evaluation { value } -> value
+
+let get_alarm = function
+ | Unreachable -> false
+ | Evaluation { alarm } -> alarm
+
+let get_after_value =
+ Extlib.opt_map
+ (function Unchanged -> "unchanged" | Reduced eval -> get_value eval)
+
+module CallStackId =
+ Data.Index (Value_types.Callstack.Map)
+ (struct
+ let page = page
+ let name = "eva-callstack-id"
+ let descr = Md.plain "CallStack"
+ end)
+
+(* This pretty-printer drops the toplevel kf, which is always the function
+ in which we are pretty-printing the expression/term *)
+let pretty_callstack fmt cs =
+ match cs with
+ | [_, Kglobal] -> ()
+ | (_kf_cur, Kstmt callsite) :: q -> begin
+ let rec aux callsite = function
+ | (kf, callsite') :: q -> begin
+ Format.fprintf fmt "%a (%a)"
+ Kernel_function.pretty kf
+ Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc callsite);
+ match callsite' with
+ | Kglobal -> ()
+ | Kstmt callsite' ->
+ Format.fprintf fmt " â†@ ";
+ aux callsite' q
+ end
+ | _ -> assert false
+ in
+ Format.fprintf fmt "@[<hv>%a" Value_types.Callstack.pretty_hash cs;
+ aux callsite q;
+ Format.fprintf fmt "@]"
+ end
+ | _ -> assert false
+
+(* This pretty-printer prints only the lists of the functions, not
+ the locations. *)
+let pretty_callstack_short fmt cs =
+ match cs with
+ | [_, Kglobal] -> ()
+ | (_kf_cur, Kstmt _callsite) :: q ->
+ Format.fprintf fmt "%a" Value_types.Callstack.pretty_hash cs;
+ Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
+ (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt q
+ | _ -> assert false
+
+module CallStack = struct
+ type record
+
+ let record: record Record.signature =
+ Record.signature ~page
+ ~name:"eva-callstack" ~descr:(Md.plain "CallStack") ()
+
+ let id = Record.field record ~name:"id"
+ ~descr:(Md.plain "Callstack id") (module Jint)
+ let short = Record.field record ~name:"short"
+ ~descr:(Md.plain "Short name for the callstack") (module Jstring)
+ let full = Record.field record ~name:"full"
+ ~descr:(Md.plain "Full name for the callstack") (module Jstring)
+
+ module R = (val (Record.publish record) : Record.S with type r = record)
+
+ type t = Value_types.callstack option
+ let syntax = R.syntax
+
+ let pp_callstack ~short = function
+ | None -> "all"
+ | Some callstack ->
+ let pp_text =
+ if short
+ then Pretty_utils.to_string ~margin:50 pretty_callstack_short
+ else Pretty_utils.to_string pretty_callstack
+ in
+ (pp_text callstack)
+
+ let id_callstack = function
+ | None -> -1
+ | Some callstack -> CallStackId.get callstack
+
+ let to_json callstack =
+ R.default |>
+ R.set id (id_callstack callstack) |>
+ R.set short (pp_callstack ~short:true callstack) |>
+ R.set full (pp_callstack ~short:false callstack) |>
+ R.to_json
+
+ let key = function
+ | None -> "all"
+ | Some callstack -> string_of_int (CallStackId.get callstack)
+end
+
+
+let consolidated = ref None
+let table = Hashtbl.create 100
+
+let iter f =
+ Hashtbl.iter (fun key data -> f (Some key, data)) table;
+ Extlib.may (fun values -> f (None, values)) !consolidated
+
+let array =
+ let model = States.model () in
+ let () =
+ States.column ~model
+ ~name:"callstack" ~descr:(Md.plain "CallStack")
+ ~data:(module CallStack) ~get:fst ()
+ in
+ let () =
+ States.column ~model
+ ~name:"value_before"
+ ~descr:(Md.plain "Value inferred just before the selected point")
+ ~data:(module Jstring)
+ ~get:(fun (_, e) -> get_value e.before)
+ ()
+ in
+ let () =
+ States.column ~model
+ ~name:"alarm"
+ ~descr:(Md.plain "Did the evaluation led to an alarm?")
+ ~data:(module Jbool)
+ ~get:(fun (_, e) -> get_alarm e.before)
+ ()
+ in
+ let () =
+ States.column ~model
+ ~name:"value_after"
+ ~descr:(Md.plain "Value inferred just after the selected point")
+ ~data:(module Jstring.Joption)
+ ~get:(fun (_, e) -> get_after_value e.after_instr)
+ ()
+ in
+ States.register_array
+ ~page
+ ~name:"eva.values"
+ ~descr:(Md.plain "Abstract values inferred by the Eva analysis")
+ ~key:(fun (cs, _) -> CallStack.key cs)
+ ~iter
+ model
+
+let update_values values =
+ Hashtbl.clear table;
+ consolidated := Some values.values;
+ let () =
+ match values.callstack with
+ | None -> ()
+ | Some by_callstack ->
+ List.iter
+ (fun (callstack, before_after) ->
+ Hashtbl.add table callstack before_after)
+ by_callstack
+ in
+ States.reload array
+
+module type S = sig
+ val evaluate: kinstr -> exp -> values
+ val lvaluate: kinstr -> lval -> values
+end
+
+module Make (Eva: Analysis.S) : S = struct
+
+ let eval f state elt =
+ let value, alarms = f state elt in
+ let alarm = not (Alarmset.is_empty alarms) in
+ let str = Format.asprintf "%a" (Bottom.pretty Eva.Val.pretty) value in
+ { value = str; alarm }
+
+ let make_before f before elt =
+ let before =
+ match before with
+ | `Bottom -> Unreachable
+ | `Value state -> Evaluation (eval f state elt)
+ in
+ { before; after_instr = None; after_then = None; after_else = None; }
+
+ let make_callstack stmt f elt =
+ let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
+ match before with
+ | (`Bottom | `Top) -> []
+ | `Value before ->
+ let aux callstack before acc =
+ let before_after = make_before f (`Value before) elt in
+ (callstack, before_after) :: acc
+ in
+ Value_types.Callstack.Hashtbl.fold aux before []
+
+ let make_before_after f ~before ~after elt =
+ match before with
+ | `Bottom ->
+ { before = Unreachable;
+ after_instr = None;
+ after_then = None;
+ after_else = None; }
+ | `Value before ->
+ let before = eval f before elt in
+ let after_instr =
+ match after with
+ | `Bottom -> Some (Reduced Unreachable)
+ | `Value after ->
+ let after = eval f after elt in
+ if String.equal before.value after.value
+ then Some Unchanged
+ else Some (Reduced (Evaluation after))
+ in
+ { before = Evaluation before;
+ after_instr; after_then = None; after_else = None; }
+
+ let make_instr_callstack stmt f elt =
+ let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
+ let after = Eva.get_stmt_state_by_callstack ~after:true stmt in
+ match before, after with
+ | (`Bottom | `Top), _
+ | _, (`Bottom | `Top) -> []
+ | `Value before, `Value after ->
+ let aux callstack before acc =
+ let before = `Value before in
+ let after =
+ try `Value (Value_types.Callstack.Hashtbl.find after callstack)
+ with Not_found -> `Bottom
+ in
+ let before_after = make_before_after f ~before ~after elt in
+ (callstack, before_after) :: acc
+ in
+ Value_types.Callstack.Hashtbl.fold aux before []
+
+ let make f elt kinstr =
+ let before = Eva.get_kinstr_state ~after:false kinstr in
+ let values, callstack =
+ match kinstr with
+ | Cil_types.Kglobal ->
+ make_before f before elt, None
+ | Cil_types.Kstmt stmt ->
+ match stmt.skind with
+ | Instr _ ->
+ let after = Eva.get_kinstr_state ~after:true kinstr in
+ let values = make_before_after f ~before ~after elt in
+ let callstack = make_instr_callstack stmt f elt in
+ values, Some callstack
+ | _ ->
+ make_before f before elt,
+ Some (make_callstack stmt f elt)
+ in
+ { values; callstack; }
+
+
+ let evaluate kinstr expr =
+ make (Eva.eval_expr) expr kinstr
+
+ let lvaluate kinstr lval =
+ let loc = Cil_datatype.Location.unknown in
+ let expr = Cil.new_exp ~loc (Lval lval) in
+ make (Eva.eval_expr) expr kinstr
+end
+
+
+let ref_request =
+ let module Analyzer = (val Analysis.current_analyzer ()) in
+ ref (module Make (Analyzer) : S)
+
+let hook (module Analyzer: Analysis.S) =
+ ref_request := (module Make (Analyzer) : S)
+
+let () = Analysis.register_hook hook
+
+
+let update tag =
+ let module Request = (val !ref_request) in
+ match tag with
+ | Printer_tag.PExp (_kf, kinstr, expr) ->
+ update_values (Request.evaluate kinstr expr)
+ | Printer_tag.PLval (_kf, kinstr, lval) ->
+ update_values (Request.lvaluate kinstr lval)
+ | PVDecl (_kf, kinstr, varinfo) ->
+ update_values (Request.lvaluate kinstr (Var varinfo, NoOffset))
+ | _ -> ()
+
+let () = Server.Request.register ~page
+ ~kind:`GET ~name:"eva.values.compute"
+ ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue")
+ ~input:(module Kernel_ast.Marker) ~output:(module Junit)
+ update
diff --git a/src/plugins/value/api/values_request.mli b/src/plugins/value/api/values_request.mli
new file mode 100644
index 0000000000000000000000000000000000000000..182bc40a8e1af00f6d1329952d449d0f2e6808e1
--- /dev/null
+++ b/src/plugins/value/api/values_request.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)