diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index 2fc410f59d4a1a98fa508ce5dcf8d8428655a427..b6ef39a67856b8c00985e4a92dc62e4be686179c 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -39,3 +39,4 @@ aef808e15e4dcc02dcee7004add8530083d33474
6ead6d862f1960e6baca64d335b811c954cf8430
7955ef2039b2010cc30b88da7a47d4f07e298042
8353ff71c9958169cf27c589b678f183cca63a9c
+fe98b40c209dbe13fdc2069e26c42d4062fda3f0
diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 5c93176a091e3436ccc53e46bbbc52090370f534..4819e832e67595fea0a995ab42cb2698672d8345 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+25.0 (Manganese) 2022, June 22
24.0 (Chromium) 2021, November 30
23.1 (Vanadium) 2021, July 20
23.0 (Vanadium) 2021, July 7
diff --git a/Changelog b/Changelog
index 8fa0ae1eca938d72e434382f575730467f3d4786..dc984a5c05ecad75c391614d7f387263f3c0d859 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,7 @@
Open Source Release <next-release>
##################################
+o! Pdg [2022-07-01] Removed from Db. Use proper Pdg API instead.
-! Kernel [2022-06-06] Remove journalisation.
####################################
diff --git a/VERSION b/VERSION
index 5d9f0c7da19e7181f37905b778d6a953b6fc31e1..be8e64f5a38cfeb3e1c58884871821fdedcf09c7 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-25.0~beta
+25.0
diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile
index c6cae592a0f241287c37ea2fba3a5c897463c8ff..46b12aad0c9522ed5fee002bed6c31c825088f55 100644
--- a/devel_tools/docker/Makefile
+++ b/devel_tools/docker/Makefile
@@ -137,6 +137,61 @@ sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTES
sed 's|@OCAMLV@|4.08|g' | \
cat > $@
+25.0-stripped: Dockerfile.25.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-25.0-Manganese.tar.gz $(ARGS)
+TARGETS += 25.0-stripped
+
+25.0: Dockerfile.25.0
+ docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-25.0-Manganese.tar.gz $(ARGS)
+TARGETS += 25.0
+
+25.0-gui: Dockerfile.25.0
+ docker build . -t framac/frama-c-gui:25.0 --target frama-c-gui-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-25.0-Manganese.tar.gz $(ARGS)
+TARGETS += 25.0-gui
+
+push-25.0: 25.0 25.0-gui 25.0-stripped
+ docker push framac/frama-c:25.0
+ docker push framac/frama-c-gui:25.0
+ docker push framac/frama-c:25.0-stripped
+
+Dockerfile.25.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.2.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.1 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.6.1 \\\
+ppx_import.1.9.0 \\\
+why3.1.5.0 \\\
+yojson.1.7.0 \\\
+zarith.1.10 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g' | \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTESTS_OPTS=-error-code|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
24.0-stripped: Dockerfile.24.0
docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
--build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
diff --git a/doc/Makefile b/doc/Makefile
index 2f13b8379cbd1a5f1c476fc8be36fff95627e5e5..929dc0b7326ee3dbce28aea9f87a5e570ac21d15 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -145,7 +145,7 @@ ACSL_SUFFIX=-$(ACSL_VERSION)
endif
clean::
- $(MAKE) -C acsl clean
+ $(MAKE) -C acsl super-clean
all: \
manuals/acsl-implementation$(FC_SUFFIX).pdf \
@@ -164,7 +164,7 @@ EACSL_VERSION=$(shell grep 'newcommand{\\eacsllangversion' $(EACSL_DOC)/refman/m
ifeq ($(EACSL_VERSION),)
-$(info could not retrieve E-ACSL version from ../src/plugins/e-acsl/doc/refman/main.tex")
+$(info "could not retrieve E-ACSL version from ../src/plugins/e-acsl/doc/refman/main.tex")
else
@@ -178,8 +178,8 @@ ifneq ($(ACSL_VERSION),$(EACSL_VERSION))
endif
clean::
- $(MAKE) -C $(EACSL_DOC)/refman/ clean
- $(MAKE) -C $(EACSL_DOC)/userman/ clean
+ $(MAKE) -C $(EACSL_DOC)/refman/ super-clean
+ $(MAKE) -C $(EACSL_DOC)/userman/ super-clean
all: \
manuals/e-acsl-implementation$(FC_SUFFIX).pdf \
diff --git a/ivette/src/dome/renderer/layout/style.css b/ivette/src/dome/renderer/layout/style.css
index a2e0fca13db2095fde266199646103b6c8264367..41dfbcc3254a14b6e4c9ff107da9d50735193f12 100644
--- a/ivette/src/dome/renderer/layout/style.css
+++ b/ivette/src/dome/renderer/layout/style.css
@@ -103,7 +103,6 @@
.dome-xSplitter-block {
display: block;
- overflow: hidden;
position: relative;
width: 100%;
height: 100%;
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..dab3218c24ad0398e44e8b525e703ed1508fcf7b
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
@@ -0,0 +1,129 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2022 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+// React & Dome
+import React from 'react';
+import * as Ivette from 'ivette';
+import * as States from 'frama-c/states';
+import { GlobalState, useGlobalState } from 'dome/data/states';
+import * as Eva from 'frama-c/plugins/eva/api/general';
+import * as Boxes from 'dome/layout/boxes';
+import { HSplit } from 'dome/layout/splitters';
+import { Text } from 'frama-c/richtext';
+import { Checkbox, Select } from 'dome/controls/buttons';
+import { Label } from 'dome/controls/labels';
+
+const globalSelectedDomain = new GlobalState("");
+const globalFilter = new GlobalState(true);
+
+export function EvaStates(): JSX.Element {
+ const [selection] = States.useSelection();
+ const selectedLoc = selection?.current;
+ const marker = selectedLoc?.marker;
+ const [domains, setDomains] = React.useState<string[]>([]);
+ const [selected, setSelected] = useGlobalState(globalSelectedDomain);
+ const [stateBefore, setStateBefore] = React.useState("");
+ const [stateAfter, setStateAfter] = React.useState("");
+ const [filter, setFilter] = useGlobalState(globalFilter);
+
+ const requestArg = marker ? [marker, filter] : undefined;
+ const states = States.useRequest(Eva.getStates, requestArg);
+
+ React.useEffect(() => {
+ if (states && states.length > 0) {
+ const names = states.map((d) => d[0]);
+ setDomains(names);
+ if (!names.includes(selected))
+ setSelected(names[0]);
+ const selectedDomain = states.find((d) => d[0] === selected);
+ if (selectedDomain) {
+ setStateBefore(selectedDomain[1]);
+ setStateAfter(selectedDomain[2]);
+ }
+ } else
+ setDomains([]);
+ }, [states, selected, setSelected]);
+
+ if (domains.length === 0)
+ return (<></>);
+
+ function makeOption(name: string): React.ReactNode {
+ return <option value={name}>{name}</option>;
+ }
+ const list = React.Children.toArray(domains.map(makeOption));
+
+ return (
+ <>
+ <Boxes.Hbox className="domain-state-box">
+ <Label>Domain: </Label>
+ <Select
+ title="Select the analysis domain to be shown"
+ value={selected}
+ onChange={(domain) => setSelected(domain ?? "")}
+ >
+ {list}
+ </Select>
+ <Boxes.Filler/>
+ <Checkbox
+ label="Filtered state"
+ title="If enabled, only the part of the states relevant to the
+ selected marker are shown, for domains supporting this feature.
+ For other domains or if disabled, entire domain states are printed.
+ Beware that entire domain states can be very large."
+ value={filter}
+ onChange={setFilter}
+ />
+ </Boxes.Hbox>
+ <Boxes.Scroll>
+ <HSplit
+ settings="ivette.eva.domainStates.beforeAfterSplit"
+ >
+ <div className="domain-state-box">
+ State before the selected statement:
+ <Text className="domain-state" text={stateBefore} />
+ </div>
+ <div className="domain-state-box">
+ State after the selected statement:
+ <Text className="domain-state" text={stateAfter} />
+ </div>
+ </HSplit>
+ </Boxes.Scroll>
+ </>);
+}
+
+function EvaStatesComponent(): JSX.Element {
+ return (
+ <>
+ <Ivette.TitleBar />
+ <EvaStates />
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.domain_states',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'Eva States',
+ title: 'States of the Eva analysis',
+ children: <EvaStatesComponent />,
+});
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 55d8b6b7768e3e1717a91f126b192ce459c819bd..3ed2ea6b595d436fd82035130a5f13647d828103 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -580,4 +580,30 @@ export const functionStats: State.Array<
functionStatsData
> = functionStats_internal;
+const getStates_internal: Server.GetRequest<
+ [ marker, boolean ],
+ [ string, string, string ][]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getStates',
+ input: Json.jTry(
+ Json.jPair(
+ jMarkerSafe,
+ Json.jFail(Json.jBoolean,'Boolean expected'),
+ )),
+ output: Json.jList(
+ Json.jTry(
+ Json.jTriple(
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jString,'String expected'),
+ ))),
+ signals: [],
+};
+/** Get the domain states about the given marker */
+export const getStates: Server.GetRequest<
+ [ marker, boolean ],
+ [ string, string, string ][]
+ >= getStates_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 8aeb22bb817b5b6b873944d8b6f18ab43d2c4dff..36b6dc1d5ba54d5aede3104b1b40d767a38c784d 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -28,6 +28,7 @@ import * as Ivette from 'ivette';
import { } from 'frama-c/plugins/eva/valuetable';
import { } from './Summary';
import { } from './Coverage';
+import { } from './DomainStates';
import './style.css';
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index e4a17e65e23a5e3baf3af13f49d6f319b4c86f35..2d6367d5845267d7a8f76eaca15084b32936e1e0 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -317,3 +317,20 @@ tr:first-of-type > .eva-table-callsite-box {
}
/* -------------------------------------------------------------------------- */
+/* --- Domains state print --- */
+/* -------------------------------------------------------------------------- */
+
+.domain-state-box {
+ margin: 6px;
+}
+
+.domain-state {
+ cursor: auto;
+ user-select: text;
+ overflow: auto;
+ padding: 6px;
+ margin-top: 6px;
+ background-color: var(--background-report);
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/nix/default.nix b/nix/default.nix
index b7f5fcf6a9937e35271a2ed38e5dc2f8b0f3ddfb..4e146ccd47d633f8737f0183882061de862ed84a 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -14,6 +14,7 @@ let mydir = builtins.getEnv("PWD");
"why3=1.5.0" "why3-coq=1.5.0"
"menhir=20211012" "dune=2.9.1"
"easy-format=1.3.2"
+ "biniou=1.2.1"
];
# only pure nix packages. See mk_deriv below for adding opam2nix packages
mk_buildInputs = { nixPackages ? [] } :
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index d330023067eb7aa336fad8020cabdb397368f45c..1a19ba3926ebeb591bac02fb259657b22c9332d1 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -476,6 +476,8 @@ module Zone = struct
Base.SetLattice.mem b top_param
| Map m -> M.mem b m
+ let get_bases = get_keys
+
let shape x = x
let fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty =
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index c76b6002c1146de8e6b267ec72d5d70cecea31a9..632cbb17a31e507e2c1a80c3d9d524197fde6615 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -265,6 +265,10 @@ module Zone : sig
@since Carbon-20101201 *)
+ val get_bases : t -> Base.SetLattice.t
+ (** Returns the bases contained by the given zone. Never fails, but
+ may return [Base.SetLattice.Top]. *)
+
val intersects : t -> t -> bool
(** Assuming that [z1] and [z2] only contain valid bases,
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d3588a38f5d14a51e136166dc95a9a2d4aff15c3..9f06014cbb857fee989f7119f69b2874675b85b9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3951,11 +3951,11 @@ let find_sizeof t f =
| Error (msg, t') -> raise (SizeOfError(msg, t'))
with Not_found ->
try
- let size = f () in
- TypSize.add t (Size size) ;
+ let t', size = f () in
+ TypSize.add t' (Size size) ;
size
- with SizeOfError(t',msg) as e ->
- TypSize.add t (Error (t', msg)) ;
+ with SizeOfError(msg, t') as e ->
+ TypSize.add t' (Error (msg, t')) ;
raise e
let selfTypSize = TypSize.self
@@ -4371,7 +4371,7 @@ and bitsSizeOf t =
(SizeOfError
(Format.sprintf "abstract type '%s'" (compFullName comp), t))
| TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
- find_sizeof t (fun () -> 0)
+ find_sizeof t (fun () -> t,0)
| TComp ({cfields=Some[]} as comp,_) ->
find_sizeof t
(fun () ->
@@ -4398,9 +4398,9 @@ and bitsSizeOf t =
then
(* On MSVC if we have just a zero-width bitfields then the length
* is 32 and is not padded *)
- 32
+ t, 32
else
- addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
+ t, addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
| TComp (comp, _) -> (* Union *)
find_sizeof t
@@ -4421,14 +4421,16 @@ and bitsSizeOf t =
(* Note: we treat None above *)
let max = List.fold_left fold 0 (Option.get comp.cfields) in
(* Add trailing by simulating adding an extra field *)
- addTrailing max (8 * bytesAlignOf t))
+ t, addTrailing max (8 * bytesAlignOf t))
- | TArray(bt, Some len, _) ->
+ | TArray(bt, Some len, attrs) ->
find_sizeof t
(fun () ->
begin
- match (constFold true len).enode with
- Const(CInt64(l,_,_)) ->
+ let v = constFold true len in
+ let norm_typ = TArray(bt, Some v, attrs) in
+ match v with
+ { enode = Const(CInt64(l,_,_)) } ->
let sz = Integer.mul (Integer.of_int (bitsSizeOf bt)) l in
let sz' =
match Integer.to_int_opt sz with
@@ -4437,11 +4439,12 @@ and bitsSizeOf t =
raise
(SizeOfError
("Array is so long that its size can't be "
- ^"represented with an OCaml int.", t))
+ ^"represented with an OCaml int.", norm_typ))
in
- sz' (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
- | _ -> raise (SizeOfError ("Array with non-constant length.", t))
+ (norm_typ, sz') (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
+ | _ ->
+ raise (SizeOfError ("Array with non-constant length.", norm_typ))
end)
| TVoid _ ->
if theMachine.theMachine.sizeof_void >= 0 then
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 64e5c108ab5c3840e18f335d49f175bf582864d0..4d69ac1a7f47a72f2d819c48e4655f08e40f7fa6 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -708,86 +708,6 @@ module From = struct
end
end
-(* ************************************************************************* *)
-(** {2 PDG} *)
-(* ************************************************************************* *)
-
-module Pdg = struct
- type t = PdgTypes.Pdg.t
-
- type t_nodes_and_undef =
- ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
-
- exception Top = PdgTypes.Pdg.Top
- exception Bottom = PdgTypes.Pdg.Bottom
-
- let self = ref State.dummy
-
- let get = mk_fun "Pdg.get"
-
- let from_same_fun pdg1 pdg2 =
- let kf1 = PdgTypes.Pdg.get_kf pdg1 in
- let kf2 = PdgTypes.Pdg.get_kf pdg2 in
- Kernel_function.equal kf1 kf2
-
- let node_key = mk_fun "Pdg.node_key"
-
- let find_decl_var_node = mk_fun "Pdg.find_decl_var_node"
- let find_input_node = mk_fun "Pdg.find_input_nodes"
- let find_ret_output_node = mk_fun "Pdg.find_ret_output_node"
- let find_output_nodes = mk_fun "Pdg.find_output_nodes"
- let find_all_inputs_nodes = mk_fun "Pdg.find_all_inputs_nodes"
- let find_stmt_and_blocks_nodes = mk_fun "Pdg.find_stmt_and_blocks_nodes"
- let find_simple_stmt_nodes = mk_fun "Pdg.find_simplestmt_nodes"
- let find_stmt_node = mk_fun "Pdg.find_stmt_node"
- let find_label_node = mk_fun "Pdg.find_label_node"
- let find_entry_point_node = mk_fun "Pdg.find_entry_point_node"
- let find_top_input_node = mk_fun "Pdg.find_top_input_node"
- let find_call_ctrl_node = mk_fun "Pdg.find_call_ctrl_node"
- let find_location_nodes_at_stmt = mk_fun "Pdg.find_location_nodes_at_stmt"
- let find_location_nodes_at_end = mk_fun "Pdg.find_location_nodes_at_end"
- let find_location_nodes_at_begin = mk_fun "Pdg.find_location_nodes_at_begin"
- let find_call_input_node = mk_fun "Pdg.find_call_input_node"
- let find_call_output_node = mk_fun "Pdg.find_call_output_node"
- let find_code_annot_nodes = mk_fun "Pdg.find_code_annot_nodes"
- let find_fun_precond_nodes = mk_fun "Pdg.find_fun_precond_nodes"
- let find_fun_postcond_nodes = mk_fun "Pdg.find_fun_postcond_nodes"
- let find_fun_variant_nodes = mk_fun "Pdg.find_fun_variant_nodes"
-
- let find_call_out_nodes_to_select = mk_fun "Pdg.find_call_out_nodes_to_select"
- let find_in_nodes_to_select_for_this_call =
- mk_fun "Pdg.find_in_nodes_to_select_for_this_call"
-
- let direct_dpds = mk_fun "Pdg.direct_dpds"
- let direct_ctrl_dpds = mk_fun "Pdg.direct_ctrl_dpds"
- let direct_data_dpds = mk_fun "Pdg.direct_data_dpds"
- let direct_addr_dpds = mk_fun "Pdg.direct_addr_dpds"
-
- let all_dpds = mk_fun "Pdg.all_dpds"
- let all_ctrl_dpds = mk_fun "Pdg.all_ctrl_dpds"
- let all_data_dpds = mk_fun "Pdg.all_data_dpds"
- let all_addr_dpds = mk_fun "Pdg.all_addr_dpds"
-
- let direct_uses = mk_fun "Pdg.direct_uses"
- let direct_ctrl_uses = mk_fun "Pdg.direct_ctrl_uses"
- let direct_data_uses = mk_fun "Pdg.direct_data_uses"
- let direct_addr_uses = mk_fun "Pdg.direct_addr_uses"
-
- let all_uses = mk_fun "Pdg.all_uses"
-
- let custom_related_nodes = mk_fun "Pdg.custom_related_nodes"
-
- let find_call_stmts = mk_fun "Pdg.find_call_stmts"
-
- let iter_nodes = mk_fun "Pdg.iter_nodes"
-
- let extract = mk_fun "Pdg.extract"
- let pretty = ref (fun ?bw:_ _ _ -> mk_labeled_fun "Pdg.pretty")
- let pretty_node = mk_fun "Pdg.pretty_node"
- let pretty_key = mk_fun "Pdg.pretty_key"
-
-end
-
(* ************************************************************************* *)
(** {2 Properties} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 905663fa636b56df38e8b0fbcbeda93483098aac..62334a53e2eda38fd43e4b647ac20c2b526507ff 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -844,329 +844,6 @@ module Security : sig
end
-(** Program Dependence Graph.
- @see <../pdg/index.html> PDG internal documentation. *)
-module Pdg : sig
-
- exception Bottom
- (** Raised by most function when the PDG is Bottom because we can hardly do
- nothing with it. It happens when the function is unreachable because we
- have no information about it. *)
-
- exception Top
- (** Raised by most function when the PDG is Top because we can hardly do
- nothing with it. It happens when we didn't manage to compute it, for
- instance for a variadic function. *)
-
- type t = PdgTypes.Pdg.t
- (** PDG type *)
-
- type t_nodes_and_undef =
- ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
- (** type for the return value of many [find_xxx] functions when the
- answer can be a list of [(node, z_part)] and an [undef zone].
- For each node, [z_part] can specify which part of the node
- is used in terms of zone ([None] means all).
- *)
-
- val self : State.t ref
-
- (** {3 Getters} *)
-
- val get : (kernel_function -> t) ref
- (** Get the PDG of a function. Build it if it doesn't exist yet. *)
-
- val node_key : (PdgTypes.Node.t -> PdgIndex.Key.t) ref
-
- val from_same_fun : t -> t -> bool
-
- (** {3 Finding PDG nodes} *)
-
- val find_decl_var_node : (t -> Cil_types.varinfo -> PdgTypes.Node.t) ref
- (** Get the node corresponding the declaration of a local variable or a
- formal parameter.
- @raise Not_found if the variable is not declared in this function.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_ret_output_node : (t -> PdgTypes.Node.t) ref
- (** Get the node corresponding return stmt.
- @raise Not_found if the output state in unreachable
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_output_nodes :
- (t -> PdgIndex.Signature.out_key -> t_nodes_and_undef) ref
- (** Get the nodes corresponding to a call output key in the called pdg.
- @raise Not_found if the output state in unreachable
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_input_node : (t -> int -> PdgTypes.Node.t) ref
- (** Get the node corresponding to a given input (parameter).
- @raise Not_found if the number is not an input number.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_all_inputs_nodes : (t -> PdgTypes.Node.t list) ref
- (** Get the nodes corresponding to all inputs.
- {!node_key} can be used to know their numbers.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_stmt_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) ref
- (** Get the node corresponding to the statement.
- It shouldn't be a call statement.
- See also {!find_simple_stmt_nodes} or {!find_call_stmts}.
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top.
- @raise PdgIndex.CallStatement if the given stmt is a function
- call. *)
-
-
- val find_simple_stmt_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
- (** Get the nodes corresponding to the statement.
- It is usually composed of only one node (see {!find_stmt_node}),
- except for call statement.
- Be careful that for block statements, it only returns a node
- corresponding to the elementary stmt
- (see {!find_stmt_and_blocks_nodes} for more)
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_label_node : (t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t) ref
- (** Get the node corresponding to the label.
- @raise Not_found if the given label is not in the PDG.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_stmt_and_blocks_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
- (** Get the nodes corresponding to the statement like
- * {!find_simple_stmt_nodes} but also add the nodes of the enclosed
- * statements if [stmt] contains blocks.
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_top_input_node : (t -> PdgTypes.Node.t) ref
- (** @raise Not_found if there is no top input in the PDG.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_entry_point_node : (t -> PdgTypes.Node.t) ref
- (** Find the node that represent the entry point of the function, i.e. the
- higher level block.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_location_nodes_at_stmt :
- (t -> Cil_types.stmt -> before:bool -> Locations.Zone.t
- -> t_nodes_and_undef) ref
- (** Find the nodes that define the value of the location at the given
- program point. Also return a zone that might be undefined at that
- point.
- @raise Not_found if the given statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_location_nodes_at_end :
- (t -> Locations.Zone.t -> t_nodes_and_undef) ref
- (** Same than {!find_location_nodes_at_stmt} for the program point located
- at the end of the function.
- @raise Not_found if the output state is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_location_nodes_at_begin :
- (t -> Locations.Zone.t -> t_nodes_and_undef) ref
- (** Same than {!find_location_nodes_at_stmt} for the program point located
- at the beginning of the function.
- Notice that it can only find formal argument nodes.
- The remaining zone (implicit input) is returned as undef.
- @raise Not_found if the output state is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_stmts:
- (kernel_function -> caller:kernel_function -> Cil_types.stmt list) ref
- (** Find the call statements to the function (can maybe be somewhere
- else).
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_ctrl_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) ref
- (** @raise Not_found if the call is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_input_node : (t -> Cil_types.stmt -> int -> PdgTypes.Node.t) ref
- (** @raise Not_found if the call is unreachable or has no such input.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_call_output_node : (t -> Cil_types.stmt -> PdgTypes.Node.t) ref
- (** @raise Not_found if the call is unreachable or has no output node.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_code_annot_nodes :
- (t -> Cil_types.stmt -> Cil_types.code_annotation ->
- PdgTypes.Node.t list * PdgTypes.Node.t list * (t_nodes_and_undef option)) ref
- (** The result is composed of three parts :
- - the first part of the result are the control dependencies nodes
- of the annotation,
- - the second part is the list of declaration nodes of the variables
- used in the annotation;
- - the third part is similar to [find_location_nodes_at_stmt] result
- but for all the locations needed by the annotation.
- When the third part is globally [None],
- it means that we were not able to compute this information.
- @raise Not_found if the statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val find_fun_precond_nodes :
- (t -> Cil_types.predicate -> PdgTypes.Node.t list * (t_nodes_and_undef option)) ref
- (** Similar to [find_code_annot_nodes] (no control dependencies nodes) *)
-
- val find_fun_postcond_nodes :
- (t -> Cil_types.predicate -> PdgTypes.Node.t list * (t_nodes_and_undef option)) ref
- (** Similar to [find_fun_precond_nodes] *)
-
- val find_fun_variant_nodes :
- (t -> Cil_types.term -> (PdgTypes.Node.t list * t_nodes_and_undef option)) ref
- (** Similar to [find_fun_precond_nodes] *)
-
- (** {3 Propagation}
- See also [Pdg.mli] for more function that cannot be here because
- they use polymorphic types.
- **)
-
- val find_call_out_nodes_to_select :
- (t -> PdgTypes.NodeSet.t -> t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
- (** [find_call_out_nodes_to_select pdg_called called_selected_nodes
- pdg_caller call_stmt]
- @return the call outputs nodes [out] such that
- [find_output_nodes pdg_called out_key]
- intersects [called_selected_nodes]. *)
-
- val find_in_nodes_to_select_for_this_call :
- (t -> PdgTypes.NodeSet.t -> Cil_types.stmt -> t -> PdgTypes.Node.t list) ref
- (** [find_in_nodes_to_select_for_this_call
- pdg_caller caller_selected_nodes call_stmt pdg_called]
- @return the called input nodes such that the corresponding nodes
- in the caller intersect [caller_selected_nodes]
- @raise Not_found if the statement is unreachable.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- (** {3 Dependencies} *)
-
- val direct_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Get the nodes to which the given node directly depend on.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_ctrl_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_dpds}, but for control dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_data_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_dpds}, but for data dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_addr_dpds : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_dpds}, but for address dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Transitive closure of {!direct_dpds} for all the given nodes.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_data_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Gives the data dependencies of the given nodes, and recursively, all
- the dependencies of those nodes (regardless to their kind).
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_ctrl_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Similar to {!all_data_dpds} for control dependencies.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_addr_dpds : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** Similar to {!all_data_dpds} for address dependencies.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** build a list of all the nodes that have direct dependencies on the
- given node.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_ctrl_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_uses}, but for control dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_data_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_uses}, but for data dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val direct_addr_uses : (t -> PdgTypes.Node.t -> PdgTypes.Node.t list) ref
- (** Similar to {!direct_uses}, but for address dependencies only.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val all_uses : (t -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** build a list of all the nodes that have dependencies (even indirect) on
- the given nodes.
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val custom_related_nodes :
- ((PdgTypes.Node.t -> PdgTypes.Node.t list) -> PdgTypes.Node.t list -> PdgTypes.Node.t list) ref
- (** [custom_related_nodes get_dpds node_list] build a list, starting from
- the node in [node_list], and recursively add the nodes given by the
- function [get_dpds]. For this function to work well, it is important
- that [get_dpds n] returns a subset of the nodes directly related to
- [n], ie a subset of [direct_uses] U [direct_dpds].
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- val iter_nodes : ((PdgTypes.Node.t -> unit) -> t -> unit) ref
- (** apply a given function to all the PDG nodes
- @raise Bottom if given PDG is bottom.
- @raise Top if the given pdg is top. *)
-
- (** {3 Pretty printing} *)
-
- val extract : (t -> string -> unit) ref
- (** Pretty print pdg into a dot file.
- @see <../pdg/index.html> PDG internal documentation. *)
-
- val pretty_node : (bool -> Format.formatter -> PdgTypes.Node.t -> unit) ref
- (** Pretty print information on a node : with [short=true], only the id
- of the node is printed.. *)
-
- val pretty_key : (Format.formatter -> PdgIndex.Key.t -> unit) ref
- (** Pretty print information on a node key *)
-
- val pretty : (?bw:bool -> Format.formatter -> t -> unit) ref
- (** For debugging... Pretty print pdg information.
- Print codependencies rather than dependencies if [bw=true]. *)
-
-end
-
-
(** Signature common to some Inout plugin options. The results of
the computations are available on a per function basis. *)
module type INOUTKF = sig
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 4814aa3de68bdd6d17d32d595cee401abb95bd43..961f6fe09ec4ba3fcedf46c9a869f5aa369181f9 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -54,6 +54,9 @@ clean:
*.cb *.cm? *.bbl *.blg *.idx *.ind *.ilg \
transf trans.ml pp.ml pp
+super-clean: clean
+ rm -f e-acsl-implementation.pdf e-acsl.pdf
+
#########
# Tools #
#########
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 8486028efd975dbb02cf54f4540b6aaf3fafa1d7..14ee4a24894e7fc06e7c18dbe438c3aabd725d4a 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -35,3 +35,6 @@ clean:
*.haux *.hbbl *.htoc \
*.cb *.cm? *.bbl *.blg *.idx *.ind *.ilg \
transf trans.ml pp.ml pp
+
+super-clean: clean
+ rm -f $(MAIN).pdf
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 1744f0a3e7da3f56490a759d998ecd28957c7be2..9f1379f3ec9104f0e9c23927c726ed55e9f30ce6 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -22,7 +22,10 @@
open Cil_types
open Cil_datatype
+
+open Pdg_types
open PdgIndex
+
open Reason_graph
(** Computation of the PDG nodes that are impacted by the "execution"
@@ -166,7 +169,7 @@ let add_to_result wl n kf init =
(** return [true] if the location in [n] is contained in [skip], in which
case the node should be skipped entirely *)
let node_to_skip skip n =
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| Key.SigKey (Signature.In (Signature.InImpl z))
| Key.SigKey (Signature.Out (Signature.OutLoc z))
| Key.SigCallKey (_, Signature.In (Signature.InImpl z))
@@ -179,7 +182,7 @@ let node_to_skip skip n =
the results *)
let filter wl (n, z) =
not (Locations.Zone.is_bottom z) &&
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| Key.SigKey (Signature.In Signature.InCtrl) -> false
(* do not consider node [InCtrl]. YYY: find when this may happen *)
| Key.VarDecl _ -> false
@@ -320,7 +323,7 @@ let add_downward_call wl (caller_kf, pdg) (called_kf, called_pdg) stmt =
callee are directly in the worklist, and the call is registered in the
field [downward_calls]. *)
let downward_one_call_node wl (pnode, _ as node) caller_kf pdg =
- match !Db.Pdg.node_key pnode with
+ match Pdg.Api.node_key pnode with
| Key.SigKey (Signature.In Signature.InCtrl) (* never in the worklist *)
| Key.VarDecl _ (* never in the worklist *)
| Key.CallStmt _ (* pdg returns a SigCallKey instead *)
@@ -335,31 +338,31 @@ let downward_one_call_node wl (pnode, _ as node) caller_kf pdg =
let called_kfs = Eva.Results.callee stmt in
List.iter
(fun called_kf ->
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg.Api.get called_kf in
let nodes_callee, pdg_ok =
Options.debug ~level:3 "%a: considering call to %a"
Pdg_aux.pretty_node node Kernel_function.pretty called_kf;
try
(match key with
| Signature.In (Signature.InNum n) ->
- (try [!Db.Pdg.find_input_node called_pdg n,
+ (try [Pdg.Api.find_input_node called_pdg n,
Locations.Zone.top]
with Not_found -> [])
| Signature.In Signature.InCtrl ->
- (try [!Db.Pdg.find_entry_point_node called_pdg,
+ (try [Pdg.Api.find_entry_point_node called_pdg,
Locations.Zone.top]
with Not_found -> [])
| Signature.In (Signature.InImpl _) -> assert false
| Signature.Out _ -> []
), true
with
- | Db.Pdg.Top ->
+ | Pdg.Api.Top ->
Options.warning
"no precise pdg for function %s. \n\
Ignoring this function in the analysis (potentially incorrect results)."
(Kernel_function.get_name called_kf);
[], false
- | Db.Pdg.Bottom ->
+ | Pdg.Api.Bottom ->
(*Function that fails or never returns immediately *)
[], false
| Not_found -> assert false
@@ -398,7 +401,7 @@ let downward_one_call_inputs wl kf_caller kf_callee (node, deps) =
(fun nsrc ->
add_to_reason wl ~nsrc ~ndst:node' InterproceduralDownward)
inter;
- add_to_do wl kf_callee (!Db.Pdg.get kf_callee) node';
+ add_to_do wl kf_callee (Pdg.Api.get kf_callee) node';
;;
(** Propagate impact for all calls registered in [downward_calls]. For each
@@ -447,10 +450,10 @@ let all_upward_callers wl kfs =
let todo =
if not (KFS.mem kf wl.callers) then (
Options.debug "Found caller %a" Kernel_function.pretty kf;
- let pdg_kf = !Db.Pdg.get kf in
+ let pdg_kf = Pdg.Api.get kf in
List.fold_left
(fun todo (caller, callsites) ->
- let pdg_caller = !Db.Pdg.get caller in
+ let pdg_caller = Pdg.Api.get caller in
List.iter (aux_call (caller, pdg_caller) (kf, pdg_kf)) callsites;
KFS.add caller todo
) todo (Eva.Results.callsites kf);
@@ -486,9 +489,9 @@ let upward_in_callers wl =
add_to_reason wl ~nsrc ~ndst:n InterproceduralUpward
) inter;
if init then
- add_to_do_part_of_initial wl caller (!Db.Pdg.get caller) n
+ add_to_do_part_of_initial wl caller (Pdg.Api.get caller) n
else
- add_to_do wl caller (!Db.Pdg.get caller) n
+ add_to_do wl caller (Pdg.Api.get caller) n
) (Lazy.force l)
in
KfKfCall.Map.iter aux wl.upward_calls;
@@ -522,7 +525,7 @@ let initial_worklist ?(skip=Locations.Zone.bottom) ?(reason=false) nodes kf =
}
in
(* Fill the [todo] field *)
- initial_to_do_list wl kf (!Db.Pdg.get kf) nodes;
+ initial_to_do_list wl kf (Pdg.Api.get kf) nodes;
let initial_callers =
if Options.Upward.get () then KFS.singleton kf else KFS.empty
in
@@ -536,10 +539,10 @@ let initial_worklist ?(skip=Locations.Zone.bottom) ?(reason=false) nodes kf =
callees of the call. *)
let initial_nodes ~skip kf stmt =
Options.debug ~level:3 "computing initial nodes for %d" stmt.sid;
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
if Eva.Results.is_reachable stmt then
try
- let all = !Db.Pdg.find_simple_stmt_nodes pdg stmt in
+ let all = Pdg.Api.find_simple_stmt_nodes pdg stmt in
let filter n = match PdgTypes.Node.elem_key n with
| Key.SigCallKey (_, Signature.In _) -> false
| _ -> not (node_to_skip skip n)
@@ -669,7 +672,7 @@ let result_to_nodes (res: result) : nodes =
(** Transform a set of PDG nodes into a set of statements *)
let nodes_to_stmts ns =
- let get_stmt node = Key.stmt (!Db.Pdg.node_key node) in
+ let get_stmt node = Key.stmt (Pdg.Api.node_key node) in
let set =
(* Do not generate a list immediately, some nodes would be duplicated *)
NS.fold
diff --git a/src/plugins/impact/compute_impact.mli b/src/plugins/impact/compute_impact.mli
index 64307dc66281a1879dd0e7332ef9748ce058813c..74831f03df77459e0b84f0b5a17f7c2154dd3c43 100644
--- a/src/plugins/impact/compute_impact.mli
+++ b/src/plugins/impact/compute_impact.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
type nodes = Pdg_aux.NS.t
type result = nodes Kernel_function.Map.t
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index 734041fbd969ca0f0697b1d757282f93c417c8d7..6bcede10dbbcfd1333725c7a55c804e15abbe9ae 100644
--- a/src/plugins/impact/dune
+++ b/src/plugins/impact/dune
@@ -28,6 +28,7 @@
(echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
(echo " - Slicing:" %{lib-available:frama-c-slicing.core} "\n")
(echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
)
)
)
@@ -38,7 +39,7 @@
(optional)
(public_name frama-c-impact.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
+ (libraries frama-c.kernel frama-c-pdg.core frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
)
(plugin (optional) (name impact) (libraries frama-c-impact.core) (site (frama-c plugins)))
diff --git a/src/plugins/impact/gui/dune b/src/plugins/impact/gui/dune
index 39db9c604eff13ccd99f1853b7a7061a4f6e8c89..e00946f69448800bdd05a5e35f6bbf859a7e19ec 100644
--- a/src/plugins/impact/gui/dune
+++ b/src/plugins/impact/gui/dune
@@ -25,7 +25,7 @@
(public_name frama-c-impact.gui)
(optional)
(flags -open Frama_c_kernel -open Frama_c_gui -open Impact :standard -w -9)
- (libraries frama-c.kernel frama-c.gui frama-c-impact.core frama-c-slicing.core frama-c-callgraph.core)
+ (libraries frama-c.kernel frama-c.gui frama-c-pdg.core frama-c-impact.core frama-c-slicing.core frama-c-callgraph.core)
)
(plugin (optional) (name impact-gui) (libraries frama-c-impact.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/impact/gui/register_gui.ml b/src/plugins/impact/gui/register_gui.ml
index 5146cb4a509f753a2e4ef66c8eac70c68377cf11..1bd988cb199607a31a287fa4df715fb8916fa52b 100644
--- a/src/plugins/impact/gui/register_gui.ml
+++ b/src/plugins/impact/gui/register_gui.ml
@@ -22,8 +22,8 @@
open Pretty_source
open Gtk_helper
-open Db
open Cil_types
+open Pdg_types
module SelectedStmt = struct
include State_builder.Option_ref
@@ -43,7 +43,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:SelectedStmt.self
- [ !Db.Pdg.self ])
+ [ Pdg.Api.self ])
module Highlighted_stmt : sig
val add: Kernel_function.t -> stmt -> unit
@@ -232,7 +232,7 @@ let pp_impact_on_inputs (main_ui:Design.main_window_extension_points) kf =
let call, formals, zones =
Pdg_aux.NS.fold
(fun (node, z) (call, formals, zones as acc) ->
- match !Pdg.node_key node with
+ match Pdg.Api.node_key node with
| SigCallKey _ | CallStmt _ | Stmt _ | Label _ ->
acc (* Related to one stmt: skip *)
| VarDecl _ -> acc (* skip *)
@@ -268,7 +268,7 @@ let pp_impacted_call_outputs
let ret, zones =
Pdg_aux.NS.fold
(fun (node, z) (ret, zones as acc) ->
- match !Pdg.node_key node with
+ match Pdg.Api.node_key node with
| SigCallKey (stmt', key)
when Cil_datatype.Stmt.equal call_stmt stmt' ->
(match key with
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index 8513bcf24116c76db8f094446ad837068f527f2e..0a3b4acb21ed47d3e6ab5e15869955fd91164b06 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -20,12 +20,12 @@
(* *)
(**************************************************************************)
+open Pdg_types
open PdgIndex
open Locations
type node = PdgTypes.Node.t * Zone.t
-
module NS = struct
include Hptmap.Make
(PdgTypes.Node)
@@ -159,7 +159,7 @@ let find_call_input_nodes pdg_caller call_stmt ?(z=Locations.Zone.top) in_key =
(* skip undef zone: any result different from None is due to calldeps or
some imprecision. *)
let nodes, _undef =
- !Db.Pdg.find_location_nodes_at_stmt
+ Pdg.Api.find_location_nodes_at_stmt
pdg_caller call_stmt ~before:true zone'
in
nodes
@@ -201,7 +201,7 @@ let all_call_out_nodes ~callee ~caller call_stmt =
in
let test_out acc (out_key, call_out_node) =
(* skip undef: any zone found undef is due to an imprecision or a bug*)
- let out_nodes, _ = !Db.Pdg.find_output_nodes callee out_key in
+ let out_nodes, _ = Pdg.Api.find_output_nodes callee out_key in
let out_nodes = node_list_to_set out_nodes in
(call_out_node, out_nodes) :: acc
in
diff --git a/src/plugins/impact/pdg_aux.mli b/src/plugins/impact/pdg_aux.mli
index 32e7f34d68c3decd9bc4b30df0046734c05d5012..f07aca633a1ca26345642e911cf4567fa5d6a3fb 100644
--- a/src/plugins/impact/pdg_aux.mli
+++ b/src/plugins/impact/pdg_aux.mli
@@ -21,16 +21,17 @@
(**************************************************************************)
open Cil_types
-open PdgTypes
open Locations
+open Pdg_types
+
(** Useful functions that are not directly accessible through the other
Pdg modules. *)
(** Refinement of a PDG node: we add an indication of which zone is really
impacted *)
-type node = Node.t * Zone.t
+type node = PdgTypes.Node.t * Zone.t
val pretty_node: node Pretty_utils.formatter
@@ -53,9 +54,9 @@ module NS: sig
val inter: t -> t -> t
val diff: t -> t -> t
- val remove: Node.t -> t -> t
+ val remove: PdgTypes.Node.t -> t -> t
- val mem: Node.t -> t -> bool
+ val mem: PdgTypes.Node.t -> t -> bool
val mem': node -> t -> bool
val intersects: t -> t -> bool
val for_all': (node -> bool) -> t -> bool
@@ -76,7 +77,7 @@ type call_interface = (PdgTypes.Node.t * NS.t) list
of [callee]. Each input node in [callee] is returned with the set
of nodes that define it in [caller]. *)
val all_call_input_nodes:
- caller:Db.Pdg.t -> callee:kernel_function * Db.Pdg.t -> stmt ->
+ caller:Pdg.Api.t -> callee:kernel_function * Pdg.Api.t -> stmt ->
call_interface
(** [all_call_out_nodes ~callee ~caller stmt] find all the nodes of [callee]
@@ -84,4 +85,4 @@ val all_call_input_nodes:
that occurs at [stmt]. Each such out node is returned, with the set
of nodes that define it in [callee] *)
val all_call_out_nodes :
- callee:Db.Pdg.t -> caller:Db.Pdg.t -> stmt -> call_interface
+ callee:Pdg.Api.t -> caller:Pdg.Api.t -> stmt -> call_interface
diff --git a/src/plugins/impact/reason_graph.ml b/src/plugins/impact/reason_graph.ml
index eceba7800cf411e23e0689b306edd741f1ef07cb..eb8452ccdd367b01b77d582fb0b6571ea7bbb209 100644
--- a/src/plugins/impact/reason_graph.ml
+++ b/src/plugins/impact/reason_graph.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
module NodeSet = PdgTypes.NodeSet
@@ -216,7 +218,7 @@ let print_dot_graph reason =
(* Very basic textual debugging function *)
let _print_reason reason =
- let pp_node = !Db.Pdg.pretty_node false in
+ let pp_node = Pdg.Api.pretty_node false in
let pp fmt (nsrc, ndst, reason) =
Format.fprintf fmt "@[<v 2>%a -> %a (%s)@]"
pp_node nsrc pp_node ndst
diff --git a/src/plugins/impact/reason_graph.mli b/src/plugins/impact/reason_graph.mli
index d0f03c55694e1a5d10439b237934cd69bce29d10..ccdbd733b2207e905a3d7054b204fcea8a674433 100644
--- a/src/plugins/impact/reason_graph.mli
+++ b/src/plugins/impact/reason_graph.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
(** Why is a node impacted. The reasons will be given as [n is impacted
by the effect of [n'], and the impact is of type reason]. *)
type reason_type =
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 6dfc46429bd86b280c90ba5418fb0e552a2314bb..e9b09ca1784c2b9f1d8e547f27209b48f3284003 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
let rec pp_stmt fmt s = match s.skind with
| Instr _ | Return _ | Goto _ | Break _ | Continue _ | TryFinally _
| TryExcept _ | Throw _ | TryCatch _ ->
diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli
index a426a0bb2b23bc8422b0ec2a2b818d0834729721..7cdc3c047533c1b1c7e33408488ce820ba5bff83 100644
--- a/src/plugins/impact/register.mli
+++ b/src/plugins/impact/register.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
val compute_pragmas: (unit -> stmt list)
(** Compute the impact analysis from the impact pragma in the program.
Print and slice the results according to the parameters -impact-print
diff --git a/src/plugins/pdg/Pdg.ml b/src/plugins/pdg/Pdg.ml
index 40d3a5633796cc24cd35e6286651003365ec1568..2472224ae4c3981e0e6720ab359d8b6f8ea034a6 100644
--- a/src/plugins/pdg/Pdg.ml
+++ b/src/plugins/pdg/Pdg.ml
@@ -22,7 +22,6 @@
(** Program Dependences Graph. *)
-(** Functions for this plugin are registered through the [Db] module,
- the dynamic API, and the module Below. *)
+module Api = Api
-module Register = Register
+module Marks = Marks
diff --git a/src/plugins/pdg/Pdg.mli b/src/plugins/pdg/Pdg.mli
index 2fcfa88853137ba80dbddf902f353d2bbc5ac1fb..aaaefb329d90b35ec8a6078cf2d3cd5d767ca2d1 100644
--- a/src/plugins/pdg/Pdg.mli
+++ b/src/plugins/pdg/Pdg.mli
@@ -22,7 +22,6 @@
(** Program Dependences Graph. *)
-(** Functions for this plugin are registered through the [Db] module,
- the dynamic API, and the module Below. *)
+module Api : module type of Api
-module Register : module type of Marks
+module Marks : module type of Marks
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index d76dc95c38da8546bce3569b83ddcadbb3fbfa54..09c37fa94373490d0eb7133f4c09be10d36bccec 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -22,6 +22,8 @@
open Cil_types
open Cil_datatype
+
+open Pdg_types
open PdgIndex
type data_info = ((PdgTypes.Node.t * Locations.Zone.t option) list
@@ -117,13 +119,13 @@ let find_code_annot_nodes pdg stmt annot =
let labels = decl_label_info.Db.Properties.Interp.To_zone.lbl in
let stmt_key = Key.stmt_key stmt in
let stmt_node = match stmt_key with
- | Key.Stmt _ -> !Db.Pdg.find_stmt_node pdg stmt
- | Key.CallStmt _ -> !Db.Pdg.find_call_ctrl_node pdg stmt
+ | Key.Stmt _ -> Sets.find_stmt_node pdg stmt
+ | Key.CallStmt _ -> Sets.find_call_ctrl_node pdg stmt
| _ -> assert false
in
- let ctrl_dpds = !Db.Pdg.direct_ctrl_dpds pdg stmt_node in
+ let ctrl_dpds = Sets.direct_ctrl_dpds pdg stmt_node in
let add_stmt_nodes s acc =
- try !Db.Pdg.find_stmt_and_blocks_nodes pdg s @ acc
+ try Sets.find_stmt_and_blocks_nodes pdg s @ acc
with Not_found -> acc
in
(* can safely ignore pragmas.ctrl
diff --git a/src/plugins/pdg/annot.mli b/src/plugins/pdg/annot.mli
index 8aa296375843ddb909c61cba30f6b76014ea6c3e..c46dd70667d8e4df934d0843732858f3694fa267 100644
--- a/src/plugins/pdg/annot.mli
+++ b/src/plugins/pdg/annot.mli
@@ -24,6 +24,8 @@
@raise Kernel_function.No_Definition on annotations for function declarations.
*)
+open Pdg_types
+
(** [data_info] is composed of [(node,z_part) list, undef_loc)]
* and correspond to data dependencies nodes.
* Can be None if we don't know how to compute them.
diff --git a/src/plugins/pdg/api.ml b/src/plugins/pdg/api.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0024018d796890a4136e964dcbc48c9d1ee97ec7
--- /dev/null
+++ b/src/plugins/pdg/api.ml
@@ -0,0 +1,113 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+[@@@ warning "-32" ]
+
+open Pdg_types
+
+type t = PdgTypes.Pdg.t
+
+type t_nodes_and_undef =
+ ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
+
+exception Top = PdgTypes.Pdg.Top
+exception Bottom = PdgTypes.Pdg.Bottom
+
+(**************************************************************************)
+
+let self = Pdg_tbl.self
+let get = Pdg_tbl.get
+
+let node_key = PdgTypes.Node.elem_key
+
+let from_same_fun pdg1 pdg2 =
+ let kf1 = PdgTypes.Pdg.get_kf pdg1 in
+ let kf2 = PdgTypes.Pdg.get_kf pdg2 in
+ Kernel_function.equal kf1 kf2
+
+(**************************************************************************)
+let find_decl_var_node = Sets.find_decl_var_node
+let find_entry_point_node = Sets.find_entry_point_node
+let find_top_input_node = Sets.find_top_input_node
+let find_simple_stmt_nodes = Sets.find_simple_stmt_nodes
+let find_stmt_and_blocks_nodes = Sets.find_stmt_and_blocks_nodes
+let find_stmt_node = Sets.find_stmt_node
+let find_label_node = Sets.find_label_node
+let find_location_nodes_at_stmt = Sets.find_location_nodes_at_stmt
+let find_location_nodes_at_begin = Sets.find_location_nodes_at_begin
+let find_location_nodes_at_end = Sets.find_location_nodes_at_end
+let find_call_ctrl_node = Sets.find_call_ctrl_node
+let find_call_input_node = Sets.find_call_num_input_node
+let find_call_output_node = Sets.find_call_output_node
+let find_input_node = Sets.find_input_node
+let find_ret_output_node = Sets.find_output_node
+let find_output_nodes = Sets.find_output_nodes
+let find_all_inputs_nodes = Sets.find_all_input_nodes
+
+let find_call_stmts = Sets.find_call_stmts
+
+let find_code_annot_nodes = Annot.find_code_annot_nodes
+let find_fun_precond_nodes = Annot.find_fun_precond_nodes
+let find_fun_postcond_nodes = Annot.find_fun_postcond_nodes
+let find_fun_variant_nodes = Annot.find_fun_variant_nodes
+
+let find_call_out_nodes_to_select = Sets.find_call_out_nodes_to_select
+let find_in_nodes_to_select_for_this_call =
+ Sets.find_in_nodes_to_select_for_this_call
+
+(**************************************************************************)
+
+let direct_dpds = Sets.direct_dpds
+let direct_ctrl_dpds = Sets.direct_ctrl_dpds
+let direct_data_dpds = Sets.direct_data_dpds
+let direct_addr_dpds = Sets.direct_addr_dpds
+
+let all_dpds = Sets.find_nodes_all_dpds
+let all_ctrl_dpds = Sets.find_nodes_all_ctrl_dpds
+let all_data_dpds = Sets.find_nodes_all_data_dpds
+let all_addr_dpds = Sets.find_nodes_all_addr_dpds
+
+let direct_uses = Sets.direct_uses
+let direct_ctrl_uses = Sets.direct_ctrl_uses
+let direct_data_uses = Sets.direct_data_uses
+let direct_addr_uses = Sets.direct_addr_uses
+
+let all_uses = Sets.all_uses
+
+let custom_related_nodes = Sets.custom_related_nodes
+
+let iter_nodes = PdgTypes.Pdg.iter_nodes
+
+(**************************************************************************)
+
+
+let extract = Pdg_tbl.print_dot
+
+let pretty_node = Pdg_tbl.pretty_node
+let pretty_key = Pdg_tbl.pretty_key
+let pretty = Pdg_tbl.pretty
+
+(**************************************************************************)
+
+module Marks = Marks
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/api.mli b/src/plugins/pdg/api.mli
new file mode 100644
index 0000000000000000000000000000000000000000..6094779cec4e5920a5575b27b90613eae0deaf66
--- /dev/null
+++ b/src/plugins/pdg/api.mli
@@ -0,0 +1,352 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 Pdg_types
+
+type t = PdgTypes.Pdg.t
+(** Program Dependence Graph type *)
+
+type t_nodes_and_undef =
+ ((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
+(** type for the return value of many [find_xxx] functions when the
+ answer can be a list of [(node, z_part)] and an [undef zone].
+ For each node, [z_part] can specify which part of the node
+ is used in terms of zone ([None] means all). *)
+
+(**************************************************************************)
+
+exception Bottom
+(** Raised by most function when the PDG is Bottom because we can hardly do
+ nothing with it. It happens when the function is unreachable because we
+ have no information about it. *)
+
+exception Top
+(** Raised by most function when the PDG is Top because we can hardly do
+ nothing with it. It happens when we didn't manage to compute it, for
+ instance for a variadic function. *)
+
+(**************************************************************************)
+
+val self : State.t
+(** PDG depedency state *)
+
+(**************************************************************************)
+
+(** {3 Getters} *)
+
+val get : Cil_types.kernel_function -> t
+(** Get the PDG of a function. Build it if it doesn't exist yet. *)
+
+val node_key : PdgTypes.Node.t -> PdgIndex.Key.t
+
+val from_same_fun : t -> t -> bool
+
+(**************************************************************************)
+
+(** {Finding PDG nodes} *)
+
+val find_decl_var_node : t -> Cil_types.varinfo -> PdgTypes.Node.t
+(** Get the node corresponding the declaration of a local variable or a
+ formal parameter.
+ @raise Not_found if the variable is not declared in this function.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_ret_output_node : t -> PdgTypes.Node.t
+(** Get the node corresponding return stmt.
+ @raise Not_found if the output state in unreachable
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_output_nodes : t -> PdgIndex.Signature.out_key -> t_nodes_and_undef
+(** Get the nodes corresponding to a call output key in the called pdg.
+ @raise Not_found if the output state in unreachable
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_input_node : t -> int -> PdgTypes.Node.t
+(** Get the node corresponding to a given input (parameter).
+ @raise Not_found if the number is not an input number.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_all_inputs_nodes : t -> PdgTypes.Node.t list
+(** Get the nodes corresponding to all inputs.
+ {!node_key} can be used to know their numbers.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_stmt_node : t -> Cil_types.stmt -> PdgTypes.Node.t
+(** Get the node corresponding to the statement.
+ It shouldn't be a call statement.
+ See also {!find_simple_stmt_nodes} or {!find_call_stmts}.
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top.
+ @raise PdgIndex.CallStatement if the given stmt is a function
+ call. *)
+
+
+val find_simple_stmt_nodes : t -> Cil_types.stmt -> PdgTypes.Node.t list
+(** Get the nodes corresponding to the statement.
+ It is usually composed of only one node (see {!find_stmt_node}),
+ except for call statement.
+ Be careful that for block statements, it only returns a node
+ corresponding to the elementary stmt
+ (see {!find_stmt_and_blocks_nodes} for more)
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_label_node : t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t
+(** Get the node corresponding to the label.
+ @raise Not_found if the given label is not in the PDG.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_stmt_and_blocks_nodes : t -> Cil_types.stmt -> PdgTypes.Node.t list
+(** Get the nodes corresponding to the statement like
+ {!find_simple_stmt_nodes} but also add the nodes of the enclosed
+ statements if [stmt] contains blocks.
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_top_input_node : t -> PdgTypes.Node.t
+(** @raise Not_found if there is no top input in the PDG.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_entry_point_node : t -> PdgTypes.Node.t
+(** Find the node that represent the entry point of the function, i.e. the
+ higher level block.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_location_nodes_at_stmt : t -> Cil_types.stmt -> before:bool ->
+ Locations.Zone.t -> t_nodes_and_undef
+(** Find the nodes that define the value of the location at the given
+ program point. Also return a zone that might be undefined at that point.
+ @raise Not_found if the given statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_location_nodes_at_end : t -> Locations.Zone.t -> t_nodes_and_undef
+(** Same than {!find_location_nodes_at_stmt} for the program point located
+ at the end of the function.
+ @raise Not_found if the output state is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_location_nodes_at_begin : t -> Locations.Zone.t -> t_nodes_and_undef
+(** Same than {!find_location_nodes_at_stmt} for the program point located
+ at the beginning of the function.
+ Notice that it can only find formal argument nodes.
+ The remaining zone (implicit input) is returned as undef.
+ @raise Not_found if the output state is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_stmts : Cil_types.kernel_function ->
+ caller:Cil_types.kernel_function -> Cil_types.stmt list
+(** Find the call statements to the function (can maybe be somewhere
+ else).
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_ctrl_node : t -> Cil_types.stmt -> PdgTypes.Node.t
+(** @raise Not_found if the call is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_input_node : t -> Cil_types.stmt -> int -> PdgTypes.Node.t
+(** @raise Not_found if the call is unreachable or has no such input.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_call_output_node : t -> Cil_types.stmt -> PdgTypes.Node.t
+(** @raise Not_found if the call is unreachable or has no output node.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_code_annot_nodes : t -> Cil_types.stmt ->
+ Cil_types.code_annotation ->
+ PdgTypes.Node.t list * PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** The result is composed of three parts :
+ - the first part of the result are the control dependencies nodes
+ of the annotation,
+ - the second part is the list of declaration nodes of the variables
+ used in the annotation;
+ - the third part is similar to [find_location_nodes_at_stmt] result
+ but for all the locations needed by the annotation.
+ When the third part is globally [None],
+ it means that we were not able to compute this information.
+ @raise Not_found if the statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val find_fun_precond_nodes : t -> Cil_types.predicate ->
+ PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** Similar to [find_code_annot_nodes] (no control dependencies nodes) *)
+
+val find_fun_postcond_nodes : t -> Cil_types.predicate ->
+ PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** Similar to [find_fun_precond_nodes] *)
+
+val find_fun_variant_nodes : t -> Cil_types.term ->
+ PdgTypes.Node.t list * (t_nodes_and_undef option)
+(** Similar to [find_fun_precond_nodes] *)
+
+(**************************************************************************)
+
+(** {3 Propagation}
+ See also [Pdg.mli] for more function that cannot be here because
+ they use polymorphic types. **)
+
+val find_call_out_nodes_to_select :
+ t -> PdgTypes.NodeSet.t -> t -> Cil_types.stmt -> PdgTypes.Node.t list
+(** [find_call_out_nodes_to_select pdg_called called_selected_nodes
+ pdg_caller call_stmt]
+ @return the call outputs nodes [out] such that
+ [find_output_nodes pdg_called out_key]
+ intersects [called_selected_nodes]. *)
+
+val find_in_nodes_to_select_for_this_call :
+ t -> PdgTypes.NodeSet.t -> Cil_types.stmt -> t -> PdgTypes.Node.t list
+(** [find_in_nodes_to_select_for_this_call
+ pdg_caller caller_selected_nodes call_stmt pdg_called]
+ @return the called input nodes such that the corresponding nodes
+ in the caller intersect [caller_selected_nodes]
+ @raise Not_found if the statement is unreachable.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+(**************************************************************************)
+
+(** {3 Dependencies} *)
+
+val direct_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Get the nodes to which the given node directly depend on.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_ctrl_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_dpds}, but for control dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_data_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_dpds}, but for data dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_addr_dpds : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_dpds}, but for address dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Transitive closure of {!direct_dpds} for all the given nodes.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_data_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Gives the data dependencies of the given nodes, and recursively, all
+ the dependencies of those nodes (regardless to their kind).
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_ctrl_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Similar to {!all_data_dpds} for control dependencies.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_addr_dpds : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** Similar to {!all_data_dpds} for address dependencies.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** build a list of all the nodes that have direct dependencies on the
+ given node.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_ctrl_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_uses}, but for control dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_data_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_uses}, but for data dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val direct_addr_uses : t -> PdgTypes.Node.t -> PdgTypes.Node.t list
+(** Similar to {!direct_uses}, but for address dependencies only.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val all_uses : t -> PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** build a list of all the nodes that have dependencies (even indirect) on
+ the given nodes.
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val custom_related_nodes : (PdgTypes.Node.t -> PdgTypes.Node.t list) ->
+ PdgTypes.Node.t list -> PdgTypes.Node.t list
+(** [custom_related_nodes get_dpds node_list] build a list, starting from
+ the node in [node_list], and recursively add the nodes given by the
+ function [get_dpds]. For this function to work well, it is important
+ that [get_dpds n] returns a subset of the nodes directly related to
+ [n], ie a subset of [direct_uses] U [direct_dpds].
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+val iter_nodes : (PdgTypes.Node.t -> unit) -> t -> unit
+(** apply a given function to all the PDG nodes
+ @raise Bottom if given PDG is bottom.
+ @raise Top if the given pdg is top. *)
+
+(**************************************************************************)
+
+(** {3 Printers} *)
+
+val extract : t -> string -> unit
+(** Pretty print pdg into a dot file. *)
+
+val pretty_node : bool -> Format.formatter -> PdgTypes.Node.t -> unit
+(** Pretty print information on a node : with [short=true], only the id
+ of the node is printed.. *)
+
+val pretty_key : Format.formatter -> PdgIndex.Key.t -> unit
+(** Pretty print information on a node key *)
+
+val pretty : ?bw:bool -> Format.formatter -> t -> unit
+(** For debugging... Pretty print pdg information.
+ Print codependencies rather than dependencies if [bw=true]. *)
+
+(**************************************************************************)
+
+module Marks : module type of Marks
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 256f3d9f9980db347853fa0fcef8ed3ab51deb27..34dfb781a9acc918cf7bbffb2cd0f28718053bbd 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -31,6 +31,8 @@
{!module: Build.Computer} below).
*)
+open Pdg_types
+
let dkey = Pdg_parameters.register_category "build"
let debug fmt = Pdg_parameters.debug ~dkey fmt
let debug2 fmt = Pdg_parameters.debug ~dkey fmt ~level:2
diff --git a/src/plugins/pdg/build.mli b/src/plugins/pdg/build.mli
index 583fdbc47301200ea659df06ad1ba628c46044f9..6e134517409b423d3a2dab2e50cfa49f4f2a20a1 100644
--- a/src/plugins/pdg/build.mli
+++ b/src/plugins/pdg/build.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val compute_pdg : Cil_types.kernel_function -> PdgTypes.Pdg.t
(*
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 09b16b196070e41eb98cc7c8d813def69334e81c..8e02c55d171fe9f97229f4b502f4820a1885bc63 100644
--- a/src/plugins/pdg/dune
+++ b/src/plugins/pdg/dune
@@ -25,6 +25,7 @@
(deps (universe))
(action (progn
(echo "PDG:" %{lib-available:frama-c-pdg.core} "\n")
+ (echo " - Pdg-Types:" %{lib-available:frama-c-pdg.types.core} "\n")
(echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
(echo " - From:" %{lib-available:frama-c-from.core} "\n")
@@ -37,7 +38,7 @@
(optional)
(public_name frama-c-pdg.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-pdg.types.core frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
)
(plugin (optional) (name pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg/marks.ml b/src/plugins/pdg/marks.ml
index 272b5b1ad9fe0928b90ed766e1c06a0345f5afcc..6330ce5fb40bb8dfbe87e315f1ed4c2639b905d1 100644
--- a/src/plugins/pdg/marks.ml
+++ b/src/plugins/pdg/marks.ml
@@ -20,9 +20,11 @@
(* *)
(**************************************************************************)
-open PdgIndex
open Cil_datatype
+open Pdg_types
+open PdgIndex
+
(** compute the marks to propagate in the caller nodes from the marks of
* a function inputs [in_marks].
*)
@@ -36,12 +38,12 @@ let in_marks_to_caller pdg call m2m ?(rqs=[]) in_marks =
let build rqs (in_key, m) =
match in_key with
| Signature.InCtrl ->
- add_n_m rqs (!Db.Pdg.find_call_ctrl_node pdg call) None m
+ add_n_m rqs (Sets.find_call_ctrl_node pdg call) None m
| Signature.InNum in_num ->
- add_n_m rqs (!Db.Pdg.find_call_input_node pdg call in_num) None m
+ add_n_m rqs (Sets.find_call_num_input_node pdg call in_num) None m
| Signature.InImpl zone ->
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg call ~before:true zone
+ Sets.find_location_nodes_at_stmt pdg call ~before:true zone
in
let rqs =
List.fold_left (fun acc (n,z) -> add_n_m acc n z m) rqs nodes in
@@ -64,10 +66,10 @@ let translate_in_marks pdg_called in_new_marks
in_marks_to_caller pdg call (m2m (Some call) pdg) ~rqs in_new_marks
in
let build rqs caller =
- let pdg_caller = !Db.Pdg.get caller in
+ let pdg_caller = Pdg_tbl.get caller in
let caller_rqs =
try
- let call_stmts = !Db.Pdg.find_call_stmts ~caller kf_called in
+ let call_stmts = Sets.find_call_stmts ~caller kf_called in
(* TODO : more intelligent merge ? *)
let rqs = List.fold_left (translate pdg_caller) [] call_stmts in
PdgMarks.SelList rqs
@@ -98,7 +100,7 @@ let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks =
let translate_out_mark _pdg m2m other_rqs (call, l) =
let add_list l_out_m rqs called_kf =
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg_tbl.get called_kf in
let m2m = m2m (Some call) called_pdg in
try
let node_marks =
@@ -165,7 +167,7 @@ module F_Proj (C : PdgMarks.Config) :
let fct_var = Kernel_function.get_vi kf in
try Varinfo.Hashtbl.find proj fct_var
with Not_found ->
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg_tbl.get kf in
let info = F.create pdg in
Varinfo.Hashtbl.add proj fct_var info;
info
diff --git a/src/plugins/pdg/marks.mli b/src/plugins/pdg/marks.mli
index 55a303293f931a46d482ff89bc32e84d1ad9666d..846aeae6adace9a638d1fbda719eff249dec6731 100644
--- a/src/plugins/pdg/marks.mli
+++ b/src/plugins/pdg/marks.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
open PdgMarks
(** [in_marks_to_caller] translate the input information part returned by
diff --git a/src/plugins/pdg/pdg_state.ml b/src/plugins/pdg/pdg_state.ml
index 276f231efbe10bc51e0dd8891540a12b56feb943..b5c081a3438d810f876fa6b30fe4f949be98804e 100644
--- a/src/plugins/pdg/pdg_state.ml
+++ b/src/plugins/pdg/pdg_state.ml
@@ -29,6 +29,8 @@
let dkey = Pdg_parameters.register_category "state"
module P = Pdg_parameters
+
+open Pdg_types
open PdgTypes
exception Cannot_fold
diff --git a/src/plugins/pdg/pdg_state.mli b/src/plugins/pdg/pdg_state.mli
index a108bd99666eca31c374ce242e6a9c50e1a7134b..72f8297b41a2e8f42130aca2aed6dbe160cb99ce 100644
--- a/src/plugins/pdg/pdg_state.mli
+++ b/src/plugins/pdg/pdg_state.mli
@@ -22,6 +22,8 @@
exception Cannot_fold
+open Pdg_types
+
open PdgTypes
(** Types data_state and Node.t come froms this module *)
diff --git a/src/plugins/pdg/pdg_tbl.ml b/src/plugins/pdg/pdg_tbl.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5603732213786a2cc7020bd13272323edd35081c
--- /dev/null
+++ b/src/plugins/pdg/pdg_tbl.ml
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 Pdg_types
+
+type t = PdgTypes.Pdg.t
+
+(**************************************************************************)
+
+let compute = Build.compute_pdg
+
+module Tbl =
+ Kernel_function.Make_Table
+ (PdgTypes.Pdg)
+ (struct
+ let name = "Pdg.State"
+ let dependencies = [] (* postponed because !Db.From.self may
+ not exist yet *)
+ let size = 17
+ end)
+
+let self = Tbl.self
+let get = Tbl.memo compute
+
+(**************************************************************************)
+
+let pretty ?(bw=false) fmt pdg =
+ let kf = PdgTypes.Pdg.get_kf pdg in
+ Format.fprintf fmt "@[RESULT for %s:@]@\n@[ %a@]"
+ (Kernel_function.get_name kf) (PdgTypes.Pdg.pretty_bw ~bw) pdg
+
+let pretty_node short =
+ if short then PdgTypes.Node.pretty
+ else PdgTypes.Node.pretty_node
+
+let print_dot pdg filename =
+ PdgTypes.Pdg.build_dot filename pdg;
+ Pdg_parameters.feedback "dot file generated in %s" filename
+
+let pretty_key = PdgIndex.Key.pretty
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/pdg_tbl.mli b/src/plugins/pdg/pdg_tbl.mli
new file mode 100644
index 0000000000000000000000000000000000000000..541731a591138e8f100578e57827682b488da976
--- /dev/null
+++ b/src/plugins/pdg/pdg_tbl.mli
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 Pdg_types
+
+type t = PdgTypes.Pdg.t
+
+val self : State.t
+
+val get : Cil_types.kernel_function -> t
+(** Get the PDG of a function. Build it if it doesn't exist yet. *)
+
+(** {3 Pretty printing} *)
+
+val pretty_node : bool -> Format.formatter -> PdgTypes.Node.t -> unit
+(** Pretty print information on a node : with [short=true], only the id
+ of the node is printed.. *)
+
+val pretty_key : Format.formatter -> PdgIndex.Key.t -> unit
+(** Pretty print information on a node key *)
+
+val pretty : ?bw:bool -> Format.formatter -> t -> unit
+(** For debugging... Pretty print pdg information.
+ Print codependencies rather than dependencies if [bw=true]. *)
+
+val print_dot : t -> string -> unit
+(** Pretty print pdg into a dot file. *)
diff --git a/src/plugins/pdg/pdg_types/Pdg_types.ml b/src/plugins/pdg/pdg_types/Pdg_types.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a27209b47941a8551ffbe793be5f98d714307ea5
--- /dev/null
+++ b/src/plugins/pdg/pdg_types/Pdg_types.ml
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module PdgIndex = PdgIndex
+module PdgMarks = PdgMarks
+module PdgTypes = PdgTypes
diff --git a/src/plugins/pdg/pdg_types/Pdg_types.mli b/src/plugins/pdg/pdg_types/Pdg_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..edc3a0fd49034f42631a26719c9338ac75e292ce
--- /dev/null
+++ b/src/plugins/pdg/pdg_types/Pdg_types.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module PdgIndex: module type of PdgIndex
+module PdgMarks: module type of PdgMarks
+module PdgTypes: module type of PdgTypes
+
+(**************************************************************************)
diff --git a/src/plugins/pdg/pdg_types/dune b/src/plugins/pdg/pdg_types/dune
new file mode 100644
index 0000000000000000000000000000000000000000..722fae390011c23904d8646cfcfbd7e30f6c06e4
--- /dev/null
+++ b/src/plugins/pdg/pdg_types/dune
@@ -0,0 +1,40 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Pdg-Types:" %{lib-available:frama-c-pdg.types.core} "\n")
+ )
+ )
+)
+
+( library
+ (name Pdg_types)
+ (optional)
+ (public_name frama-c-pdg.types.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel)
+)
+
+(plugin (optional) (name pdg-types) (libraries frama-c-pdg.types.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg/pdg_types/frama-c-pdg-types.opam b/src/plugins/pdg/pdg_types/frama-c-pdg-types.opam
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/kernel_externals/pdg_types/pdgIndex.ml b/src/plugins/pdg/pdg_types/pdgIndex.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgIndex.ml
rename to src/plugins/pdg/pdg_types/pdgIndex.ml
diff --git a/src/kernel_externals/pdg_types/pdgIndex.mli b/src/plugins/pdg/pdg_types/pdgIndex.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgIndex.mli
rename to src/plugins/pdg/pdg_types/pdgIndex.mli
diff --git a/src/kernel_externals/pdg_types/pdgMarks.ml b/src/plugins/pdg/pdg_types/pdgMarks.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgMarks.ml
rename to src/plugins/pdg/pdg_types/pdgMarks.ml
diff --git a/src/kernel_externals/pdg_types/pdgMarks.mli b/src/plugins/pdg/pdg_types/pdgMarks.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgMarks.mli
rename to src/plugins/pdg/pdg_types/pdgMarks.mli
diff --git a/src/kernel_externals/pdg_types/pdgTypes.ml b/src/plugins/pdg/pdg_types/pdgTypes.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgTypes.ml
rename to src/plugins/pdg/pdg_types/pdgTypes.ml
diff --git a/src/kernel_externals/pdg_types/pdgTypes.mli b/src/plugins/pdg/pdg_types/pdgTypes.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgTypes.mli
rename to src/plugins/pdg/pdg_types/pdgTypes.mli
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 4f707e7ffeb43572c405893f74411acb98b2b560..8217fb8ccc0794e95ec2b72c7178730c50fa990c 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -20,104 +20,18 @@
(* *)
(**************************************************************************)
-let compute = Build.compute_pdg
-let pretty ?(bw=false) fmt pdg =
- let kf = PdgTypes.Pdg.get_kf pdg in
- Format.fprintf fmt "@[RESULT for %s:@]@\n@[ %a@]"
- (Kernel_function.get_name kf) (PdgTypes.Pdg.pretty_bw ~bw) pdg
+open Pdg_types
-let pretty_node short =
- if short then PdgTypes.Node.pretty
- else PdgTypes.Node.pretty_node
-
-let print_dot pdg filename =
- PdgTypes.Pdg.build_dot filename pdg;
- Pdg_parameters.feedback "dot file generated in %s" filename
-
-module Tbl =
- Kernel_function.Make_Table
- (PdgTypes.Pdg)
- (struct
- let name = "Pdg.State"
- let dependencies = [] (* postponed because !Db.From.self may
- not exist yet *)
- let size = 17
- end)
let () =
Cmdline.run_after_extended_stage
(fun () ->
State_dependency_graph.add_codependencies
- ~onto:Tbl.self
+ ~onto:Pdg_tbl.self
[ !Db.From.self ])
-(** Register external functions into Db. *)
-let () =
- Db.Pdg.self := Tbl.self;
- Db.Pdg.get := Tbl.memo compute;
- Db.Pdg.node_key := PdgTypes.Node.elem_key;
-
- Db.Pdg.find_decl_var_node := Sets.find_decl_var_node;
- Db.Pdg.find_entry_point_node := Sets.find_entry_point_node;
- Db.Pdg.find_top_input_node := Sets.find_top_input_node;
- Db.Pdg.find_simple_stmt_nodes := Sets.find_simple_stmt_nodes;
- Db.Pdg.find_stmt_and_blocks_nodes := Sets.find_stmt_and_blocks_nodes;
- Db.Pdg.find_stmt_node := Sets.find_stmt_node;
- Db.Pdg.find_label_node := Sets.find_label_node;
- Db.Pdg.find_location_nodes_at_stmt := Sets.find_location_nodes_at_stmt;
- Db.Pdg.find_location_nodes_at_begin := Sets.find_location_nodes_at_begin;
- Db.Pdg.find_location_nodes_at_end := Sets.find_location_nodes_at_end;
- Db.Pdg.find_call_ctrl_node := Sets.find_call_ctrl_node;
- Db.Pdg.find_call_input_node := Sets.find_call_num_input_node;
- Db.Pdg.find_call_output_node := Sets.find_call_output_node;
- Db.Pdg.find_input_node := Sets.find_input_node;
- Db.Pdg.find_ret_output_node := Sets.find_output_node;
- Db.Pdg.find_output_nodes := Sets.find_output_nodes;
- Db.Pdg.find_all_inputs_nodes := Sets.find_all_input_nodes;
-
- Db.Pdg.find_call_stmts := Sets.find_call_stmts;
-
- Db.Pdg.find_code_annot_nodes := Annot.find_code_annot_nodes;
- Db.Pdg.find_fun_precond_nodes := Annot.find_fun_precond_nodes;
- Db.Pdg.find_fun_postcond_nodes := Annot.find_fun_postcond_nodes;
-
- Db.Pdg.find_call_out_nodes_to_select := Sets.find_call_out_nodes_to_select;
- Db.Pdg.find_in_nodes_to_select_for_this_call :=
- Sets.find_in_nodes_to_select_for_this_call;
-
- Db.Pdg.direct_dpds := Sets.direct_dpds;
- Db.Pdg.direct_ctrl_dpds := Sets.direct_ctrl_dpds;
- Db.Pdg.direct_data_dpds := Sets.direct_data_dpds;
- Db.Pdg.direct_addr_dpds := Sets.direct_addr_dpds;
-
- Db.Pdg.all_dpds := Sets.find_nodes_all_dpds;
- Db.Pdg.all_ctrl_dpds := Sets.find_nodes_all_ctrl_dpds;
- Db.Pdg.all_data_dpds := Sets.find_nodes_all_data_dpds;
- Db.Pdg.all_addr_dpds := Sets.find_nodes_all_addr_dpds;
-
- Db.Pdg.direct_uses := Sets.direct_uses;
- Db.Pdg.direct_ctrl_uses := Sets.direct_ctrl_uses;
- Db.Pdg.direct_data_uses := Sets.direct_data_uses;
- Db.Pdg.direct_addr_uses := Sets.direct_addr_uses;
-
- Db.Pdg.all_uses := Sets.all_uses;
-
- Db.Pdg.custom_related_nodes := Sets.custom_related_nodes;
-
- Db.Pdg.iter_nodes := PdgTypes.Pdg.iter_nodes;
-
- Db.Pdg.pretty := pretty ;
- Db.Pdg.pretty_node := pretty_node ;
- Db.Pdg.pretty_key := PdgIndex.Key.pretty;
- Db.Pdg.extract := print_dot
-
-(* This module contains polymorphic functions : cannot be registered in Db.
- Can be used through Pdg.Register instead (see Pdg.mli) *)
-include Marks
-
-
let deps =
- [!Db.Pdg.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]
+ [Pdg_tbl.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]
let () = Pdg_parameters.BuildAll.set_output_dependencies deps
@@ -130,11 +44,11 @@ let compute () =
Eva.Analysis.compute ();
let do_kf_pdg kf =
if compute_for_kf kf then
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg_tbl.get kf in
let dot_basename = Pdg_parameters.DotBasename.get () in
if dot_basename <> "" then
let fname = Kernel_function.get_name kf in
- !Db.Pdg.extract pdg (dot_basename ^ "." ^ fname ^ ".dot")
+ Pdg_tbl.print_dot pdg (dot_basename ^ "." ^ fname ^ ".dot")
in
Callgraph.Uses.iter_in_rev_order do_kf_pdg;
let pp_sep fmt () = Format.pp_print_string fmt "," in
@@ -151,7 +65,7 @@ let output () =
let bw = Pdg_parameters.PrintBw.get () in
let do_kf_pdg kf =
if compute_for_kf kf then
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg_tbl.get kf in
let header fmt =
Format.fprintf fmt "PDG for %a" Kernel_function.pretty kf
in
diff --git a/src/plugins/pdg/register.mli b/src/plugins/pdg/register.mli
index a99bfbabb26f9923ead07b600345bf705b0b6757..a7f49285d2960e715b6059dcd0fbfc316c2c6360 100644
--- a/src/plugins/pdg/register.mli
+++ b/src/plugins/pdg/register.mli
@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
-include module type of Marks
+(* empty *)
diff --git a/src/plugins/pdg/sets.ml b/src/plugins/pdg/sets.ml
index 275477477b083ab80dca3d0e8df4ae8a95a30e96..846b30c2540db37082090965d0a76a07d422b553 100644
--- a/src/plugins/pdg/sets.ml
+++ b/src/plugins/pdg/sets.ml
@@ -23,6 +23,8 @@
(** Provides function to extract information from the PDG. *)
open Cil_types
+
+open Pdg_types
open PdgIndex
type nodes_and_undef =
diff --git a/src/plugins/pdg/sets.mli b/src/plugins/pdg/sets.mli
index a416d993e6975611bf9612afb1c25d71a28ee41d..27c12193321a174aad89fcd0e57f19643b355c6d 100644
--- a/src/plugins/pdg/sets.mli
+++ b/src/plugins/pdg/sets.mli
@@ -23,6 +23,7 @@
(** PDG (program dependence graph) access functions. *)
open Cil_types
+open Pdg_types
type nodes_and_undef =
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
diff --git a/src/plugins/postdominators/print.ml b/src/plugins/postdominators/print.ml
index 6ff5e94dd085ea9bafddbe2bd0a0f78f66928221..56e3d81e8ee858dcef7e14a2888dd4a7a516cf80 100644
--- a/src/plugins/postdominators/print.ml
+++ b/src/plugins/postdominators/print.ml
@@ -23,8 +23,7 @@
open Cil_types
open Cil_datatype
-let pretty_stmt fmt s =
- let key = PdgIndex.Key.stmt_key s in !Db.Pdg.pretty_key fmt key
+let pretty_stmt fmt s = Cil_printer.pp_stmt fmt s
module Printer = struct
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 2e7fbdbdf8694c5424314143013f4681865576b5..b7783e9f5e508440367136109324a5fb629805e9 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -27,6 +27,8 @@
open Cil_datatype
open Cil_types
+open Pdg_types
+
let debug1 fmt = Datascope.R.debug ~level:1 fmt
module Interproc =
@@ -60,19 +62,19 @@ let _pp_set prefix fmt =
let rec add_callee_nodes z acc nodes =
let new_nodes, acc = NSet.fold
(fun node acc2 ->
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| PdgIndex.Key.SigCallKey (cid, PdgIndex.Signature.Out out_key) ->
let callees = Eva.Results.callee (PdgIndex.Key.call_from_id cid) in
List.fold_left (fun (new_nodes, acc) kf ->
- let callee_pdg = !Db.Pdg.get kf in
+ let callee_pdg = Pdg.Api.get kf in
let outputs = match out_key with
| PdgIndex.Signature.OutLoc out ->
(* [out] might be an over-approximation of the location
we are searching for. We refine the search if needed. *)
let z = Locations.Zone.narrow out z in
- fst (!Db.Pdg.find_location_nodes_at_end callee_pdg z)
+ fst (Pdg.Api.find_location_nodes_at_end callee_pdg z)
| PdgIndex.Signature.OutRet -> (* probably never occurs *)
- fst (!Db.Pdg.find_output_nodes callee_pdg out_key)
+ fst (Pdg.Api.find_output_nodes callee_pdg out_key)
in
let outputs = List.map fst outputs in
add_list_to_set outputs new_nodes, add_list_to_set outputs acc)
@@ -99,25 +101,25 @@ let rec add_caller_nodes z kf acc (undef, nodes) =
| None -> acc_undef, acc
| Some undef ->
let nodes_for_undef, undef' =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before:true undef
+ Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before:true undef
in
let acc_undef = join_undef acc_undef undef' in
let acc = add_list_to_set (List.map fst nodes_for_undef) acc in
acc_undef, acc
in
let add_call_input_nodes node (acc_undef, acc) =
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| PdgIndex.Key.SigKey (PdgIndex.Signature.In in_key) ->
begin match in_key with
| PdgIndex.Signature.InCtrl ->
(* We only look for the values *)
acc_undef, acc
| PdgIndex.Signature.InNum n_param ->
- let n = !Db.Pdg.find_call_input_node pdg stmt n_param in
+ let n = Pdg.Api.find_call_input_node pdg stmt n_param in
acc_undef, NSet.add n acc
| PdgIndex.Signature.InImpl z' ->
let z = Locations.Zone.narrow z z' in
- let nodes, undef'= !Db.Pdg.find_location_nodes_at_stmt
+ let nodes, undef'= Pdg.Api.find_location_nodes_at_stmt
pdg stmt ~before:true z
in
let acc_undef = join_undef acc_undef undef' in
@@ -128,7 +130,7 @@ let rec add_caller_nodes z kf acc (undef, nodes) =
NSet.fold add_call_input_nodes nodes (acc_undef, acc)
in
let add_one_caller_nodes acc (kf, stmts) =
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let acc_undef, caller_nodes =
List.fold_left (add_one_call_nodes pdg) (None, NSet.empty) stmts
in add_caller_nodes z kf (NSet.union caller_nodes acc) (acc_undef, caller_nodes)
@@ -138,9 +140,9 @@ let compute_aux kf stmt zone =
debug1 "[Defs.compute] for %a at sid:%d in '%a'@."
Locations.Zone.pretty zone stmt.sid Kernel_function.pretty kf;
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before:true zone
+ Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before:true zone
in
let nodes = add_list_to_set (List.map fst nodes) NSet.empty in
let nodes =
@@ -152,13 +154,13 @@ let compute_aux kf stmt zone =
else nodes
in
Some (nodes, undef)
- with Db.Pdg.Bottom | Db.Pdg.Top | Not_found ->
+ with Pdg.Api.Bottom | Pdg.Api.Top | Not_found ->
None
let compute kf stmt lval =
let extract (nodes, undef) =
let add_node node defs =
- match PdgIndex.Key.stmt (!Db.Pdg.node_key node) with
+ match PdgIndex.Key.stmt (Pdg.Api.node_key node) with
| None -> defs
| Some s -> Stmt.Hptset.add s defs
in
@@ -185,7 +187,7 @@ let compute_with_def_type_zone kf stmt zone =
let after = (direct || prev_d, indirect || pred_i) in
Stmt.Map.add stmt after acc
in
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| PdgIndex.Key.Stmt s -> change s (true, false)
| PdgIndex.Key.CallStmt _ -> assert false
| PdgIndex.Key.SigCallKey (s, sign) ->
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index 95c81426d4f4e3e8411ac1a494d109152f432b38..82e4e62e6002f60ee6ee6b9267438cf6dd4e304e 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -27,6 +27,7 @@
(echo "Scope:" %{lib-available:frama-c-scope.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
(echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
)
)
)
@@ -36,7 +37,7 @@
(optional)
(public_name frama-c-scope.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core frama-c-pdg.core)
)
(plugin (optional) (name scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index aa02df158d8b3d246e59e501748f8fdf5dd3ae08..ba308e499fa2110d4aef18bbe2f29c18c890d9e8 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
module R = Datascope.R
let debug1 fmt = R.debug ~level:1 fmt
let debug2 fmt = R.debug ~level:2 fmt
@@ -262,7 +264,7 @@ let compute_ctrl_info pdg ctrl_part used_stmts =
let module CtrlCompute = Dataflow2.Backwards(CtrlComputer) in
let seen = Stmt.Hashtbl.create 50 in
let rec add_node_ctrl_nodes new_stmts node =
- let ctrl_nodes = !Db.Pdg.direct_ctrl_dpds pdg node in
+ let ctrl_nodes = Pdg.Api.direct_ctrl_dpds pdg node in
List.fold_left add_ctrl_node new_stmts ctrl_nodes
and add_ctrl_node new_stmts ctrl_node =
debug2 "[zones] add ctrl node %a@." PdgTypes.Node.pretty ctrl_node;
@@ -287,7 +289,7 @@ let compute_ctrl_info pdg ctrl_part used_stmts =
if Stmt.Hashtbl.mem seen stmt then new_stmts
else begin
Stmt.Hashtbl.add seen stmt ();
- match !Db.Pdg.find_simple_stmt_nodes pdg stmt with
+ match Pdg.Api.find_simple_stmt_nodes pdg stmt with
| [] -> []
| n::_ -> add_node_ctrl_nodes new_stmts n
end
@@ -323,7 +325,7 @@ let compute kf stmt lval =
let used_stmts = DataComputer.get_and_reset_used_stmts () in
let all_used_stmts =
if used_stmts = [] then []
- else compute_ctrl_info (!Db.Pdg.get kf) ctrl_part used_stmts
+ else compute_ctrl_info (Pdg.Api.get kf) ctrl_part used_stmts
in
let all_used_stmts =
List.fold_left
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 629fa05f3835588deac0848a4d24514a7f93b89f..e28a649eb889d5ade1e2af1bf5e0072e8607ad8b 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
(* ************************************************************************* *)
(** {2 Searching security annotations} *)
(* ************************************************************************* *)
@@ -98,7 +100,7 @@ let search_security_requirements () =
open PdgIndex
-let get_node_stmt node = Key.stmt (!Db.Pdg.node_key node)
+let get_node_stmt node = Key.stmt (Pdg.Api.node_key node)
module NodeKf = Datatype.Pair(PdgTypes.Node)(Kernel_function)
@@ -246,26 +248,26 @@ module Todolist : sig
type todo = private
{ node: PdgTypes.Node.t;
kf: kernel_function;
- pdg: Db.Pdg.t;
+ pdg: Pdg.Api.t;
callstack_length: int;
from_deep: bool }
type t = todo list
- val mk_init: kernel_function -> Db.Pdg.t -> PdgTypes.Node.t list -> todo list
+ val mk_init: kernel_function -> Pdg.Api.t -> PdgTypes.Node.t list -> todo list
val add:
- PdgTypes.Node.t -> kernel_function -> Db.Pdg.t -> int -> bool -> t -> t
+ PdgTypes.Node.t -> kernel_function -> Pdg.Api.t -> int -> bool -> t -> t
end = struct
type todo =
{ node: PdgTypes.Node.t;
kf: kernel_function;
- pdg: Db.Pdg.t;
+ pdg: Pdg.Api.t;
callstack_length: int;
from_deep: bool }
type t = todo list
let add n kf pdg len fd list =
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| Key.SigKey (Signature.In Signature.InCtrl) ->
(* do not consider node [InCtrl] *)
list
@@ -276,7 +278,7 @@ end = struct
list
| _ ->
Security_slicing_parameters.debug ~level:2 "adding node %a (in %s)"
- (!Db.Pdg.pretty_node false) n
+ (Pdg.Api.pretty_node false) n
(Kernel_function.get_name kf);
{ node = n; kf = kf; pdg = pdg;
callstack_length = len; from_deep = fd }
@@ -301,7 +303,7 @@ module Component = struct
| Forward of fwd_kind
type value =
- { pdg: Db.Pdg.t;
+ { pdg: Pdg.Api.t;
mutable callstack_length: int;
mutable direct: bool;
mutable indirect_backward: bool;
@@ -356,15 +358,15 @@ module Component = struct
(* do not consider address dependencies now (except for impact analysis):
just consider them during the last slicing pass
(for semantic preservation of pointers) *)
- let direct node = !Db.Pdg.direct_data_dpds pdg node in
+ let direct node = Pdg.Api.direct_data_dpds pdg node in
match kind with
| Direct -> direct node
- | Indirect_Backward -> direct node @ !Db.Pdg.direct_ctrl_dpds pdg node
+ | Indirect_Backward -> direct node @ Pdg.Api.direct_ctrl_dpds pdg node
| Forward Security ->
- !Db.Pdg.direct_data_uses pdg node @ !Db.Pdg.direct_ctrl_uses pdg node
+ Pdg.Api.direct_data_uses pdg node @ Pdg.Api.direct_ctrl_uses pdg node
| Forward Impact ->
- !Db.Pdg.direct_data_uses pdg node @ !Db.Pdg.direct_ctrl_uses pdg node
- @ !Db.Pdg.direct_addr_uses pdg node
+ Pdg.Api.direct_data_uses pdg node @ Pdg.Api.direct_ctrl_uses pdg node
+ @ Pdg.Api.direct_addr_uses pdg node
let search_input kind kf lazy_l =
try
@@ -378,18 +380,18 @@ module Component = struct
[]
let add_from_deep caller todo n =
- Todolist.add n caller (!Db.Pdg.get caller) 0 true todo
+ Todolist.add n caller (Pdg.Api.get caller) 0 true todo
let forward_caller kf node todolist =
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
List.fold_left
(fun todolist (caller, callsites) ->
(* foreach caller *)
List.fold_left
(fun todolist callsite ->
let nodes =
- !Db.Pdg.find_call_out_nodes_to_select
- pdg (PdgTypes.NodeSet.singleton node) (!Db.Pdg.get caller) callsite
+ Pdg.Api.find_call_out_nodes_to_select
+ pdg (PdgTypes.NodeSet.singleton node) (Pdg.Api.get caller) callsite
in
List.fold_left
(add_from_deep caller)
@@ -420,7 +422,7 @@ module Component = struct
end else begin
Security_slicing_parameters.debug
~level:2 "considering node %a (in %s)"
- (!Db.Pdg.pretty_node false) node
+ (Pdg.Api.pretty_node false) node
(Kernel_function.get_name kf);
(* intraprocedural related_nodes *)
let related_nodes = one_step_related_nodes kind pdg node in
@@ -448,7 +450,7 @@ module Component = struct
for zone %a@." (Kernel_function.get_name kf)
(Kernel_function.get_name caller)
Locations.Zone.pretty zone;*)
- let pdg_caller = !Db.Pdg.get caller in
+ let pdg_caller = Pdg.Api.get caller in
let do_call todolist callsite =
match kind with
| Direct | Indirect_Backward ->
@@ -465,13 +467,13 @@ module Component = struct
todolist
in
let todolist =
- match !Db.Pdg.node_key node with
+ match Pdg.Api.node_key node with
| Key.SigKey (Signature.In Signature.InCtrl) ->
assert false
| Key.SigKey (Signature.In (Signature.InImpl zone)) ->
let compute_nodes pdg_caller callsite =
let nodes, _undef_zone =
- !Db.Pdg.find_location_nodes_at_stmt
+ Pdg.Api.find_location_nodes_at_stmt
pdg_caller callsite ~before:true zone
(* TODO : use undef_zone (see FS#201)? *)
in
@@ -484,9 +486,9 @@ module Component = struct
let compute_nodes pdg_caller callsite =
[ match key with
| Signature.In (Signature.InNum n) ->
- !Db.Pdg.find_call_input_node pdg_caller callsite n
+ Pdg.Api.find_call_input_node pdg_caller callsite n
| Signature.Out Signature.OutRet ->
- !Db.Pdg.find_call_output_node pdg_caller callsite
+ Pdg.Api.find_call_output_node pdg_caller callsite
| Signature.In
(Signature.InCtrl | Signature.InImpl _)
| Signature.Out _ ->
@@ -511,14 +513,14 @@ module Component = struct
"[security] search inside %s (from %s)@."
(Kernel_function.get_name called_kf)
(Kernel_function.get_name kf);*)
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg.Api.get called_kf in
let nodes =
try
match kind, key with
| (Direct | Indirect_Backward),
Signature.Out out_key ->
let nodes, _undef_zone =
- !Db.Pdg.find_output_nodes called_pdg out_key
+ Pdg.Api.find_output_nodes called_pdg out_key
(* TODO: use undef_zone (see FS#201) *)
in
let nodes =
@@ -527,28 +529,28 @@ module Component = struct
nodes
| _, Signature.In (Signature.InNum n) ->
search_input kind called_kf
- (lazy [!Db.Pdg.find_input_node called_pdg n])
+ (lazy [Pdg.Api.find_input_node called_pdg n])
| _, Signature.In Signature.InCtrl ->
search_input kind called_kf
(lazy
- [!Db.Pdg.find_entry_point_node called_pdg])
+ [Pdg.Api.find_entry_point_node called_pdg])
| _, Signature.In (Signature.InImpl _) ->
assert false
| Forward _, Signature.Out _ ->
[]
with
- | Db.Pdg.Top ->
+ | Pdg.Api.Top ->
Security_slicing_parameters.warning
"no precise pdg for function %s. \n\
Ignoring this function in the analysis (potentially incorrect results)."
(Kernel_function.get_name called_kf);
[]
- | Db.Pdg.Bottom | Not_found -> assert false
+ | Pdg.Api.Bottom | Not_found -> assert false
in
List.fold_left
(fun todo n ->
(*Format.printf "node %a inside %s@."
- (!Db.Pdg.pretty_node false) n
+ (Pdg.Api.pretty_node false) n
(Kernel_function.get_name called_kf);*)
Todolist.add
n called_kf called_pdg
@@ -584,16 +586,16 @@ module Component = struct
let from_stmt = List.fold_left
(fun s n -> PdgTypes.NodeSet.add n s)
PdgTypes.NodeSet.empty from_stmt in
- let called_pdg = !Db.Pdg.get called_kf in
+ let called_pdg = Pdg.Api.get called_kf in
let nodes =
try
- !Db.Pdg.find_in_nodes_to_select_for_this_call
+ Pdg.Api.find_in_nodes_to_select_for_this_call
pdg from_stmt stmt called_pdg
with
- | Db.Pdg.Top ->
+ | Pdg.Api.Top ->
(* warning already emitted in the previous fold *)
[]
- | Db.Pdg.Bottom | Not_found -> assert false
+ | Pdg.Api.Bottom | Not_found -> assert false
in
List.fold_left
(fun todo n ->
@@ -623,10 +625,10 @@ module Component = struct
let initial_nodes kf stmt =
Security_slicing_parameters.debug
~level:3 "computing initial nodes for %d" stmt.sid;
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes =
if Eva.Results.is_reachable stmt then
- try !Db.Pdg.find_simple_stmt_nodes pdg stmt
+ try Pdg.Api.find_simple_stmt_nodes pdg stmt
with Not_found -> assert false
else begin
Security_slicing_parameters.debug
@@ -654,7 +656,7 @@ module Component = struct
nodes
in
res
- with Db.Pdg.Top | Db.Pdg.Bottom ->
+ with Pdg.Api.Top | Pdg.Api.Bottom ->
Security_slicing_parameters.warning "PDG is not manageable. skipping.";
M.empty
@@ -665,7 +667,7 @@ module Component = struct
Security_slicing_parameters.debug
"computing backward indirect component for %d" stmt.sid;
related_nodes_of_nodes Indirect_Backward res nodes
- with Db.Pdg.Top | Db.Pdg.Bottom ->
+ with Pdg.Api.Top | Pdg.Api.Bottom ->
Security_slicing_parameters.warning "PDG is not manageable. skipping.";
M.empty
@@ -855,7 +857,7 @@ let slice ctrl =
let slicing = !Slicing.Project.mk_project name in
let select (n, kf) sel =
Security_slicing_parameters.debug ~level:2 "selecting %a (of %s)"
- (!Db.Pdg.pretty_node false) n
+ (Pdg.Api.pretty_node false) n
(Kernel_function.get_name kf);
!Slicing.Select.select_pdg_nodes
sel
diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune
index 91009d8a81921bc390fd8964c6fdd617c764c233..4e24b20cfd4e2c6103fd71897dc204be5fe01bcb 100644
--- a/src/plugins/security_slicing/dune
+++ b/src/plugins/security_slicing/dune
@@ -26,6 +26,7 @@
(action (progn
(echo "Security Slicing:" %{lib-available:frama-c-security_slicing.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
)
)
)
@@ -35,7 +36,7 @@
(optional)
(public_name frama-c-security_slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-pdg.core)
)
(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index 2a0af61952fbb5e2b4ef8ed5550aed059a351773..c1b4b19a0d97e6391031f0fb39fb5ac64367937a 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -306,6 +306,8 @@ module Select : sig
(** {3 Pdg selectors.} *)
+ open Pdg_types
+
val select_pdg_nodes :
set -> Mark.t -> PdgTypes.Node.t list -> Cil_types.kernel_function -> set
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index b470412386a2539a15b5fd3c3b3fb857fa5de024..43be72e63ec8990bfab89552dde3857cebd463e6 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -41,6 +41,7 @@
(**/**)
open Cil_types
+open Pdg_types
(**/**)
(* Look at (only once) the callers of [kf] ([kf] included). *)
@@ -356,7 +357,7 @@ end = struct
let merge ff1 ff2 =
let pdg1, fm1 = ff1.SlicingInternals.ff_marks in
let pdg2, fm2 = ff2.SlicingInternals.ff_marks in
- assert (Db.Pdg.from_same_fun pdg1 pdg2) ;
+ assert (Pdg.Api.from_same_fun pdg1 pdg2) ;
let merge_marks m1 m2 = SlicingMarks.merge_marks [m1; m2] in
let merge_call_info _c1 _c2 = None in
let fm = PdgIndex.FctIndex.merge fm1 fm2 merge_marks merge_call_info in
@@ -418,7 +419,7 @@ end = struct
let m2m s m =
let key = match s with
| PdgMarks.SelIn loc -> PdgIndex.Key.implicit_in_key loc
- | PdgMarks.SelNode (n,_z) -> !Db.Pdg.node_key n
+ | PdgMarks.SelNode (n,_z) -> Pdg.Api.node_key n
in
let old_m = get_mark old_marks key in
let add_mark =
@@ -436,7 +437,7 @@ end = struct
SlicingParameters.debug ~level:2
"[Fct_Slice.FctMarks.marks_for_caller_inputs] for %a : \
old=%a new=%a -> %a"
- !Db.Pdg.pretty_key key SlicingMarks.pretty_mark old_m
+ Pdg.Api.pretty_key key SlicingMarks.pretty_mark old_m
SlicingMarks.pretty_mark m
SlicingMarks.pretty_mark
(match new_m with None -> SlicingMarks.bottom_mark | Some m -> m);
@@ -452,7 +453,7 @@ end = struct
None
in
let new_input_marks =
- Pdg.Register.in_marks_to_caller pdg_caller call m2m in_info in
+ Pdg.Marks.in_marks_to_caller pdg_caller call m2m in_info in
new_input_marks, !new_input
let marks_for_call_outputs (_, out_info) = out_info
@@ -467,7 +468,7 @@ end = struct
let pdg = SlicingMacros.get_ff_pdg ff_call in
let spare = SlicingMarks.mk_gen_spare in
let rec add2 marks n =
- match !Db.Pdg.node_key n with
+ match Pdg.Api.node_key n with
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.In _)) ->
marks
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.Out key)) ->
@@ -497,7 +498,7 @@ end = struct
* it has already been taken into account in the "from". *)
None
| PdgMarks.SelNode (n, _z_opt) ->
- let nkey = !Db.Pdg.node_key n in
+ let nkey = Pdg.Api.node_key n in
(*
let nkey = match z_opt with None -> nkey
| Some z -> match nkey with
@@ -516,7 +517,7 @@ end = struct
| _ -> (); false
in
SlicingParameters.debug ~level:2 "[Fct_Slice.FctMarks.check_called_marks] for %a : old=%a new=%a -> %a %s"
- !Db.Pdg.pretty_key nkey
+ Pdg.Api.pretty_key nkey
SlicingMarks.pretty_mark old_m
SlicingMarks.pretty_mark m
SlicingMarks.pretty_mark
@@ -524,7 +525,7 @@ end = struct
(if new_out then "(new out)" else "");
m_opt
in let new_called_marks =
- Pdg.Register.call_out_marks_to_called ff_pdg m2m new_call_marks
+ Pdg.Marks.call_out_marks_to_called ff_pdg m2m new_call_marks
in new_called_marks, !new_output
let persistent_in_marks_to_prop fi to_prop =
@@ -532,12 +533,12 @@ end = struct
SlicingParameters.debug ~level:2 "[Fct_Slice.FctMarks.persistent_in_marks_to_prop] from %s" (SlicingMacros.fi_name fi);
let m2m _call _pdg_caller _n m =
(* SlicingParameters.debug ~level:2 " in_m2m %a in %s ?@."
- PdgIndex.Key.pretty (!Db.Pdg.node_key n) (SlicingMacros.pdg_name pdg_caller); *)
+ PdgIndex.Key.pretty (Pdg.Api.node_key n) (SlicingMacros.pdg_name pdg_caller); *)
SlicingMarks.missing_input_mark ~call:SlicingMarks.bottom_mark ~called:m
in
let pdg = SlicingMacros.get_fi_pdg fi in
let pdg_node_marks =
- Pdg.Register.translate_in_marks pdg ~m2m in_info [] in
+ Pdg.Marks.translate_in_marks pdg ~m2m in_info [] in
pdg_node_marks
let get_new_marks ff nodes_marks =
@@ -546,13 +547,13 @@ end = struct
let nkey = match n with
| PdgMarks.SelNode (n, _z_opt) ->
(* TODO : something to do for z_opt ? *)
- !Db.Pdg.node_key n
+ Pdg.Api.node_key n
| PdgMarks.SelIn l -> PdgIndex.Key.implicit_in_key l
in
let oldm = get_mark fm nkey in
let newm = SlicingMarks.minus_marks m oldm in
(* Format.printf "get_new_marks for %a : old=%a new=%a -> %a@."
- !Db.Pdg.pretty_key nkey SlicingMarks.pretty_mark oldm
+ Pdg.Api.pretty_key nkey SlicingMarks.pretty_mark oldm
SlicingMarks.pretty_mark m SlicingMarks.pretty_mark newm; *)
if not (SlicingMarks.is_bottom_mark newm) then (n, newm)::acc else acc
in List.fold_left add_if_new [] nodes_marks
@@ -571,7 +572,7 @@ end = struct
let mark_spare_call_nodes ff call =
let pdg = SlicingMacros.get_ff_pdg ff in
- let nodes = !Db.Pdg.find_simple_stmt_nodes pdg call in
+ let nodes = Pdg.Api.find_simple_stmt_nodes pdg call in
mark_spare_nodes ff nodes
(** TODO :
@@ -587,8 +588,8 @@ end = struct
let rec check_in_params n params = match params with
| [] -> []
| _ :: params ->
- let node = !Db.Pdg.find_input_node pdg n in
- let dpds = !Db.Pdg.direct_dpds pdg node in
+ let node = Pdg.Api.find_input_node pdg n in
+ let dpds = Pdg.Api.direct_dpds pdg node in
let get_n_mark n = get_mark ff_marks (PdgTypes.Node.elem_key n) in
let dpds_marks = List.map get_n_mark dpds in
let m = SlicingMarks.inter_marks dpds_marks in
@@ -596,7 +597,7 @@ end = struct
if not (SlicingMarks.is_bottom_mark m) then begin
SlicingKernel.debug ~level:2
"[Fct_Slice.FctMarks.mark_visible_inputs] %a -> %a"
- (!Db.Pdg.pretty_node true) node SlicingMarks.pretty_mark m;
+ (Pdg.Api.pretty_node true) node SlicingMarks.pretty_mark m;
PdgMarks.add_node_to_select marks (node, None) m
end else
marks
@@ -609,15 +610,15 @@ end = struct
let mark_visible_output ff_marks =
let pdg, _ = ff_marks in
try
- let out_node = !Db.Pdg.find_ret_output_node pdg in
- let dpds = !Db.Pdg.direct_dpds pdg out_node in
+ let out_node = Pdg.Api.find_ret_output_node pdg in
+ let dpds = Pdg.Api.direct_dpds pdg out_node in
let get_n_mark n = get_mark ff_marks (PdgTypes.Node.elem_key n) in
let dpds_marks = List.map get_n_mark dpds in
let m = SlicingMarks.inter_marks dpds_marks in
if not (SlicingMarks.is_bottom_mark m) then begin
SlicingParameters.debug ~level:2
"[Fct_Slice.FctMarks.mark_visible_outputs] %a -> %a"
- (!Db.Pdg.pretty_node true) out_node SlicingMarks.pretty_mark m;
+ (Pdg.Api.pretty_node true) out_node SlicingMarks.pretty_mark m;
let select = PdgMarks.add_node_to_select [] (out_node, None) m in
let to_prop = mark_and_propagate ff_marks select in
assert (to_prop = PropMark.empty_to_prop); ()
@@ -634,10 +635,10 @@ end = struct
with PdgIndex.CallStatement -> assert false
with Not_found -> SlicingMarks.bottom_mark
in
- Format.fprintf fmt "%a : %a" (!Db.Pdg.pretty_node true) node
+ Format.fprintf fmt "%a : %a" (Pdg.Api.pretty_node true) node
SlicingMarks.pretty_mark m
in
- !Db.Pdg.iter_nodes print_node pdg
+ Pdg.Api.iter_nodes print_node pdg
let debug_marked_ff fmt ff =
Format.fprintf fmt "@[<hv>Print slice =@ %s@]" (SlicingMacros.ff_name ff);
@@ -663,7 +664,7 @@ let get_called_slice ff call =
let _pretty_node_marks fmt marks =
let print fmt (n, m) =
- (!Db.Pdg.pretty_node true) fmt n; SlicingMarks.pretty_mark fmt m
+ (Pdg.Api.pretty_node true) fmt n; SlicingMarks.pretty_mark fmt m
in
Format.fprintf fmt "%a" (fun fmt x -> List.iter (print fmt) x) marks
@@ -1000,7 +1001,7 @@ let get_call_in_nodes called_kf call_info called_in_zone =
let _, nodes, in_zone =
List.fold_left check_param (1, [], called_in_zone) param_list
in
- let impl_in_nodes, undef = !Db.Pdg.find_location_nodes_at_stmt
+ let impl_in_nodes, undef = Pdg.Api.find_location_nodes_at_stmt
pdg_caller call_stmt ~before:true in_zone
in (nodes @ impl_in_nodes), undef
@@ -1232,7 +1233,7 @@ let apply_missing_inputs ff call missing_inputs =
assert (not (SlicingMarks.is_bottom_mark m));
match sel with
| PdgMarks.SelNode (n, _)
- when (!Db.Pdg.node_key n = PdgIndex.Key.top_input) -> true
+ when (Pdg.Api.node_key n = PdgIndex.Key.top_input) -> true
| _ -> visible_top tl
in let is_top_visible = visible_top input_marks in
*)
diff --git a/src/plugins/slicing/fct_slice.mli b/src/plugins/slicing/fct_slice.mli
index 6ea3a114edbdc847d41731dc0d04e4ec1dd20157..a6dd86470f6aa83f972912dad981089fbfeb2468 100644
--- a/src/plugins/slicing/fct_slice.mli
+++ b/src/plugins/slicing/fct_slice.mli
@@ -23,6 +23,8 @@
open SlicingInternals
open Cil_types
+open Pdg_types
+
(** Return [true] if the source function is called
* (even indirectly via transitivity) from a [Slice.t]. *)
val is_src_fun_called :
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index faa275ee37bf95e7489066f89220042821c4e219..535e841b34be8791091c1f102f0074fafb09fa86 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -26,6 +26,8 @@
open Cil_types
+open Pdg_types
+
(**/**)
let find_sub_stmts st = match st.skind with
@@ -334,7 +336,7 @@ let build_dot_project filename title =
let print_fct_stmts fmt kf =
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
print_fct_from_pdg fmt pdg;
Format.pp_print_flush fmt ()
with Not_found -> ()
diff --git a/src/plugins/slicing/printSlice.mli b/src/plugins/slicing/printSlice.mli
index dbf55bac1d788e64a6a64727a937478b5402a153..f3ad3570b12b39cc771b39339d2277b03384d5ba 100644
--- a/src/plugins/slicing/printSlice.mli
+++ b/src/plugins/slicing/printSlice.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val print_fct_from_pdg :
Format.formatter ->
?ff:SlicingInternals.fct_slice -> PdgTypes.Pdg.t -> unit
diff --git a/src/plugins/slicing/slicingActions.ml b/src/plugins/slicing/slicingActions.ml
index 3529e42201527f028e136480bc7018d6c08d738a..0f8410e0446c633e8f855b3425c5993cfa613999 100644
--- a/src/plugins/slicing/slicingActions.ml
+++ b/src/plugins/slicing/slicingActions.ml
@@ -27,6 +27,8 @@
(**/**)
+open Pdg_types
+
type select = SlicingTypes.sl_mark PdgMarks.select
type n_or_d_marks = (SlicingInternals.node_or_dpds * SlicingInternals.pdg_mark) list
@@ -156,10 +158,10 @@ let mk_appli_select_calls fi = SlicingInternals.CrAppli (SlicingInternals.CaCall
let mk_crit_mark_calls fi_caller to_call mark =
let select = try
let caller = SlicingMacros.get_fi_kf fi_caller in
- let pdg_caller = !Db.Pdg.get caller in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller to_call in
+ let pdg_caller = Pdg.Api.get caller in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller to_call in
let stmt_mark stmt =
- let stmt_ctrl_node = !Db.Pdg.find_call_ctrl_node pdg_caller stmt in
+ let stmt_ctrl_node = Pdg.Api.find_call_ctrl_node pdg_caller stmt in
(PdgMarks.mk_select_node stmt_ctrl_node, mark)
in
let select = List.map stmt_mark call_stmts in
@@ -182,7 +184,7 @@ let mk_crit_add_output_marks ff select =
(*
let mk_crit_add_all_outputs_mark ff mark =
let pdg = SlicingMacros.get_ff_pdg ff in
- let nodes = !Db.Pdg.find_all_outputs_nodes pdg in
+ let nodes = Pdg.Api.find_all_outputs_nodes pdg in
let nd_m = build_simple_node_selection mark in
let select = mk_mark_nodes nodes nd_m in
mk_ff_user_crit ff select
@@ -206,7 +208,7 @@ let rec print_nd_and_mark_list fmt ndm_list =
print_nd_and_mark fmt x; print_nd_and_mark_list fmt ndm_list
let print_nodes fmt nodes =
- let print n = Format.fprintf fmt "%a " (!Db.Pdg.pretty_node true) n in
+ let print n = Format.fprintf fmt "%a " (Pdg.Api.pretty_node true) n in
List.iter print nodes
let print_node_mark fmt n z m =
diff --git a/src/plugins/slicing/slicingActions.mli b/src/plugins/slicing/slicingActions.mli
index 975252aaa930ef6d2fe39aa93fe626a20a5c655a..081e5bbb6822e1adb85919bfc86037cb7b9a62f6 100644
--- a/src/plugins/slicing/slicingActions.mli
+++ b/src/plugins/slicing/slicingActions.mli
@@ -22,6 +22,9 @@
open SlicingTypes
open Cil_types
+
+open Pdg_types
+
open SlicingInternals
type select = sl_mark PdgMarks.select
@@ -43,7 +46,7 @@ val build_node_and_dpds_selection :
?nd_marks:n_or_d_marks -> sl_mark -> n_or_d_marks
val translate_crit_to_select :
- Db.Pdg.t -> ?to_select:select ->
+ Pdg.Api.t -> ?to_select:select ->
((PdgTypes.Node.t * Locations.Zone.t option) list * n_or_d_marks) list
-> select
diff --git a/src/plugins/slicing/slicingCmds.mli b/src/plugins/slicing/slicingCmds.mli
index a54c67ba31adc7806433769f1d1ca5cb56d70666..693aa337f1c05aa23fbf27b9680e3a132ab2c66b 100644
--- a/src/plugins/slicing/slicingCmds.mli
+++ b/src/plugins/slicing/slicingCmds.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
(* TODO: This .mli exists mainly to avoid problems with 'make -j'. This API
is too vast and must be simplified. For example, functions should not
receive variables as names (ie. strings) but directly as zones, possibly
diff --git a/src/plugins/slicing/slicingInternals.ml b/src/plugins/slicing/slicingInternals.ml
index 4169f6937d3d208c157d24e958faf9d96b4aea93..df18b5d589c2cbff6be1b02017156f92ce4478fa 100644
--- a/src/plugins/slicing/slicingInternals.ml
+++ b/src/plugins/slicing/slicingInternals.ml
@@ -27,6 +27,8 @@
open Cil_datatype
+open Pdg_types
+
(** {3 About options} *)
(** associate a level to each function in order to control how it will be
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
index 0e6dc51a49ccfd353bbe3d0e3c6729e68a48eb96..2c7de6f72a77653826a563428b842f379e2d204c 100644
--- a/src/plugins/slicing/slicingInternals.mli
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -27,6 +27,8 @@
open Cil_datatype
+open Pdg_types
+
(** {3 About options} *)
(** associate a level to each function in order to control how it will be
diff --git a/src/plugins/slicing/slicingMacros.ml b/src/plugins/slicing/slicingMacros.ml
index d221c7299c34279593def3da2e49322dd59c3e88..56dc2b438bd9b2024a9d642932e6aef85e96230b 100644
--- a/src/plugins/slicing/slicingMacros.ml
+++ b/src/plugins/slicing/slicingMacros.ml
@@ -28,6 +28,8 @@
open Cil_types
+open Pdg_types
+
(**/**)
(** {2 Options} *)
@@ -127,7 +129,7 @@ let get_pdg_kf pdg = PdgTypes.Pdg.get_kf pdg
(** {4 getting PDG} *)
-let get_fi_pdg fi = let kf = get_fi_kf fi in !Db.Pdg.get kf
+let get_fi_pdg fi = let kf = get_fi_kf fi in Pdg.Api.get kf
let get_ff_pdg ff = get_fi_pdg ff.SlicingInternals.ff_fct
diff --git a/src/plugins/slicing/slicingMacros.mli b/src/plugins/slicing/slicingMacros.mli
index 04e20ee753e5287e06af6884d83120043d6c562b..427b60450b8ccffe98994cb4c62dac41866746a0 100644
--- a/src/plugins/slicing/slicingMacros.mli
+++ b/src/plugins/slicing/slicingMacros.mli
@@ -24,6 +24,8 @@
functions below should be inlined, as there is no good reason to treat
those types as semi-private *)
+open Pdg_types
+
open SlicingInternals
val str_level_option : level_option -> string
@@ -40,8 +42,8 @@ val ff_src_name : fct_slice -> string
val get_fi_kf : fct_info -> Cil_types.kernel_function
val get_ff_kf : fct_slice -> Cil_types.kernel_function
val get_pdg_kf : PdgTypes.Pdg.t -> Kernel_function.t
-val get_fi_pdg : fct_info -> Db.Pdg.t
-val get_ff_pdg : fct_slice -> Db.Pdg.t
+val get_fi_pdg : fct_info -> Pdg.Api.t
+val get_ff_pdg : fct_slice -> Pdg.Api.t
val ff_slicing_level : fct_slice -> level_option
val change_fi_slicing_level : fct_info -> level_option -> unit
val change_slicing_level : Kernel_function.t -> int -> unit
diff --git a/src/plugins/slicing/slicingMarks.ml b/src/plugins/slicing/slicingMarks.ml
index d32603122c23f6479a4139c1d7f4194016ba25ca..77e2c60002dc6e95b15e94a4df90e970610dc68b 100644
--- a/src/plugins/slicing/slicingMarks.ml
+++ b/src/plugins/slicing/slicingMarks.ml
@@ -22,6 +22,8 @@
(** Everything related with the marks. Mainly quite low level function. *)
+open Pdg_types
+
(**/**)
let debug = false
diff --git a/src/plugins/slicing/slicingMarks.mli b/src/plugins/slicing/slicingMarks.mli
index d398c3967fdaec9c47b1e2aa9a4cbd5fc79a47af..fd4505c96de75d7990f83b99007cd56f8c7f1894 100644
--- a/src/plugins/slicing/slicingMarks.mli
+++ b/src/plugins/slicing/slicingMarks.mli
@@ -22,6 +22,8 @@
open SlicingTypes
+open Pdg_types
+
val bottom_mark : sl_mark
val mk_user_mark : data:bool -> addr:bool -> ctrl:bool -> sl_mark
diff --git a/src/plugins/slicing/slicingProject.ml b/src/plugins/slicing/slicingProject.ml
index 27cca02339737ad74f510c4dfec8679ccc6b8a34..70ee325043535f43c8ae87624cf22f940addbc75 100644
--- a/src/plugins/slicing/slicingProject.ml
+++ b/src/plugins/slicing/slicingProject.ml
@@ -24,6 +24,8 @@
(**/**)
+open Pdg_types
+
module T = SlicingInternals
module M = SlicingMacros
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 25b922ab7f417778765b40c4bc8eeb43efc48ae6..cf279d65247463b02cf17fc8c0155f90ea46b625 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
(* ---------------------------------------------------------------------- *)
(** {1 For internal use} *)
@@ -72,7 +74,7 @@ let basic_add_select kf select nodes ?(undef) nd_marks =
match sel with
| SlicingInternals.CuTop _ -> select
| SlicingInternals.CuSelect sel ->
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes =
List.map (fun n -> (n, None) (*TODO: add z_part ? *)) nodes in
(* let nd_marks = SlicingActions.build_node_and_dpds_selection mark in *)
@@ -89,7 +91,7 @@ let select_pdg_nodes kf ?(select=empty_db_select kf) nodes mark =
SlicingParameters.debug ~level:1 "[Register.select_pdg_nodes]" ;
let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
try basic_add_select kf select nodes nd_marks
- with Db.Pdg.Top | Db.Pdg.Bottom ->
+ with Pdg.Api.Top | Pdg.Api.Bottom ->
assert false (* if we have node, we must have a pdg somewhere ! *)
let mk_select pdg sel nodes undef mark =
@@ -120,9 +122,9 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
| SlicingInternals.CuTop _ -> select
| SlicingInternals.CuSelect sel ->
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before loc in
+ Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before loc in
let sel = mk_select pdg sel nodes undef mark in
(fvar, sel)
with
@@ -138,8 +140,8 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
(if before then "before" else "after") stmt.sid
Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
(** this one is similar to [select_stmt_zone] with the return statement
@@ -154,10 +156,10 @@ let select_in_out_zone ~at_end ~use_undef kf select loc mark =
| SlicingInternals.CuTop _ -> select
| SlicingInternals.CuSelect sel ->
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let find =
- if at_end then !Db.Pdg.find_location_nodes_at_end
- else !Db.Pdg.find_location_nodes_at_begin in
+ if at_end then Pdg.Api.find_location_nodes_at_end
+ else Pdg.Api.find_location_nodes_at_begin in
let nodes, undef = find pdg loc in
let undef = if use_undef then undef else None in
let sel = mk_select pdg sel nodes undef mark in
@@ -169,8 +171,8 @@ let select_in_out_zone ~at_end ~use_undef kf select loc mark =
Locations.Zone.pretty loc SlicingMarks.pretty_mark mark
(if at_end then "end" else "begin") Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
let select_zone_at_end kf ?(select=empty_db_select kf) loc mark =
select_in_out_zone ~at_end:true ~use_undef:true kf select loc mark
@@ -183,9 +185,9 @@ let select_zone_at_entry kf ?(select=empty_db_select kf) loc mark =
let stmt_nodes_to_select pdg stmt =
try
- let stmt_nodes = !Db.Pdg.find_stmt_and_blocks_nodes pdg stmt in
+ let stmt_nodes = Pdg.Api.find_stmt_and_blocks_nodes pdg stmt in
SlicingParameters.debug ~level:2 "[Register.stmt_nodes_to_select] results on stmt %d (%a)" stmt.sid
- (fun fmt l -> List.iter (!Db.Pdg.pretty_node true fmt) l)
+ (fun fmt l -> List.iter (Pdg.Api.pretty_node true fmt) l)
stmt_nodes;
stmt_nodes
with Not_found ->
@@ -203,23 +205,23 @@ let select_stmt_computation kf ?(select=empty_db_select kf) stmt mark =
end
else
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let stmt_nodes = stmt_nodes_to_select pdg stmt in
let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
basic_add_select kf select stmt_nodes nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
let select_label kf ?(select=empty_db_select kf) label mark =
SlicingParameters.debug ~level:1 "[Register.select_label] on label "
(* Logic_label.pretty label *);
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let nodes =
let add_label_nodes l acc = match l with
| StmtLabel stmt ->
let add acc l =
- try !Db.Pdg.find_label_node pdg !stmt l :: acc
+ try Pdg.Api.find_label_node pdg !stmt l :: acc
with Not_found -> acc
in
List.fold_left add acc (!stmt).labels
@@ -230,8 +232,8 @@ let select_label kf ?(select=empty_db_select kf) label mark =
in
let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
basic_add_select kf select nodes nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; select
(** marking a call node means that a [choose_call] will have to decide that to
* call according to the slicing-level, but anyway, the call will be visible.
@@ -239,42 +241,42 @@ let select_label kf ?(select=empty_db_select kf) label mark =
let select_minimal_call kf ?(select=empty_db_select kf) stmt m =
SlicingParameters.debug ~level:1 "[Register.select_minimal_call]";
try
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
let call = check_call stmt true in
- let call_node = !Db.Pdg.find_call_ctrl_node pdg call in
+ let call_node = Pdg.Api.find_call_ctrl_node pdg call in
let nd_marks = SlicingActions.build_simple_node_selection m in
basic_add_select kf select [call_node] nd_marks
- with Db.Pdg.Top -> top_db_select kf m
- | Db.Pdg.Bottom -> bottom_msg kf; select
+ with Pdg.Api.Top -> top_db_select kf m
+ | Pdg.Api.Bottom -> bottom_msg kf; select
let select_stmt_ctrl kf ?(select=empty_db_select kf) stmt =
SlicingParameters.debug ~level:1 "[Register.select_stmt_ctrl] of sid:%d" stmt.sid;
let mark = SlicingMarks.mk_user_mark ~ctrl:true ~data:false ~addr:false in
try
- let pdg = !Db.Pdg.get kf in
- let stmt_nodes = !Db.Pdg.find_simple_stmt_nodes pdg stmt in
+ let pdg = Pdg.Api.get kf in
+ let stmt_nodes = Pdg.Api.find_simple_stmt_nodes pdg stmt in
let nd_marks = SlicingActions.build_ctrl_dpds_selection mark in
basic_add_select kf select stmt_nodes nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let select_entry_point kf ?(select=empty_db_select kf) mark =
SlicingParameters.debug ~level:1 "[Register.select_entry_point] of %a"
Kernel_function.pretty kf;
try
- let pdg = !Db.Pdg.get kf in
- let node = !Db.Pdg.find_entry_point_node pdg in
+ let pdg = Pdg.Api.get kf in
+ let node = Pdg.Api.find_entry_point_node pdg in
let nd_marks = SlicingActions.build_simple_node_selection mark in
basic_add_select kf select [node] nd_marks
- with Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ with Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let select_return kf ?(select=empty_db_select kf) mark =
SlicingParameters.debug ~level:1 "[Register.select_return] of %a"
Kernel_function.pretty kf;
try
- let pdg = !Db.Pdg.get kf in
- let node = !Db.Pdg.find_ret_output_node pdg in
+ let pdg = Pdg.Api.get kf in
+ let node = Pdg.Api.find_ret_output_node pdg in
let nd_marks = SlicingActions.build_simple_node_selection mark in
basic_add_select kf select [node] nd_marks
with
@@ -283,8 +285,8 @@ let select_return kf ?(select=empty_db_select kf) mark =
"@[Nothing to select for return stmt of %a@]"
Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let select_decl_var kf ?(select=empty_db_select kf) vi mark =
SlicingParameters.debug ~level:1 "[Register.select_decl_var] of %s in %a@."
@@ -292,8 +294,8 @@ let select_decl_var kf ?(select=empty_db_select kf) vi mark =
if vi.Cil_types.vglob (* no slicing request on globals *)
then select
else try
- let pdg = !Db.Pdg.get kf in
- let node = !Db.Pdg.find_decl_var_node pdg vi in
+ let pdg = Pdg.Api.get kf in
+ let node = Pdg.Api.find_decl_var_node pdg vi in
let nd_marks = SlicingActions.build_simple_node_selection mark in
basic_add_select kf select [node] nd_marks
with
@@ -302,8 +304,8 @@ let select_decl_var kf ?(select=empty_db_select kf) vi mark =
"@[Nothing to select for %s declarationin %a@]"
vi.Cil_types.vname Kernel_function.pretty kf;
select
- | Db.Pdg.Top -> top_db_select kf mark
- | Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
+ | Pdg.Api.Top -> top_db_select kf mark
+ | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf
let merge_select select1 select2 =
@@ -351,7 +353,7 @@ let add_crit_ff_change_call ff_caller call f_to_call =
let call_ff_in_caller ~caller ~to_call =
let kf_caller = SlicingMacros.get_ff_kf caller in
let kf_to_call = SlicingMacros.get_ff_kf to_call in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller kf_to_call in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller kf_to_call in
let ff_to_call = SlicingInternals.CallSlice to_call in
let add_change_call stmt =
add_crit_ff_change_call caller stmt ff_to_call ;
@@ -367,7 +369,7 @@ let call_fsrc_in_caller ~caller ~to_call =
let kf_caller = SlicingMacros.get_ff_kf caller in
let fi_to_call = SlicingMacros.get_kf_fi to_call in
let kf_to_call = SlicingMacros.get_fi_kf fi_to_call in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller kf_to_call in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller kf_to_call in
let add_change_call stmt =
add_crit_ff_change_call caller stmt (SlicingInternals.CallSrc (Some fi_to_call))
in List.iter add_change_call call_stmts
@@ -375,9 +377,9 @@ let call_fsrc_in_caller ~caller ~to_call =
let call_min_f_in_caller ~caller ~to_call =
let kf_caller = SlicingMacros.get_ff_kf caller in
let pdg = SlicingMacros.get_ff_pdg caller in
- let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller to_call in
+ let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller to_call in
let call_nodes =
- List.map (fun call -> (!Db.Pdg.find_call_ctrl_node pdg call),None)
+ List.map (fun call -> (Pdg.Api.find_call_ctrl_node pdg call),None)
call_stmts in
let m = SlicingMarks.mk_user_spare in
let nd_marks = SlicingActions.build_simple_node_selection m in
@@ -389,7 +391,7 @@ let is_already_selected ff db_select =
match select with
| SlicingInternals.CuTop _ -> assert false
| SlicingInternals.CuSelect to_select ->
- (* let pdg = !Db.Pdg.get (Globals.Functions.get fvar) in *)
+ (* let pdg = Pdg.Api.get (Globals.Functions.get fvar) in *)
let new_marks = Fct_slice.filter_already_in ff to_select in
let ok = if new_marks = [] then true else false in
if ok then
diff --git a/src/plugins/slicing/slicingSelect.mli b/src/plugins/slicing/slicingSelect.mli
index c139085e9da9b6f5dd0b7925a88397f5e229405c..f68618af4ab69e2871793680ace383a3a673be89 100644
--- a/src/plugins/slicing/slicingSelect.mli
+++ b/src/plugins/slicing/slicingSelect.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select :
@@ -69,7 +71,7 @@ val select_pdg_nodes :
SlicingTypes.sl_select
val mk_select :
- Db.Pdg.t ->
+ Pdg.Api.t ->
SlicingActions.select ->
(PdgTypes.Node.t * Locations.Zone.t option) list ->
Locations.Zone.t option ->
@@ -117,7 +119,7 @@ val select_zone_at_entry :
SlicingTypes.sl_select
val stmt_nodes_to_select :
- Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
+ Pdg.Api.t -> Cil_types.stmt -> PdgTypes.Node.t list
val select_stmt_computation :
Kernel_function.t ->
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index b51f528fe8b7d7427b7fa06fd95ecb42f94040ca..28991d806423a6408dc7202d49476160cb0c7373 100644
--- a/src/plugins/slicing/slicingState.ml
+++ b/src/plugins/slicing/slicingState.ml
@@ -34,7 +34,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:self
- [ !Db.Pdg.self; !Db.Inputs.self_external; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; !Db.Inputs.self_external; !Db.Outputs.self_external ])
let get () =
try P.get ()
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index 5d7b4d1c5282e14d1fcfe0777d92e5d020051606..2915223eec08c36ed39b517038169b951525e899 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -26,6 +26,8 @@
open Cil_types
open Cil
+open Pdg_types
+
(**/**)
module Visibility (SliceName : sig
@@ -138,7 +140,7 @@ module Visibility (SliceName : sig
begin
SlicingParameters.debug ~level:3
"[SlicingTransform.Visibility.all_nodes_visible] node %a invisible"
- (!Db.Pdg.pretty_node true) n;
+ (Pdg.Api.pretty_node true) n;
false
end
else visi
@@ -173,7 +175,7 @@ module Visibility (SliceName : sig
SlicingParameters.debug ~level:2
"[SlicingTransform.Visibility.data_nodes_visible]@\n\
node %a invisible"
- (!Db.Pdg.pretty_node true) n;
+ (Pdg.Api.pretty_node true) n;
false
end
else visi
@@ -242,10 +244,10 @@ module Visibility (SliceName : sig
| Iproto -> false
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
let ctrl_nodes, decl_nodes, data_info =
- !Db.Pdg.find_code_annot_nodes pdg stmt annot
+ Pdg.Api.find_code_annot_nodes pdg stmt annot
in
let data_visible = data_nodes_visible ff (decl_nodes, data_info) in
let visible = ((all_nodes_visible ff ctrl_nodes) && data_visible) in
@@ -276,9 +278,9 @@ module Visibility (SliceName : sig
| Iproto -> true
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
- let nodes = !Db.Pdg.find_fun_precond_nodes pdg p in
+ let nodes = Pdg.Api.find_fun_precond_nodes pdg p in
data_nodes_visible ff nodes
with NoDataInfo ->
all_logic_var_visible ff p
@@ -296,9 +298,9 @@ module Visibility (SliceName : sig
| Iproto -> true
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
- let nodes = !Db.Pdg.find_fun_postcond_nodes pdg p in
+ let nodes = Pdg.Api.find_fun_postcond_nodes pdg p in
data_nodes_visible ff nodes
with NoDataInfo -> all_logic_var_visible ff p
@@ -316,9 +318,9 @@ module Visibility (SliceName : sig
| Iproto -> true
| Iff {slice = ff} ->
let kf = SlicingMacros.get_ff_kf ff in
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
try
- let nodes = !Db.Pdg.find_fun_variant_nodes pdg v in
+ let nodes = Pdg.Api.find_fun_variant_nodes pdg v in
data_nodes_visible ff nodes
with NoDataInfo -> all_logic_var_visible_term ff v
in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fun_variant_visible] -> %s"
diff --git a/src/plugins/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index 343d08a8f13a70053957f7cbb3de2133a0394a8c..e370df2269d2401259075c7ed22268b86ea5f6a2 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -22,6 +22,8 @@
(** Slicing module types. *)
+open Pdg_types
+
exception Slicing_Internal_Error of string
exception ChangeCallErr of string
exception PtrCallExpr
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 860f24fa634864535634f4222a038748df3e161c..7db1fca385b380e152d9e8889c5e2af06be6a8e9 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -160,7 +160,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ !Db.Pdg.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; !Db.Outputs.self_external ])
let rm_unused_decl =
Result.memo
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index b684d758b6bc1fcc216d63385568821a4f334c92..3ac3e1d4ccbea47722282482cdfd82e826cba46f 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -43,7 +43,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ !Db.Pdg.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; !Db.Outputs.self_external ])
module P = Sparecode_params
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index 2f0c83674a97d3f143b99a5c84ed36342cbb6ae6..bc433062ccc8929f0be579864f7878a07a6f8cee 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -20,12 +20,14 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
let debug n format = Sparecode_params.debug ~level:n format
let fatal fmt = Sparecode_params.fatal fmt
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** The project is composed of [FctIndex] marked with [BoolMark]
- * to be used by [Pdg.Register.F_Proj], and another table to store if a function
+ * to be used by [Pdg.Api.Marks.F_Proj], and another table to store if a function
* is visible (useful for Top PDG). *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
@@ -122,7 +124,7 @@ module Config = struct
end
-module ProjBoolMarks = Pdg.Register.F_Proj (Config)
+module ProjBoolMarks = Pdg.Api.Marks.F_Proj (Config)
type proj = ProjBoolMarks.t * unit KfTopVisi.t
type fct = ProjBoolMarks.fct
@@ -172,7 +174,7 @@ let rec add_pdg_selection to_select pdg sel_mark = match to_select with
| [] ->
let l = match sel_mark with None -> [] | Some m -> [m] in [(pdg, l)]
| (p, ln) :: tl ->
- if Db.Pdg.from_same_fun p pdg
+ if Pdg.Api.from_same_fun p pdg
then
let ln = match sel_mark with None -> ln
| Some sel_mark -> sel_mark::ln
@@ -273,7 +275,7 @@ let rec process_call_inputs proj =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let select_entry_point proj _kf pdg =
- let ctrl = !Db.Pdg.find_entry_point_node pdg in
+ let ctrl = Pdg.Api.find_entry_point_node pdg in
let to_select = add_node_to_select true [] None ctrl in
select_pdg_elements proj pdg to_select
@@ -281,9 +283,9 @@ let select_all_outputs proj kf pdg =
let outputs = !Db.Outputs.get_external kf in
debug 1 "@[selecting output zones %a@]" Locations.Zone.pretty outputs;
try
- let nodes, undef = !Db.Pdg.find_location_nodes_at_end pdg outputs in
+ let nodes, undef = Pdg.Api.find_location_nodes_at_end pdg outputs in
let nodes =
- try ((!Db.Pdg.find_ret_output_node pdg),None) :: nodes
+ try ((Pdg.Api.find_ret_output_node pdg),None) :: nodes
with Not_found -> nodes
in
let nodes_and_co = ([], [], Some (nodes, undef)) in
@@ -308,7 +310,7 @@ class annot_visitor ~filter pdg = object (self)
let stmt = Option.get self#current_stmt in
debug 1 "selecting annotation : %a @."
Printer.pp_code_annotation annot;
- let info = !Db.Pdg.find_code_annot_nodes pdg stmt annot in
+ let info = Pdg.Api.find_code_annot_nodes pdg stmt annot in
to_select <- add_nodes_and_undef_to_select true info to_select
with
Not_found -> () (* unreachable *)
@@ -322,7 +324,7 @@ end
let select_annotations ~select_annot ~select_slice_pragma proj =
let visit_fun kf =
debug 1 "look for annotations in function %a@." Kernel_function.pretty kf;
- let pdg = !Db.Pdg.get kf in
+ let pdg = Pdg.Api.get kf in
if PdgTypes.Pdg.is_top pdg then debug 1 "pdg top: skip annotations"
else if PdgTypes.Pdg.is_bottom pdg
then debug 1 "pdg bottom: skip annotations"
@@ -357,7 +359,7 @@ let select_useful_things ~select_annot ~select_slice_pragma kf_entry =
assert (!call_in_to_check = []);
debug 1 "selecting function %a outputs and entry point@."
Kernel_function.pretty kf_entry;
- let pdg = !Db.Pdg.get kf_entry in
+ let pdg = Pdg.Api.get kf_entry in
if PdgTypes.Pdg.is_top pdg
then KfTopVisi.set proj kf_entry
else if PdgTypes.Pdg.is_bottom pdg
diff --git a/src/plugins/sparecode/spare_marks.mli b/src/plugins/sparecode/spare_marks.mli
index 92a003570b041fa3cf7509dbaa3efff0b6dae067..d6e60878d7c11c498afe8e03592bf2a2331fb8ff 100644
--- a/src/plugins/sparecode/spare_marks.mli
+++ b/src/plugins/sparecode/spare_marks.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Pdg_types
type proj
type fct
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index e2280ec81b2c4ad240ddcd1902c29356572e55d9..0e3ae5a6f1b496506585981e777937a9a7ef387a 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil
+open Pdg_types
+
module BoolInfo = struct
type proj = Spare_marks.proj
type fct = Spare_marks.fct option * Kernel_function.t
@@ -41,7 +43,7 @@ module BoolInfo = struct
| Some fm -> Spare_marks.key_visible fm key
in
Sparecode_params.debug ~level:3 "%s : %a -> %b"
- txt !Db.Pdg.pretty_key key visible;
+ txt Pdg.Api.pretty_key key visible;
visible
let param_visible (fm,_) n =
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 8a6068698cb4dc5568e7d35a761ccc781bc291a9..eb76164294fca8a88a3e39f3c1937a952a9308e1 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -261,7 +261,7 @@ let _array =
model
-(* ----- Analysis statistics -------------------------------------------- *)
+(* ----- Analysis statistics ------------------------------------------------ *)
module AlarmCategory = struct
open Server.Data
@@ -470,4 +470,76 @@ let _array =
model
-(**************************************************************************)
+(* ----- Domains states ----------------------------------------------------- *)
+
+let compute_lval_deps request lval =
+ let zone = Results.lval_deps lval request in
+ Locations.Zone.get_bases zone
+
+let compute_expr_deps request expr =
+ let zone = Results.expr_deps expr request in
+ Locations.Zone.get_bases zone
+
+let compute_instr_deps request = function
+ | Set (lval, expr, _) ->
+ Base.SetLattice.join
+ (compute_lval_deps request lval)
+ (compute_expr_deps request expr)
+ | Local_init (vi, AssignInit (SingleInit expr), _) ->
+ Base.SetLattice.join
+ (Base.SetLattice.inject_singleton (Base.of_varinfo vi))
+ (compute_expr_deps request expr)
+ | _ -> Base.SetLattice.empty
+
+let compute_stmt_deps request stmt =
+ match stmt.skind with
+ | Instr (instr) -> compute_instr_deps request instr
+ | If (expr, _, _, _) -> compute_expr_deps request expr
+ | _ -> Base.SetLattice.empty
+
+let compute_marker_deps request = function
+ | Printer_tag.PStmt (_, stmt)
+ | PStmtStart (_, stmt) -> compute_stmt_deps request stmt
+ | PLval (_, _, lval) -> compute_lval_deps request lval
+ | PExp (_, _, expr) -> compute_expr_deps request expr
+ | PVDecl (_, _, vi) -> Base.SetLattice.inject_singleton (Base.of_varinfo vi)
+ | _ -> Base.SetLattice.empty
+
+let get_filtered_state request marker =
+ let bases = compute_marker_deps request marker in
+ match bases with
+ | Base.SetLattice.Top -> Results.print_states request
+ | Base.SetLattice.Set bases ->
+ if Base.Hptset.is_empty bases
+ then []
+ else Results.print_states ~filter:bases request
+
+let get_state filter request marker =
+ if filter
+ then get_filtered_state request marker
+ else Results.print_states request
+
+let get_states (marker, filter) =
+ let kinstr = Printer_tag.ki_of_localizable marker in
+ match kinstr with
+ | Kglobal -> []
+ | Kstmt stmt ->
+ let states_before = get_state filter (Results.before stmt) marker in
+ let states_after = get_state filter (Results.after stmt) marker in
+ match states_before, states_after with
+ | [], _ -> List.map (fun (name, after) -> name, "", after) states_after
+ | _, [] -> List.map (fun (name, before) -> name, before, "") states_before
+ | _, _ ->
+ let join (name, before) (name', after) =
+ assert (name = name');
+ name, before, after
+ in
+ List.rev_map2 join states_before states_after
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getStates"
+ ~descr:(Markdown.plain "Get the domain states about the given marker")
+ ~input:(module Data.Jpair (Kernel_ast.Marker) (Data.Jbool))
+ ~output:(module Data.Jlist
+ (Data.Jtriple (Data.Jstring) (Data.Jstring) (Data.Jstring)))
+ get_states
diff --git a/src/plugins/value/domains/abstract_domain.ml b/src/plugins/value/domains/abstract_domain.ml
index e8536eb1f6e16c262d723f096cf919917e47eb29..6e36e58388bb196ca4fad8487d8c4a87a3863c2b 100644
--- a/src/plugins/value/domains/abstract_domain.ml
+++ b/src/plugins/value/domains/abstract_domain.ml
@@ -338,19 +338,24 @@ module type Reuse = sig
disables MemExec. *)
val relate: kernel_function -> Base.Hptset.t -> t -> Base.SetLattice.t
- (** [filter kf kind bases states] reduces the state [state] to only keep
+ (** [filter kind bases states] reduces the state [state] to only keep
properties about [bases] — it is a projection on the set of [bases].
It allows reusing an analysis of [kf] from an initial state [pre] to a
final state [post].
- If [kind] is `Pre, [state] is the initial state [pre], and [bases]
- includes all inputs of [kf] and satisfies [relate kf bases state = bases].
- If [kind] is `Post, [state] is the final state [post], and [bases]
+ If [kind] is [`Pre kf], [state] is the initial state of function [kf],
+ and [bases] includes all inputs of [kf] and satisfies
+ [relate kf bases state = bases].
+ If [kind] is [`Post kf], [state] is the final state of [kf], and [bases]
includes all inputs and outputs of [kf].
Afterwards, the two resulting states [reduced_pre] and [reduced_post] are
used as follow: when [kf] should be analyzed with the initial state [s],
if [filter kf `Pre s = reduced_pre], then the analysis is skipped, and
- [reuse kf s reduced_post] is used as its final state instead. *)
- val filter: kernel_function -> [`Pre | `Post] -> Base.Hptset.t -> t -> t
+ [reuse kf s reduced_post] is used as its final state instead.
+ If [kind] is [`Print], the state is reduced before printing it for the
+ end-user. *)
+ val filter:
+ [`Pre of kernel_function | `Post of kernel_function | `Print ] ->
+ Base.Hptset.t -> t -> t
(** [reuse kf bases current_input previous_output] merges the initial state
[current_input] with a final state [previous_output] from a previous
@@ -376,6 +381,10 @@ module type S = sig
type state
include Datatype.S_with_collections with type t = state
+ (* The domain name, shown in some logs and in the GUI. Be sure to redefine a
+ clear and simple name instead of the default one coming from Datatype. *)
+ val name: string
+
(** {3 Lattice Structure } *)
include Lattice with type state := t
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 77f90be12ff69cc314f8da40cba6f39990e344c1..68d1f194f995758cef798ecbed61fbfd4c22ce52 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -181,7 +181,8 @@ module State = struct
let mem_project = Datatype.never_any_project
end )
- let key = Structure.Key_Domain.create_key "cvalue_domain"
+ let name = "cvalue"
+ let key = Structure.Key_Domain.create_key name
type value = Model.value
type location = Model.location
@@ -287,7 +288,7 @@ module State = struct
let relate _kf _bases _state = Base.SetLattice.empty
(* Auxiliary function that keeps only some bases inside a memory state *)
- let filter _kf _kind bases (state, clob) =
+ let filter _kind bases (state, clob) =
Cvalue.Model.filter_by_shape bases state, clob
let reuse _ _ ~current_input:(state, _) ~previous_output:(output, clob) =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 141c643cc703d84b082afa5a7af9e5b6355a0b92..bea7217028e5f618e54498e1c2d54c4bf404fc6e 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -46,7 +46,9 @@ module type LeafDomain = sig
val incr_loop_counter: stmt -> t -> t
val leave_loop: stmt -> t -> t
- val filter: kernel_function -> [`Pre | `Post] -> Base.Hptset.t -> t -> t
+ val filter:
+ [`Pre of kernel_function | `Post of kernel_function | `Print ] ->
+ Base.Hptset.t -> t -> t
val reuse:
kernel_function -> Base.Hptset.t ->
current_input:t -> previous_output:t -> t
@@ -72,7 +74,7 @@ module Complete (Domain: InputDomain) = struct
let incr_loop_counter _stmt state = state
let leave_loop _stmt state = state
- let filter _kf _kind _bases state = state
+ let filter _kind _bases state = state
let reuse _kf _bases ~current_input:_ ~previous_output = previous_output
let show_expr _valuation _state fmt _expr =
@@ -325,6 +327,7 @@ module Restrict
module I = struct let module_name = Domain.name ^ " option" end
include Datatype.Option_with_collections (D) (I)
+ let name = Domain.name
let default = Domain.top, Mode.all
let structure: t Abstract.Domain.structure =
@@ -575,9 +578,9 @@ module Restrict
| None -> Base.SetLattice.empty
| Some (state, _mode) -> Domain.relate kf bases state
- let filter kf kind bases = function
+ let filter kind bases = function
| None -> None
- | Some (state, mode) -> Some (Domain.filter kf kind bases state, mode)
+ | Some (state, mode) -> Some (Domain.filter kind bases state, mode)
let reuse kf bases ~current_input ~previous_output =
match current_input, previous_output with
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index bf3c05b8f0cc79efed1e2e4ec30131f737bd49df..d4356a571fd6e3ed178c3f7d62037167d36816ae 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -27,6 +27,8 @@ open Cil_types
open Eval
module type InputDomain = sig
+ (* The [name] value from Datatype should be the domain name and will be used
+ in some logs and in the GUI for the end-user. *)
include Datatype.S
val top: t
val join: t -> t -> t
@@ -52,7 +54,9 @@ module type LeafDomain = sig
val incr_loop_counter: stmt -> t -> t
val leave_loop: stmt -> t -> t
- val filter: kernel_function -> [`Pre | `Post] -> Base.Hptset.t -> t -> t
+ val filter:
+ [`Pre of kernel_function | `Post of kernel_function | `Print ] ->
+ Base.Hptset.t -> t -> t
val reuse:
kernel_function -> Base.Hptset.t ->
current_input:t -> previous_output:t -> t
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 550a86f3d45fd987f474e297732ee21553b1f157..52abf820dee9979a0b9b0fc711dfccce911fa939 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -42,14 +42,15 @@ module Make
}
let () = incr counter
- let name = Left.name ^ "*" ^ Right.name ^
- "(" ^ string_of_int !counter ^ ")"
+ let unique_name = Left.name ^ "*" ^ Right.name ^
+ "(" ^ string_of_int !counter ^ ")"
include Datatype.Pair_with_collections
(Left)
(Right)
- (struct let module_name = name end)
+ (struct let module_name = unique_name end)
type state = t
+ let name = Left.name ^ " * " ^ Right.name
let structure = Abstract.Domain.Node (Left.structure, Right.structure)
@@ -292,8 +293,8 @@ module Make
let relate kf bases (left, right) =
Base.SetLattice.join
(Left.relate kf bases left) (Right.relate kf bases right)
- let filter kf kind bases (left, right) =
- Left.filter kf kind bases left, Right.filter kf kind bases right
+ let filter kind bases (left, right) =
+ Left.filter kind bases left, Right.filter kind bases right
let reuse kf bases ~current_input ~previous_output =
let left_input, right_input = current_input
and left_output, right_output = previous_output in
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 44604b43c15df1ff2c12a3940b0d0d745d580dff..542d48cc2ce424ece24b54e1cdfc07a6428bab75 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -121,6 +121,8 @@ module Internal = struct
type state = t
+ let name = "equality"
+
let log_category = dkey
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 7a91a6af3f8e2dc22c04e88287d12316f2853dd0..829afa083647c8d8e174c8e8c3a1303b840df1c9 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -532,6 +532,8 @@ module G = struct
(Datatype.List(Datatype.Pair(Cil_datatype.Stmt)(IterationInfo)))
(struct let module_name = "Values.Gauges_domain.G" end)
+ let name = "gauges"
+
let empty = MV.empty, []
let top (state: t) : t =
let top_iteration_info = function
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 8028b618a1d7e5df61659ebd87c72c7921f8ab96..63af3599eafb50965cc660d38e85473fa0d0a957 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -44,7 +44,7 @@ module LatticeInout = struct
include Datatype.Serializable_undefined
type t = inout
- let name = "Value.Inout.t"
+ let name = "inout"
let reprs = [ {
over_outputs = List.hd Zone.reprs;
diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index 2f6459d9c5c63631f202e43bf47504a6dfb34690..e1300c7d470e968079b423f3a7a7e5ab2ac2476e 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -363,6 +363,8 @@ struct
(Datatype.Option (Tracking))
(struct let module_name = "DomainLattice" end)
+ let name = "multidim"
+
type state = t
type value = Value.t
type value_or_uninitialized = Value_or_Uninitialized.t
@@ -885,7 +887,7 @@ struct
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases (base_map,tracked : t) =
+ let filter _kind bases (base_map,tracked : t) =
BaseMap.filter (fun elt -> Base.Hptset.mem elt bases) base_map,
Option.map (Tracking.inter bases) tracked
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 757ad4d87ecadaba7e9b0bfe9fa985c413fba7f6..b463daa3ac3b49fe3278cbb5e441cc55547f1616 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -701,7 +701,7 @@ module State = struct
type t = state
include Datatype.Serializable_undefined
- let name = "Octagons.State"
+ let name = "octagon"
let structural_descr =
Structural_descr.t_record
[| Octagons.packed_descr;
@@ -1275,7 +1275,7 @@ module Domain = struct
in
Base.Hptset.fold aux bases Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
if intraprocedural ()
then state
else
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 66ffd1337c2b6e88dd72b51d5fbc08a9ccea7c64..396598578c7eb76547068d810671bdde1078ab3b 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -81,6 +81,8 @@ module Memory = struct
include
Lmap.Make_LOffset(V_Or_Uninitialized)(V_Offsetmap)(Default_offsetmap)
+ let name = "bitwise"
+
let widen kf stmt s1 s2 =
let wh = Widen.getWidenHints kf stmt in
widen wh s1 s2
@@ -197,7 +199,7 @@ module D : Abstract_domain.Leaf
(* Memexec *)
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
Memory.filter_by_shape bases state
let reuse _kf bases ~current_input:input ~previous_output:output =
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index ab4c24f45a6d23b5a03fe815b68502fb7bfd454c..93abea72d3e62b33148dbcc5ede6db82b730a992 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -34,6 +34,7 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
(* In this domain, the states contain nothing. We use [unit] as type formal
the state and we reuse [Datatype.Unit] as a base for our domain. *)
include Datatype.Unit
+ let name = "printer"
(* --- Lattice operators --- *)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 33bae1ed3a01b54fba5d06cbbfcb0fdf77549c77..a0ba820a46fc63cde8dd2449ba2787a536ac2c76 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -47,7 +47,7 @@ module type S = sig
val fold: (Base.t -> value -> 'a -> 'a) -> t -> 'a -> 'a
end
-module Make_Memory (Value: Value) = struct
+module Make_Memory (Info: sig val name: string end) (Value: Value) = struct
module Initial_Values = struct let v = [] end
module Deps = struct let l = [Ast.self] end
@@ -55,8 +55,10 @@ module Make_Memory (Value: Value) = struct
include Hptmap.Make
(Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ let name = Info.name
+
let cache_name s =
- Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
+ Hptmap_sig.PersistentCache ("Value." ^ name ^ "." ^ s)
let disjoint_union =
let cache = cache_name "union" in
@@ -186,7 +188,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
try Some (Hashtbl.find table name)
with Not_found -> None
- module M = Make_Memory (Value)
+ module M = Make_Memory (Info) (Value)
include M
include Domain_builder.Complete (M)
@@ -325,7 +327,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
M.filter (fun elt -> Base.Hptset.mem elt bases) state
let reuse _kf bases ~current_input ~previous_output =
diff --git a/src/plugins/value/domains/simple_memory.mli b/src/plugins/value/domains/simple_memory.mli
index a194b4fe98797e8aa3438a4109d488bcf1cdb048..bbbd93735a956fa1ca8c9f9b9cb14a30a2d562b4 100644
--- a/src/plugins/value/domains/simple_memory.mli
+++ b/src/plugins/value/domains/simple_memory.mli
@@ -86,7 +86,7 @@ module type S = sig
end
(* Builds a memory from a value abstraction. *)
-module Make_Memory (Value: Value) : sig
+module Make_Memory (Info: sig val name: string end) (Value: Value) : sig
include Datatype.S_with_collections
include S with type t := t
and type value := Value.t
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 0d95237c6476678c6147b3ece9ad12a34fda9616..5ab410de611174dfee0f7a2ec1e9c1b20f128cea 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -182,7 +182,7 @@ module Memory = struct
include Datatype.Serializable_undefined
type t = memory
- let name = "Value.Symbolic_locs.Memory.t"
+ let name = "symbolic-locations"
let reprs = [ { values = List.hd K2V.M.reprs;
zones = List.hd K2Z.reprs;
@@ -603,7 +603,7 @@ module D : Abstract_domain.Leaf
by itself a variable read or written by f to a variable that is not. *)
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind = Memory.filter
+ let filter _kind = Memory.filter
(* Efficient version of [reuse], but the resulting state does not satisfy
the [_check state], as some extra dependenies of keys removed from the
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 7d46ca1e8094212d0653b9db9d465f8deb6b053d..f32bc939b956f7adb1b141cb95258b418d0bb4fb 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -75,7 +75,7 @@ module LatticeTaint = struct
type t = taint
- let name = "Value.Taint.t"
+ let name = "taint"
let reprs =
[ { locs_data = List.hd Zone.reprs;
@@ -369,7 +369,7 @@ module TaintDomain = struct
(* MemExec cache. *)
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
let filter_base = Zone.filter_base (fun b -> Base.Hptset.mem b bases) in
{ state with locs_data = filter_base state.locs_data;
locs_control = filter_base state.locs_control;
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 52e14219be6b7f3d87404deb6e778f55890cc0a2..98cd954008c82b4b7f0fd80fbe920b5bbea07c5c 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -532,7 +532,7 @@ module Traces = struct
include Datatype.Serializable_undefined
type t = state
- let name = "Value.Traces_domain.Traces.state"
+ let name = "traces"
let reprs = [empty]
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5307ef978d60d4ceeaf3a94501935175e8cfabc8..d7f7bb0a24495a638422370353bf576bbfee0e63 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -27,7 +27,7 @@ module Static = struct
include Datatype.Unit
type state = t
- let name = "Unit domain"
+ let name = "unit"
let log_category = log_key
let structure = Abstract.Domain.Unit
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index fedceb3f36ff2cd185349b8eb1b5f5303ce05829..c2221af95912657e3c1c5537a18c7ec5d8b94b5e 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -342,7 +342,6 @@ let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc
(* Set the name of the domain. *)
let module Domain = struct
include (val domain)
- let name = dname
module Store = struct
include Store
let register_global_state storage state =
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index ecd7a20c34ac6a793fb64e296ecdde05306f9006..cf8268830c4cdfa967b46f8527067d1a27423d03 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -181,7 +181,7 @@ module Make
| Base.SetLattice.Top -> raise TooImprecise
| Base.SetLattice.Set bases -> bases
in
- let state_input = Domain.filter kf `Pre input_bases input_state in
+ let state_input = Domain.filter (`Pre kf) input_bases input_state in
(* Outputs bases, that is bases that are copy-pasted, also include
input bases. Indeed, those may get reduced during the call. *)
let all_output_bases =
@@ -197,7 +197,7 @@ module Make
Extlib.opt_fold Base.Hptset.add return_base all_output_bases
in
let clear (key,state) =
- key, Domain.filter kf `Post all_output_bases state
+ key, Domain.filter (`Post kf) all_output_bases state
in
let outputs = List.map clear call_result in
let call_number = current_counter () in
@@ -241,7 +241,7 @@ module Make
then ()
else
(* restrict [state] to the inputs of this call *)
- let st_filtered = Domain.filter kf `Pre binputs state in
+ let st_filtered = Domain.filter (`Pre kf) binputs state in
try
let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
(* We have found a previous execution, in which the outputs are
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 540bc32142af6c42de9b85c1dbca17bc36ab2504..56935b6b2281b2aaef1ea25d1ccc65ad6624b27c 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -293,6 +293,26 @@ struct
| Some extract ->
convert (Response.map_join extract Cvalue.Model.join (get req))
+ let print_states ?filter req =
+ let state = Response.map_join (fun x -> x) A.Dom.join (get req) in
+ let print (type s)
+ (key: s Abstract.Domain.key)
+ (module Domain: Abstract_domain.S with type state = s)
+ (state: s) acc =
+ let name = Structure.Key_Domain.name key in
+ let state =
+ match filter with
+ | None -> state
+ | Some bases -> Domain.filter `Print bases state
+ in
+ let str = Format.asprintf "%a" Domain.pretty state in
+ (name, str) :: acc
+ in
+ let polymorphic_fold_fun = A.Dom.{ fold = print } in
+ match state with
+ | `Top | `Bottom -> []
+ | `Value state -> A.Dom.fold polymorphic_fold_fun state []
+
(* Evaluation *)
let eval_lval lval req =
@@ -487,6 +507,10 @@ let get_cvalue_model req =
| Error Bottom -> Cvalue.Model.bottom
| Error (Top | DisabledDomain) -> Cvalue.Model.top
+let print_states ?filter req =
+ let module E = Make () in
+ E.print_states ?filter req
+
(* Depedencies *)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index e6c0678569aa2f5e7077e6780f285ac667560a5f..e18f41a032527bbde86a2c4b4122423e202afb9d 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -161,6 +161,11 @@ val get_cvalue_model : request -> Cvalue.Model.t
(** Returns the Cvalue model. *)
val get_cvalue_model_result : request -> Cvalue.Model.t result
+(** Returns a textual representation of the internal domain states for the given
+ request. If [filter] is provided, states are filtered on the given bases
+ (for domains that support this feature).
+ Returns a list of pair (name, state) for all available domains. *)
+val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list
(** Dependencies *)
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 72cda0e26683743613099657926c9643456bb9f9..40733bca78a1e227aad8b2d39b822b546c94bf83 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -28,6 +28,7 @@ module type Key = sig
val create_key: string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) eq option
+ val name: 'a key -> string
val print: 'a key Pretty_utils.formatter
val compare: 'a key -> 'b key -> int
val equal: 'a key -> 'b key -> bool
@@ -82,6 +83,7 @@ module Make () = struct
let hash x = x.tag
let tag x = x.tag
+ let name x = x.name
let print fmt x = Format.pp_print_string fmt x.name
end
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index 792d6a8376e50877c30eb25b760484db5f42b29d..f0c6ed245ddc9a7f9e7e3d8659a8a44e9448fb82 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -34,6 +34,7 @@ module type Key = sig
val create_key: string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) eq option
+ val name: 'a key -> string
val print: 'a key Pretty_utils.formatter
val compare: 'a key -> 'b key -> int
val equal: 'a key -> 'b key -> bool
diff --git a/src/plugins/wp/tests/wp_bts/bts_1586.i b/src/plugins/wp/tests/wp_bts/bts_1586.i
index dab7fc01fe3489960e604ec1a582048561820a0e..510137770e7c34d8dcec9e29899e910519cbaa7e 100644
--- a/src/plugins/wp/tests/wp_bts/bts_1586.i
+++ b/src/plugins/wp/tests/wp_bts/bts_1586.i
@@ -1,54 +1,54 @@
-
-/*@ behavior Bizarre:
- assumes x;
- ensures TRANS: x ==> \result==1 ;
- */
-int compute_bizarre(int x)
-{
- if (x)
- return 1;
- else
- return 2;
-}
-
-/*@ behavior Normal:
- assumes x;
- ensures TRANS: x <==> \result==1 ;
- */
-int compute_normal(int x)
-{
- if (x)
- return 1;
- else
- return 2;
-}
-
-int main_bizarre_KO(int x)
-{
- int trans = compute_bizarre(x);
-
- switch(trans) {
- case 0:
- //@ assert FALSE: \false;
- return -1;
- break;
- default:
- return -1;
- break;
- }
-}
-
-int main_normal_KO(int x)
-{
- int trans = compute_normal(x);
-
- switch(trans) {
- case 0:
- //@ assert FALSE: \false;
- return -1;
- break;
- default:
- return -1;
- break;
- }
-}
+
+/*@ behavior Bizarre:
+ assumes x;
+ ensures TRANS: x ==> \result==1 ;
+ */
+int compute_bizarre(int x)
+{
+ if (x)
+ return 1;
+ else
+ return 2;
+}
+
+/*@ behavior Normal:
+ assumes x;
+ ensures TRANS: x <==> \result==1 ;
+ */
+int compute_normal(int x)
+{
+ if (x)
+ return 1;
+ else
+ return 2;
+}
+
+int main_bizarre_KO(int x)
+{
+ int trans = compute_bizarre(x);
+
+ switch(trans) {
+ case 0:
+ //@ assert FALSE: \false;
+ return -1;
+ break;
+ default:
+ return -1;
+ break;
+ }
+}
+
+int main_normal_KO(int x)
+{
+ int trans = compute_normal(x);
+
+ switch(trans) {
+ case 0:
+ //@ assert FALSE: \false;
+ return -1;
+ break;
+ default:
+ return -1;
+ break;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_bts/ergo_typecheck.i b/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
index 27786043f20fd6d2e90613e767fd3de0deed156c..3a05b9220dd03e2b1b1444e202df0a8a79ab2978 100644
--- a/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
+++ b/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
@@ -1,44 +1,44 @@
-typedef struct
-{
- unsigned int a[2];
- unsigned int b[2];
- unsigned int c;
-} my_type;
-
-my_type var = {0};
-
-/*@
- @ ensures var_divded : var == {\old(var) \with
- @ .a = {\old(var.a) \with
- @ [0] = (unsigned int) 0,
- @ [1] = (unsigned int) 1},
- @ .b = {\old(var.b) \with
- @ [0] = (unsigned int)(\old(var.b[0]) + 1),
- @ [1] = (unsigned int)(\old(var.b[1]) + 2)},
- @ .c = (unsigned int) 5
- @ };
- @
- @ ensures var_inline : var == {\old(var) \with
- @ .a[0] = (unsigned int) 0,
- @ .a[1] = (unsigned int) 1,
- @ .b[0] = (unsigned int)(\old(var.b[0]) + 1),
- @ .b[1] = (unsigned int)(\old(var.b[1]) + 2),
- @ .c = (unsigned int) 5
- @ };
- @
- @ ensures var_unit0 : var.a[0] == 0;
- @ ensures var_unit1 : var.a[1] == 1;
- @ ensures var_unit2 : var.b[0] == (unsigned int)(\old(var.b[0]) + 1);
- @ ensures var_unit3 : var.b[1] == (unsigned int)(\old(var.b[1]) + 2);
- @ ensures var_unit4 : var.c == 5;
- @ assigns var;
- @
- */
-void f()
-{
- var.a[0] = 0u;
- var.a[1] = 1u;
- var.b[0] ++;
- var.b[1] += 2;
- var.c = 5u;
-}
+typedef struct
+{
+ unsigned int a[2];
+ unsigned int b[2];
+ unsigned int c;
+} my_type;
+
+my_type var = {0};
+
+/*@
+ @ ensures var_divded : var == {\old(var) \with
+ @ .a = {\old(var.a) \with
+ @ [0] = (unsigned int) 0,
+ @ [1] = (unsigned int) 1},
+ @ .b = {\old(var.b) \with
+ @ [0] = (unsigned int)(\old(var.b[0]) + 1),
+ @ [1] = (unsigned int)(\old(var.b[1]) + 2)},
+ @ .c = (unsigned int) 5
+ @ };
+ @
+ @ ensures var_inline : var == {\old(var) \with
+ @ .a[0] = (unsigned int) 0,
+ @ .a[1] = (unsigned int) 1,
+ @ .b[0] = (unsigned int)(\old(var.b[0]) + 1),
+ @ .b[1] = (unsigned int)(\old(var.b[1]) + 2),
+ @ .c = (unsigned int) 5
+ @ };
+ @
+ @ ensures var_unit0 : var.a[0] == 0;
+ @ ensures var_unit1 : var.a[1] == 1;
+ @ ensures var_unit2 : var.b[0] == (unsigned int)(\old(var.b[0]) + 1);
+ @ ensures var_unit3 : var.b[1] == (unsigned int)(\old(var.b[1]) + 2);
+ @ ensures var_unit4 : var.c == 5;
+ @ assigns var;
+ @
+ */
+void f()
+{
+ var.a[0] = 0u;
+ var.a[1] = 1u;
+ var.b[0] ++;
+ var.b[1] += 2;
+ var.c = 5u;
+}
diff --git a/tests/misc/array_sizeof.i b/tests/misc/array_sizeof.i
new file mode 100644
index 0000000000000000000000000000000000000000..c857ad90a1b0f3dddaff3790a7ea5fccb2b7f24d
--- /dev/null
+++ b/tests/misc/array_sizeof.i
@@ -0,0 +1,17 @@
+/* run.config
+PLUGIN: @EVA_PLUGINS@
+STDOPT:
+*/
+
+int x;
+void main(int c) {
+if (c) {
+ unsigned char buf[sizeof(unsigned char[1]) + sizeof(x)];
+ buf[sizeof(buf)];
+}
+else {
+ x = 4;
+ unsigned char buf[sizeof(unsigned char[1]) + x];
+ buf[x];
+}
+}
diff --git a/tests/misc/oracle/array_sizeof.res.oracle b/tests/misc/oracle/array_sizeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..04709d7aeef10d123f254d881895f0173ef3a986
--- /dev/null
+++ b/tests/misc/oracle/array_sizeof.res.oracle
@@ -0,0 +1,40 @@
+[kernel] Parsing array_sizeof.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ x ∈ {0}
+[eva:alarm] array_sizeof.i:10: Warning:
+ accessing out of bounds index.
+ assert
+ sizeof(unsigned char [sizeof(unsigned char [1]) + sizeof(x)]) <
+ (unsigned int)(sizeof(unsigned char [1]) + sizeof(int));
+[eva] array_sizeof.i:14: assertion 'alloca_bounds' got status valid.
+[eva] array_sizeof.i:14: Call to builtin __fc_vla_alloc
+[eva] array_sizeof.i:14: allocating variable __malloc_main_l14
+[eva:alarm] array_sizeof.i:15: Warning:
+ accessing uninitialized left-value. assert \initialized(buf_0 + x);
+[eva] Recording results for main
+[eva] done for function main
+[eva] array_sizeof.i:10: assertion 'Eva,index_bound' got final status invalid.
+[eva] array_sizeof.i:15:
+ assertion 'Eva,initialization' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ NON TERMINATING FUNCTION
+[from] Computing for function main
+[from] Computing for function __fc_vla_alloc <-main
+[from] Done for function __fc_vla_alloc
+[from] Non-terminating function main (no dependencies)
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function __fc_vla_alloc:
+ \result FROM \nothing
+[from] Function main:
+ NON TERMINATING - NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ x; tmp; buf_0; __lengthof_buf_0; tmp_3
+[inout] Inputs for function main:
+ x; __malloc_main_l14[4]
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 716e5067f6a276524b036e8efe28dd061dd235ab..4907cf29314c0d98ef989c991d66b70567bc1493 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -21,29 +21,29 @@ let main _ =
File.pretty_ast ();
Kernel.Debug.set memo_debug ;
let kf = Globals.Functions.find_def_by_name "main" in
- let pdg = !Db.Pdg.get kf in
- Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
- !Db.Pdg.extract pdg "dyn_dpds_0.dot";
+ let pdg = Pdg.Api.get kf in
+ Format.printf "%a@." (Pdg.Api.pretty ~bw:false) pdg;
+ Pdg.Api.extract pdg "dyn_dpds_0.dot";
let assert_sid = 5 in (* assert ( *p>G) *)
let assert_stmt, kf = Kernel_function.find_from_sid assert_sid in
let _assert_node =
- match !Db.Pdg.find_simple_stmt_nodes pdg assert_stmt with
+ match Pdg.Api.find_simple_stmt_nodes pdg assert_stmt with
| n::[] -> n | _ -> assert false
in
let star_p = get_zones "*p" (assert_stmt, kf) in
let data_nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg assert_stmt ~before:true star_p
+ Pdg.Api.find_location_nodes_at_stmt pdg assert_stmt ~before:true star_p
in
assert (undef = None);
let g_zone = get_zones "G" (assert_stmt, kf) in
let g_nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg assert_stmt ~before:true g_zone
+ Pdg.Api.find_location_nodes_at_stmt pdg assert_stmt ~before:true g_zone
in
let _data_nodes = g_nodes @ data_nodes in
let undef = match undef with None -> assert false | Some z -> z in
Format.printf "Warning : cannot select %a in this function...@\n"
Locations.Zone.pretty undef;
- Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
- !Db.Pdg.extract pdg "dyn_dpds_1.dot"
+ Format.printf "%a@." (Pdg.Api.pretty ~bw:false) pdg;
+ Pdg.Api.extract pdg "dyn_dpds_1.dot"
let () = Db.Main.extend main
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index f9759901253978aef39e3675d91663df60b7587e..23c627b3a5bb207fb6a40a3d1ec5fcd793dfbe3e 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -1,58 +1,57 @@
-open Db;;
-open Cil_types;;
-
-let pp_nodes msg nodes =
- Kernel.result "%s" msg ;
- List.iter (fun n -> Kernel.result "%a" (!Pdg.pretty_node false) n) nodes;;
-
-exception Find of varinfo;;
-
-let main _ =
- let f = Globals.Functions.find_by_name "f" in
- let pdg = !Pdg.get f in
-
- (* Uncomment to retrieve sid *)
- (*Kernel.Debug.set 1;;
- Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
- *)
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let stmt_1 = fst (Kernel_function.find_from_sid 1) in (* y = 0 *)
- let node = !Pdg.find_stmt_node pdg stmt_1 in
- let nodes = !Pdg.all_uses pdg [node] in
- pp_nodes "Test [all_uses] stmt1" nodes;
-
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let y =
- try
- Globals.Vars.iter (fun v _ -> if v.vname = "y" then raise (Find v));
- assert false
- with Find v ->
- v
- in
-
- let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
- let y_at_11_nodes, undef = (* y=5 *)
- !Pdg.find_location_nodes_at_stmt
- pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
- in
-
- assert (undef = None);
- let y_at_11_nodes = List.map (fun (n,_z) -> n) y_at_11_nodes in
-
- let () = pp_nodes "Test [find_location_nodes_at_stmt] y@11" y_at_11_nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = !Pdg.all_dpds pdg y_at_11_nodes in
- let () = pp_nodes "Test [all_dpds] y@11" nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = !Pdg.all_uses pdg y_at_11_nodes in
- let () = pp_nodes "Test [all_uses] y@11" nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let all_related_nodes pdg =
- let all n = (!Pdg.direct_uses pdg n) @ (!Pdg.direct_dpds pdg n) in
- !Pdg.custom_related_nodes all
- in
- let nodes = all_related_nodes pdg y_at_11_nodes in
- pp_nodes "Test [all_related_nodes] y@11" nodes
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-
-let () = Db.Main.extend main
+open Cil_types;;
+
+let pp_nodes msg nodes =
+ Kernel.result "%s" msg ;
+ List.iter (fun n -> Kernel.result "%a" (Pdg.Api.pretty_node false) n) nodes;;
+
+exception Find of varinfo;;
+
+let main _ =
+ let f = Globals.Functions.find_by_name "f" in
+ let pdg = Pdg.Api.get f in
+
+ (* Uncomment to retrieve sid *)
+ (*Kernel.Debug.set 1;;
+ Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
+ *)
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let stmt_1 = fst (Kernel_function.find_from_sid 1) in (* y = 0 *)
+ let node = Pdg.Api.find_stmt_node pdg stmt_1 in
+ let nodes = Pdg.Api.all_uses pdg [node] in
+ pp_nodes "Test [all_uses] stmt1" nodes;
+
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let y =
+ try
+ Globals.Vars.iter (fun v _ -> if v.vname = "y" then raise (Find v));
+ assert false
+ with Find v ->
+ v
+ in
+
+ let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
+ let y_at_11_nodes, undef = (* y=5 *)
+ Pdg.Api.find_location_nodes_at_stmt
+ pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
+ in
+
+ assert (undef = None);
+ let y_at_11_nodes = List.map (fun (n,_z) -> n) y_at_11_nodes in
+
+ let () = pp_nodes "Test [find_location_nodes_at_stmt] y@11" y_at_11_nodes in
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let nodes = Pdg.Api.all_dpds pdg y_at_11_nodes in
+ let () = pp_nodes "Test [all_dpds] y@11" nodes in
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let nodes = Pdg.Api.all_uses pdg y_at_11_nodes in
+ let () = pp_nodes "Test [all_uses] y@11" nodes in
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let all_related_nodes pdg =
+ let all n = (Pdg.Api.direct_uses pdg n) @ (Pdg.Api.direct_dpds pdg n) in
+ Pdg.Api.custom_related_nodes all
+ in
+ let nodes = all_related_nodes pdg y_at_11_nodes in
+ pp_nodes "Test [all_related_nodes] y@11" nodes
+(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+
+let () = Db.Main.extend main
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index fae01cc8b503d8b9ea25207c7d62c2617596d3aa..8fed3fdca1f1de30f97a13a1bb3d6d358a5197d9 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -29,7 +29,7 @@ let print_stmt kf =
Slicing.PrintSlice.print_fct_stmts fmt kf
(* print PDG (for debugging purposes) *)
-let print_pdg kf = !Db.Pdg.pretty fmt (!Db.Pdg.get kf) ;;
+let print_pdg kf = Pdg.Api.pretty fmt (Pdg.Api.get kf) ;;
let print_ff ff = Slicing.Api.Slice.pretty fmt ff
diff --git a/tests/slicing/min_call.ml b/tests/slicing/min_call.ml
index ebb0e3e8983bf0c210980e6700575ac75ff6f5ab..80fbe7ad12575a7cf978e0441508b3fec992676d 100644
--- a/tests/slicing/min_call.ml
+++ b/tests/slicing/min_call.ml
@@ -31,8 +31,8 @@ let main _ =
* the call to [send_bis] is visible as wished. *)
Slicing.Api.Project.reset_slicing ();
- (*let pdg_k = !Db.Pdg.get kf_k;;*)
- let calls = !Db.Pdg.find_call_stmts ~caller:kf_k(*pdg_k*) kf_send_bis in
+ (*let pdg_k = Pdg.Api.get kf_k;;*)
+ let calls = Pdg.Api.find_call_stmts ~caller:kf_k(*pdg_k*) kf_send_bis in
let sb_call = match calls with c::[] -> c | _ -> assert false in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.select_stmt_internal kf_k sb_call mark in
@@ -52,8 +52,8 @@ let main _ =
* But as [send_bis] is an undefined function, this makes no difference.
*)
Slicing.Api.Project.reset_slicing ();
- (*let pdg_k = !Db.Pdg.get kf_k;;*)
- let calls = !Db.Pdg.find_call_stmts (*pdg_k*)~caller:kf_k kf_send_bis in
+ (*let pdg_k = Pdg.Api.get kf_k;;*)
+ let calls = Pdg.Api.find_call_stmts (*pdg_k*)~caller:kf_k kf_send_bis in
let sb_call = match calls with c::[] -> c | _ -> assert false in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.select_min_call_internal kf_k sb_call mark in
diff --git a/tests/slicing/select_by_annot.ml b/tests/slicing/select_by_annot.ml
index c3dec000e6239395812460cca35e5dd40299bcda..39e3e6d67a0bbda7190384523b629ca7b7ba20b9 100644
--- a/tests/slicing/select_by_annot.ml
+++ b/tests/slicing/select_by_annot.ml
@@ -7,7 +7,7 @@ open LibSelect;;
let main _ =
Slicing.Api.Project.reset_slicing ();
- let pretty_pdg fmt kf = !Db.Pdg.pretty fmt (!Db.Pdg.get kf) in
+ let pretty_pdg fmt kf = Pdg.Api.pretty fmt (Pdg.Api.get kf) in
let add_annot kf =
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.empty_selects in
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index f9e17c3b87c76683424ec6fc3679609606e3beac..7a7e189a1c90ae91ae2a9165430481ed0d3d05d7 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -7,7 +7,7 @@ include LibSelect;;
let main _ =
Slicing.Api.Project.reset_slicing ();
- let pretty_pdg fmt kf = !Db.Pdg.pretty fmt (!Db.Pdg.get kf) in
+ let pretty_pdg fmt kf = Pdg.Api.pretty fmt (Pdg.Api.get kf) in
let apply_all_actions = Slicing.Api.Request.apply_all_internal in
let print_slice = Slicing.Api.Slice.pretty in
let print_fct_stmts kf =
diff --git a/tests/spec/const_ptr_bts1729.i b/tests/spec/const_ptr_bts1729.i
index e2231335e0454d2586897f1552b3eac698e88e87..cb6ef2c2f0fe442b5bcd69f4714ec14f65cd0c73 100644
--- a/tests/spec/const_ptr_bts1729.i
+++ b/tests/spec/const_ptr_bts1729.i
@@ -1,4 +1,4 @@
-
-static void elem_size(void) {
- //@ assert \valid_read((char const * const *)0);
-}
+
+static void elem_size(void) {
+ //@ assert \valid_read((char const * const *)0);
+}
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index d26b1010abf5ca0abdc6ed8c1f089c43bc39291c..7f6abc845200d0eceff40365c3c812cd702b3632 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -1,55 +1,55 @@
-(*============================================================================*)
-module P = Plugin.Register
- (struct
- let name = "Testing plugin"
- let shortname = "test"
- let help = "Just to test Filter..."
- end)
-module Opt = P.False
- (struct
- let option_name = "-test"
- let help = "switch the plug-in on"
- end)
-(*============================================================================*)
-module Visi = struct
- exception EraseAssigns
- exception EraseAllocation
+(*============================================================================*)
+module P = Plugin.Register
+ (struct
+ let name = "Testing plugin"
+ let shortname = "test"
+ let help = "Just to test Filter..."
+ end)
+module Opt = P.False
+ (struct
+ let option_name = "-test"
+ let help = "switch the plug-in on"
+ end)
+(*============================================================================*)
+module Visi = struct
+ exception EraseAssigns
+ exception EraseAllocation
- type fct = unit
- type proj = unit
+ type fct = unit
+ type proj = unit
- let fct_name vf _fi = vf.Cil_types.vname
- let fct_info () _ = [ () ]
- let param_visible _ _ = true
- let body_visible _fi = true
- let loc_var_visible _ _ = true
- let inst_visible _ _ = true
- let label_visible _ _ _ = true
- let annotation_visible _ _ _ = true
- let fun_precond_visible _ _ = true
- let fun_postcond_visible _ _ = true
- let fun_variant_visible _ _ = true
- let fun_frees_visible _ _ = true
- let fun_allocates_visible _ _ = true
- let fun_assign_visible _ _ = true
- let fun_deps_visible _ _ = true
- let called_info _ _ = None
- let res_call_visible _ _ = true
- let result_visible _ _ = true
- let cond_edge_visible _ _ = true, true
-end
-(*============================================================================*)
-let main () =
- if Opt.get () then
- begin
- let _ast = Ast.get () in
- P.feedback "start compute";
- let new_proj_name = "filtered" in
- let module Transform = Filter.F (Visi) in
- let new_prj = Transform.build_cil_file new_proj_name () in
- Project.on new_prj Opt.clear ();
- P.feedback "exported in new project : %s" new_proj_name
- end
+ let fct_name vf _fi = vf.Cil_types.vname
+ let fct_info () _ = [ () ]
+ let param_visible _ _ = true
+ let body_visible _fi = true
+ let loc_var_visible _ _ = true
+ let inst_visible _ _ = true
+ let label_visible _ _ _ = true
+ let annotation_visible _ _ _ = true
+ let fun_precond_visible _ _ = true
+ let fun_postcond_visible _ _ = true
+ let fun_variant_visible _ _ = true
+ let fun_frees_visible _ _ = true
+ let fun_allocates_visible _ _ = true
+ let fun_assign_visible _ _ = true
+ let fun_deps_visible _ _ = true
+ let called_info _ _ = None
+ let res_call_visible _ _ = true
+ let result_visible _ _ = true
+ let cond_edge_visible _ _ = true, true
+end
+(*============================================================================*)
+let main () =
+ if Opt.get () then
+ begin
+ let _ast = Ast.get () in
+ P.feedback "start compute";
+ let new_proj_name = "filtered" in
+ let module Transform = Filter.F (Visi) in
+ let new_prj = Transform.build_cil_file new_proj_name () in
+ Project.on new_prj Opt.clear ();
+ P.feedback "exported in new project : %s" new_proj_name
+ end
-let () = Db.Main.extend main
-(*============================================================================*)
+let () = Db.Main.extend main
+(*============================================================================*)
diff --git a/tests/syntax/duplicated_global_bts1129.i b/tests/syntax/duplicated_global_bts1129.i
index b95f7dfed63c40ac468c5af75edf3b4f1d7ef84b..b8ac93ff233a19e3dcd95c1d12e7297ff4c9668e 100644
--- a/tests/syntax/duplicated_global_bts1129.i
+++ b/tests/syntax/duplicated_global_bts1129.i
@@ -1,7 +1,7 @@
-void f(int* x);
-
-void f(int* x) { *x++; }
-
-int X;
-//@ ensures X==1;
-void f(int* x);
+void f(int* x);
+
+void f(int* x) { *x++; }
+
+int X;
+//@ ensures X==1;
+void f(int* x);