diff --git a/Makefile b/Makefile
index fb909f46afab84a40328ffe9eed296856317cfb0..9f8f99e9b5e3a794996712a698fed3660a7053c8 100644
--- a/Makefile
+++ b/Makefile
@@ -904,11 +904,10 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
- api/general_requests \
- utils/unit_tests \
- api/values_request \
domains/taint_domain \
- $(APRON_CMO) $(NUMERORS_CMO)
+ $(APRON_CMO) $(NUMERORS_CMO) \
+ api/general_requests api/values_request \
+ utils/unit_tests
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server
diff --git a/ivette/src/dome/renderer/controls/gallery.json b/ivette/src/dome/renderer/controls/gallery.json
index 62fe91ead33c03e2bd5b866519ffd02dfc3574a8..719e0b838040aa67305e87be0730254a02810214 100644
--- a/ivette/src/dome/renderer/controls/gallery.json
+++ b/ivette/src/dome/renderer/controls/gallery.json
@@ -368,5 +368,15 @@
"title": "Package",
"viewBox": "0 0 21 16",
"path": "M5.714 14.571l3.429-1.714v-2.804l-3.429 1.464v3.054zM5.143 10.518l3.607-1.545-3.607-1.545-3.607 1.545zM14.857 14.571l3.429-1.714v-2.804l-3.429 1.464v3.054zM14.286 10.518l3.607-1.545-3.607-1.545-3.607 1.545zM10.286 7.902l3.429-1.473v-2.375l-3.429 1.464v2.384zM9.714 4.518l3.938-1.688-3.938-1.688-3.938 1.688zM19.429 9.143v3.714q0 0.321-0.17 0.598t-0.464 0.42l-4 2q-0.223 0.125-0.509 0.125t-0.509-0.125l-4-2q-0.045-0.018-0.063-0.036-0.018 0.018-0.063 0.036l-4 2q-0.223 0.125-0.509 0.125t-0.509-0.125l-4-2q-0.295-0.143-0.464-0.42t-0.17-0.598v-3.714q0-0.339 0.192-0.625t0.504-0.429l3.875-1.661v-3.571q0-0.339 0.192-0.625t0.504-0.429l4-1.714q0.205-0.089 0.446-0.089t0.446 0.089l4 1.714q0.313 0.143 0.504 0.429t0.192 0.625v3.571l3.875 1.661q0.321 0.143 0.509 0.429t0.188 0.625z"
+ },
+ "DROP.FILLED": {
+ "section": "Eva",
+ "viewBox": "0 0 295 295",
+ "path": "M158.116,6.916c-1.938-4.214-6.151-6.915-10.789-6.916c-4.639-0.001-8.855,2.697-10.793,6.911 c-29.875,64.975-82.858,148.605-82.858,194.09c0,51.721,41.927,93.648,93.648,93.648s93.649-41.928,93.649-93.648 C240.974,155.519,187.992,71.891,158.116,6.916z M143.324,264.816c-34.601,0-62.75-28.149-62.75-62.75c0-6.903,5.597-12.5,12.5-12.5 c6.903,0,12.5,5.597,12.5,12.5c0,20.815,16.935,37.75,37.75,37.75c6.903,0,12.5,5.597,12.5,12.5 C155.824,259.22,150.227,264.816,143.324,264.816z"
+ },
+ "DROP.EMPTY": {
+ "section": "Eva",
+ "viewBox": "0 0 512 512",
+ "path": "M353.613,133.606c-39.327-66.81-77.99-121.944-79.618-124.258C269.876,3.487,263.163,0,256.001,0 c-7.163,0-13.875,3.487-17.994,9.347c-1.626,2.314-40.291,57.448-79.618,124.258C103.415,226.999,76.69,292.12,76.69,332.691 C76.69,431.563,157.128,512,256.001,512S435.31,431.563,435.31,332.691C435.31,292.12,408.587,226.997,353.613,133.606z M256.001,468.012c-74.616,0-135.323-60.705-135.323-135.321c0-57.658,85.693-197.636,135.324-271.762 c49.63,74.111,135.32,214.066,135.32,271.762C391.322,407.308,330.617,468.012,256.001,468.012z"
}
}
diff --git a/ivette/src/dome/renderer/table/views.tsx b/ivette/src/dome/renderer/table/views.tsx
index 654599d6b9fc4432f0e16b7069e965d768ba76cd..971994a341212189e42cda7f208d233f242fb446 100644
--- a/ivette/src/dome/renderer/table/views.tsx
+++ b/ivette/src/dome/renderer/table/views.tsx
@@ -409,7 +409,7 @@ class TableState<Key, Row> {
const cwr = colws.get(rcol);
const wl = cwl ? cwl + offset : 0;
const wr = cwr ? cwr - offset : 0;
- if (wl > 40 && wr > 40) {
+ if (wl > 25 && wr > 25) {
const { resize } = this;
resize.set(lcol, wl);
resize.set(rcol, wr);
diff --git a/ivette/src/frama-c/api/generated/kernel/properties/index.ts b/ivette/src/frama-c/api/generated/kernel/properties/index.ts
index bd3d2a7d4170e8a883912045120f7d48a522acd5..80e498300fff92cff41a415bed35def2dc4be947 100644
--- a/ivette/src/frama-c/api/generated/kernel/properties/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/properties/index.ts
@@ -122,6 +122,8 @@ export enum propKind {
lemma = 'lemma',
/** Logical check lemma */
check_lemma = 'check_lemma',
+ /** ACSL extension */
+ extension = 'extension',
}
/** Loose decoder for `propKind` */
diff --git a/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts b/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
index 56cc6605d4e490885d3605fdbe2990a7f4ecf078..d1916a17963dc979304c9a4dbb44d27ef73b9e58 100644
--- a/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
+++ b/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
@@ -45,6 +45,14 @@ import { jMarker } from 'frama-c/api/kernel/ast';
import { jMarkerSafe } from 'frama-c/api/kernel/ast';
//@ts-ignore
import { marker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { byTag } from 'frama-c/api/kernel/data';
+//@ts-ignore
+import { jTag } from 'frama-c/api/kernel/data';
+//@ts-ignore
+import { jTagSafe } from 'frama-c/api/kernel/data';
+//@ts-ignore
+import { tag } from 'frama-c/api/kernel/data';
const isComputed_internal: Server.GetRequest<null,boolean> = {
kind: Server.RqKind.GET,
@@ -111,4 +119,117 @@ const getDeadCode_internal: Server.GetRequest<Json.key<'#fct'>,deadCode> = {
/** Get the lists of unreachable and of non terminating statements in a function */
export const getDeadCode: Server.GetRequest<Json.key<'#fct'>,deadCode>= getDeadCode_internal;
+/** TODO */
+export enum taintStatus {
+ /** The Eva taint analysis has not been computed */
+ not_computed = 'not_computed',
+ /** Error: the memory zone on which this property depends could not be computed */
+ error = 'error',
+ /** No taint for this kind of property */
+ not_applicable = 'not_applicable',
+ /** Tainted property: this property is related to a memory zone that can be affected by an attacker, according to the Eva taint domain. */
+ tainted = 'tainted',
+ /** Untainted property: this property is safe, according to the Eva taint domain. */
+ not_tainted = 'not_tainted',
+}
+
+/** Loose decoder for `taintStatus` */
+export const jTaintStatus: Json.Loose<taintStatus> = Json.jEnum(taintStatus);
+
+/** Safe decoder for `taintStatus` */
+export const jTaintStatusSafe: Json.Safe<taintStatus> =
+ Json.jFail(Json.jEnum(taintStatus),
+ 'plugins.eva.general.taintStatus expected');
+
+/** Natural order for `taintStatus` */
+export const byTaintStatus: Compare.Order<taintStatus> =
+ Compare.byEnum(taintStatus);
+
+const taintStatusTags_internal: Server.GetRequest<null,tag[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.taintStatusTags',
+ input: Json.jNull,
+ output: Json.jList(jTag),
+};
+/** Registered tags for the above type. */
+export const taintStatusTags: Server.GetRequest<null,tag[]>= taintStatusTags_internal;
+
+/** Data for array rows [`properties`](#properties) */
+export interface propertiesData {
+ /** Entry identifier. */
+ key: Json.key<'#property'>;
+ /** Is the property invalid in some context of the analysis? */
+ priority: boolean;
+ /** Is the property tainted according to the Eva taint domain? */
+ taint: taintStatus;
+}
+
+/** Loose decoder for `propertiesData` */
+export const jPropertiesData: Json.Loose<propertiesData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey<'#property'>('#property'),'#property expected'),
+ priority: Json.jFail(Json.jBoolean,'Boolean expected'),
+ taint: jTaintStatusSafe,
+ });
+
+/** Safe decoder for `propertiesData` */
+export const jPropertiesDataSafe: Json.Safe<propertiesData> =
+ Json.jFail(jPropertiesData,'PropertiesData expected');
+
+/** Natural order for `propertiesData` */
+export const byPropertiesData: Compare.Order<propertiesData> =
+ Compare.byFields
+ <{ key: Json.key<'#property'>, priority: boolean, taint: taintStatus }>({
+ key: Compare.string,
+ priority: Compare.boolean,
+ taint: byTaintStatus,
+ });
+
+/** Signal for array [`properties`](#properties) */
+export const signalProperties: Server.Signal = {
+ name: 'plugins.eva.general.signalProperties',
+};
+
+const reloadProperties_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.reloadProperties',
+ input: Json.jNull,
+ output: Json.jNull,
+};
+/** Force full reload for array [`properties`](#properties) */
+export const reloadProperties: Server.GetRequest<null,null>= reloadProperties_internal;
+
+const fetchProperties_internal: Server.GetRequest<
+ number,
+ { pending: number, updated: propertiesData[],
+ removed: Json.key<'#property'>[], reload: boolean }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.fetchProperties',
+ input: Json.jNumber,
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jPropertiesData),
+ removed: Json.jList(Json.jKey<'#property'>('#property')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
+};
+/** Data fetcher for array [`properties`](#properties) */
+export const fetchProperties: Server.GetRequest<
+ number,
+ { pending: number, updated: propertiesData[],
+ removed: Json.key<'#property'>[], reload: boolean }
+ >= fetchProperties_internal;
+
+const properties_internal: State.Array<Json.key<'#property'>,propertiesData> = {
+ name: 'plugins.eva.general.properties',
+ getkey: ((d:propertiesData) => d.key),
+ signal: signalProperties,
+ fetch: fetchProperties,
+ reload: reloadProperties,
+ order: byPropertiesData,
+};
+/** Status of Registered Properties */
+export const properties: State.Array<Json.key<'#property'>,propertiesData> = properties_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 13e7ff4172851521ebdee5a2719c3e46b7853823..18c8c5ac5006fc6d6f633d657d547343933515d5 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -32,6 +32,7 @@ import * as States from 'frama-c/states';
import * as Compare from 'dome/data/compare';
import * as Settings from 'dome/data/settings';
import { Label, Code } from 'dome/controls/labels';
+import { Icon } from 'dome/controls/icons';
import { IconButton, Checkbox } from 'dome/controls/buttons';
import * as Models from 'dome/table/models';
import * as Arrays from 'dome/table/arrays';
@@ -42,8 +43,11 @@ import { Scroll, Folder } from 'dome/layout/boxes';
import { RSplit } from 'dome/layout/splitters';
import { source as SourceLoc } from 'frama-c/api/kernel/services';
-import { statusData as Property } from 'frama-c/api/kernel/properties';
+import { statusData } from 'frama-c/api/kernel/properties';
import * as Properties from 'frama-c/api/kernel/properties';
+import * as Eva from 'frama-c/api/plugins/eva/general';
+
+type Property = statusData & Eva.propertiesData;
// --------------------------------------------------------------------------
// --- Filters
@@ -94,6 +98,8 @@ const DEFAULTS: { [key: string]: boolean } = {
'alarms.function_pointer': true,
'alarms.union_initialization': true,
'alarms.bool_value': true,
+ 'eva.priority_only': false,
+ 'eva.tainted_only': false,
};
function filter(path: string) {
@@ -193,10 +199,21 @@ function filterAlarm(alarm: string | undefined) {
return filter('alarms.others');
}
+function filterEva(p: Property) {
+ let b = true;
+ if (p.priority === false && filter('eva.priority_only'))
+ b = false;
+ if ((p.taint === 'not_tainted' || p.taint === 'not_applicable')
+ && filter('eva.tainted_only'))
+ b = false;
+ return b;
+}
+
function filterProperty(p: Property) {
return filterStatus(p.status)
- && filterKind(p.kind)
- && filterAlarm(p.alarm);
+ && filterKind(p.kind)
+ && filterAlarm(p.alarm)
+ && filterEva(p);
}
// --------------------------------------------------------------------------
@@ -225,6 +242,22 @@ const renderFile: Renderer<SourceLoc> =
<Code className="code-column" label={loc.base} title={loc.file} />
);
+const renderPriority: Renderer<boolean> =
+ (prio: boolean) => (prio ? <Icon id="ATTENTION" /> : null);
+
+const renderTaint: Renderer<any> =
+ (taint: States.Tag) => {
+ let id = null;
+ let color = 'black';
+ switch (taint.name) {
+ case 'not_tainted': id = 'DROP.EMPTY'; color = '#00B900'; break;
+ case 'tainted': id = 'DROP.FILLED'; color = '#FF8300'; break;
+ case 'error': id = 'HELP'; break;
+ default:
+ }
+ return (id ? <Icon id={id} fill={color} title={taint.descr} /> : null);
+ };
+
function ColumnCode<Row>(props: ColumnProps<Row, string>) {
return <Column render={renderCode} {...props} />;
}
@@ -265,6 +298,8 @@ const byProperty: Compare.ByFields<Property> = {
predicate: Compare.defined(Compare.alpha),
key: Compare.string,
kinstr: Compare.structural,
+ priority: Compare.structural,
+ taint: Compare.structural,
};
const byDir = Compare.byFields<SourceLoc>({ dir: Compare.alpha });
@@ -323,6 +358,8 @@ function Section(props: SectionProps) {
interface CheckFieldProps {
label: string;
+ title?: string;
+ highligh?: boolean; // Highlights the label when the value is [highligh]
path: string;
}
@@ -331,8 +368,12 @@ function CheckField(props: CheckFieldProps) {
const onChange = () => { setValue(); Reload.emit(); };
return (
<Checkbox
- style={{ display: 'block' }}
+ style={{
+ display: 'block',
+ color: (props.highligh === value) ? 'red' : '',
+ }}
label={props.label}
+ title={props.title}
value={value}
onChange={onChange}
/>
@@ -396,6 +437,18 @@ function PropertyFilter() {
<CheckField label="Overlaps" path="alarms.overlap" />
<CheckField label="Initialization of unions" path="alarms.union_initialization" />
</Section>
+ <Section label="Eva">
+ <CheckField
+ label="High-priority only"
+ path="eva.priority_only"
+ title="Show only high-priority properties for the Eva analysis"
+ />
+ <CheckField
+ label="Tainted only"
+ path="eva.tainted_only"
+ title="Show only tainted properties according to the Eva taint domain"
+ />
+ </Section>
</Scroll>
);
}
@@ -411,6 +464,7 @@ const PropertyColumns = () => {
const statusDict = States.useTags(Properties.propStatusTags);
const kindDict = States.useTags(Properties.propKindTags);
const alarmDict = States.useTags(Properties.alarmsTags);
+ const taintDict = States.useTags(Eva.taintStatusTags);
const getStatus = React.useCallback(
({ status: st }: Property) => (statusDict.get(st) ?? { name: st }),
@@ -429,6 +483,11 @@ const PropertyColumns = () => {
[alarmDict],
);
+ const getTaint = React.useCallback(
+ ({ taint }: Property) => (taintDict.get(taint) ?? { name: taint }),
+ [taintDict],
+ );
+
return (
<>
<Column
@@ -458,6 +517,28 @@ const PropertyColumns = () => {
/>
<ColumnCode id="predicate" label="Predicate" fill />
<ColumnCode id="descr" label="Property" fill visible={false} />
+ <Column
+ id="priority"
+ label="Priority"
+ title="Properties invalid in some context of the Eva analysis"
+ icon="ATTENTION"
+ width={30}
+ visible={false}
+ align="center"
+ getter={(prop: Eva.propertiesData) => prop?.priority}
+ render={renderPriority}
+ />
+ <ColumnTag
+ id="taint"
+ label="Taint"
+ title="Properties tainted according to the Eva taint domain"
+ icon="PAINTBRUSH"
+ width={30}
+ visible={false}
+ align="center"
+ getter={getTaint}
+ render={renderTaint}
+ />
<ColumnTag
id="status"
label="Status"
@@ -493,12 +574,17 @@ export default function RenderProperties() {
// Hooks
const model = React.useMemo(() => new PropertyModel(), []);
- const data = States.useSyncArray(Properties.status).getArray();
+ const kernelData = States.useSyncArray(Properties.status).getArray();
+ const evaData = States.useSyncArray(Eva.properties).getArray();
useEffect(() => {
model.removeAllData();
+ const data = new Array(kernelData.length);
+ for (let i = 0; i < kernelData.length; i++) {
+ data[i] = { ...kernelData[i], ...evaData[i] };
+ }
model.updateData(data);
model.reload();
- }, [model, data]);
+ }, [model, kernelData, evaData]);
const [selection, updateSelection] = States.useSelection();
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 298ad6fe8eed25d5da9f1c0a0b0d8d56141dd2cf..64bc3512a2b8c077dfd7a522fc00790edcf1c64c 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -502,7 +502,7 @@ module Value = struct
Callstack.Hashtbl.add by_callstack cs state
let get_initial_state kf =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
try Called_Functions_Memo.find kf
with Not_found ->
let state =
@@ -517,8 +517,9 @@ module Value = struct
Called_Functions_Memo.add kf state;
state
+ (* This function is used by the Inout plugin during Eva analysis, so it
+ should not fail during Eva analysis, even if results are incomplete. *)
let get_initial_state_callstack kf =
- assert (is_computed ()); (* this assertion fails during value analysis *)
try Some (Called_Functions_By_Callstack.find kf)
with Not_found -> None
@@ -568,28 +569,28 @@ module Value = struct
noassert_get_stmt_state ~after s
let get_stmt_state ?(after=false) s =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
noassert_get_stmt_state ~after s
let get_state ?(after=false) k =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
noassert_get_state ~after k
let get_stmt_state_callstack ~after stmt =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
try
Some (if after then AfterTable_By_Callstack.find stmt else
Table_By_Callstack.find stmt)
with Not_found -> None
let fold_stmt_state_callstack f acc ~after stmt =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
match get_stmt_state_callstack ~after stmt with
| None -> acc
| Some h -> Value_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
let fold_state_callstack f acc ~after ki =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
match ki with
| Kglobal -> f (globals_state ()) acc
| Kstmt stmt -> fold_stmt_state_callstack f acc ~after stmt
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 082623df4cebc301120cad492e68bd270ef5bb88..534bee463c92d8665d56f5b438d6ca7a5851f08f 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -84,6 +84,8 @@ struct
let t_lemma = t_kind "lemma" "Logical lemma"
let t_check_lemma = t_kind "check_lemma" "Logical check lemma"
+ let t_ext = t_kind "extension" "ACSL extension"
+
let p_ext = Enum.prefix kinds ~name:"ext" ~var:"<clause>"
~descr:(Md.plain "ACSL extension `<clause>`")
@@ -107,7 +109,7 @@ struct
| PKEnsures(_,Returns) -> t_returns
| PKTerminates -> t_terminates
end
- | IPExtended { ie_ext={ ext_name } } -> Enum.instance p_ext ext_name
+ | IPExtended { ie_ext={ ext_name=_ } } -> t_ext
| IPAxiomatic _ -> t_axiomatic
| IPLemma { il_pred = { tp_kind = Admit } } -> t_axiom
| IPLemma { il_pred = { tp_kind = Assert } } -> t_lemma
@@ -127,7 +129,7 @@ struct
| AAssigns _ -> t_loop_assigns
| AAllocation _ -> t_loop_allocates
| APragma _ -> t_loop_pragma
- | AExtended(_,_,{ext_name}) -> Enum.instance p_loop_ext ext_name
+ | AExtended(_,_,{ext_name=_}) -> t_ext
end
| IPAllocation _ -> t_allocates
| IPAssigns _ -> t_assigns
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 66c110104c2f5047316685b75c2adfa0f3bddffa..075e7e7f88a2c69843272f1fcf5fa5255b20e4e3 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -119,4 +119,81 @@ let () = Request.register ~package
~output:(module DeadCode)
dead_code
+
+(* ----- Red and tainted alarms --------------------------------------------- *)
+
+
+module Taint = struct
+ open Server.Data
+ open Taint_domain
+
+ let dictionary = Enum.dictionary ()
+
+ let tag value name label descr =
+ Enum.tag ~name
+ ~label:(Markdown.plain label)
+ ~descr:(Markdown.plain descr) ~value dictionary
+
+ let tag_not_computed =
+ tag (Error NotComputed) "not_computed" ""
+ "The Eva taint analysis has not been computed"
+
+ let tag_error =
+ tag (Error LogicError) "error" "Error"
+ "Error: the memory zone on which this property depends could not be computed"
+
+ let tag_not_applicable =
+ tag (Error Irrelevant) "not_applicable" "—"
+ "No taint for this kind of property"
+
+ let tag_tainted =
+ tag (Ok true) "tainted" "yes"
+ "Tainted property: this property is related to a memory zone that \
+ can be affected by an attacker, according to the Eva taint domain"
+
+ let tag_not_tainted =
+ tag (Ok false) "not_tainted" "no"
+ "Untainted property: this property is safe, \
+ according to the Eva taint domain"
+
+ let () = Enum.set_lookup dictionary
+ begin function
+ | Error Taint_domain.NotComputed -> tag_not_computed
+ | Error Taint_domain.Irrelevant -> tag_not_applicable
+ | Error Taint_domain.LogicError -> tag_error
+ | Ok true -> tag_tainted
+ | Ok false -> tag_not_tainted
+ end
+
+ let data = Request.dictionary ~package ~name:"taintStatus"
+ ~descr:(Markdown.plain "Taint status of logical properties") dictionary
+
+ include (val data : S with type t = (bool, taint_error) result)
+end
+
+
+let model = States.model ()
+
+let () = States.column model ~name:"priority"
+ ~descr:(Markdown.plain "Is the property invalid in some context \
+ of the analysis?")
+ ~data:(module Data.Jbool)
+ ~get:(fun ip -> Red_statuses.is_red ip)
+
+let () = States.column model ~name:"taint"
+ ~descr:(Markdown.plain "Is the property tainted according to \
+ the Eva taint domain?")
+ ~data:(module Taint)
+ ~get:(fun ip -> Taint_domain.is_tainted_property ip)
+
+let _array =
+ States.register_array
+ ~package
+ ~name:"properties"
+ ~descr:(Markdown.plain "Status of Registered Properties")
+ ~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
+ ~keyType:Kernel_ast.Marker.jproperty
+ ~iter:Property_status.iter
+ model
+
(**************************************************************************)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 3bc961572d72b56d63387af68454bccf5321e833..80abee069ddbf66e854c3852c71e984751c2c637 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -499,6 +499,8 @@ module State = struct
| None -> `Bottom
else `Top
+ let mark_as_computed = Db.Value.mark_as_computed
+ let is_computed = Db.Value.is_computed
end
let display ?fmt kf =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index d5b24f78bd2119db70670d9f3344fb9b03660559..24a1b2effb86cb319813b9cbdc7826ba8f50e04f 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -629,5 +629,7 @@ module Restrict
let get_stmt_state_by_callstack ~after stmt =
inject_table (Domain.Store.get_stmt_state_by_callstack ~after stmt)
+ let mark_as_computed = Domain.Store.mark_as_computed
+ let is_computed = Domain.Store.is_computed
end
end
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 3adc09a45327fa56e9b929c6e6e79404de03b14a..3069d90b752a5aee918f5169532921b8d364e705 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -364,6 +364,11 @@ module Make
and right_tbl = Right.Store.get_stmt_state_by_callstack ~after stmt in
merge_callstack_tbl left_tbl right_tbl
+ let mark_as_computed () =
+ Left.Store.mark_as_computed ();
+ Right.Store.mark_as_computed ()
+
+ let is_computed () = Left.Store.is_computed () && Right.Store.is_computed ()
end
let post_analysis = function
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 9cf5b92d0dbe587e4b08e77cd62805473327b779..716bb29bb57404a8f56baf0ed268f1e1684ff6d9 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -46,6 +46,9 @@ module type S = sig
val get_stmt_state: after:bool -> stmt -> t or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_or_bottom
+
+ val mark_as_computed: unit -> unit
+ val is_computed: unit -> bool
end
module Make (Domain: InputDomain) = struct
@@ -267,4 +270,6 @@ module Make (Domain: InputDomain) = struct
if Storage.get ()
then update_callstack_table ~after:true stmt callstack state
+ let mark_as_computed () = Table_By_Callstack.mark_as_computed ()
+ let is_computed () = Storage.get () && Table_By_Callstack.is_computed ()
end
diff --git a/src/plugins/value/domains/domain_store.mli b/src/plugins/value/domains/domain_store.mli
index 2417beb53f67fcfa81718142a9b7d20bb5728251..aac671baeec92680e7317bf83599393e0ebaf170 100644
--- a/src/plugins/value/domains/domain_store.mli
+++ b/src/plugins/value/domains/domain_store.mli
@@ -53,6 +53,9 @@ module type S = sig
val get_stmt_state: after:bool -> stmt -> t or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_or_bottom
+
+ val mark_as_computed: unit -> unit
+ val is_computed: unit -> bool
end
module Make (Domain : InputDomain) : S with type t := Domain.t
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index f48720413afd88d24c32ddf9d66a7754d5b0c655..ae137312ca71732afc9d0a420e23fdd51aca29c4 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -559,3 +559,45 @@ let flag =
Abstractions.register ~name ~descr ~experimental abstraction
let () = Abstractions.register_hook interpret_taint_logic
+
+
+type taint_error = NotComputed | Irrelevant | LogicError
+
+let zone_of_predicate env predicate =
+ let logic_deps = Eval_terms.predicate_deps env predicate in
+ let deps_list = Option.map Logic_label.Map.bindings logic_deps in
+ match deps_list with
+ | Some [ BuiltinLabel Here, zone ] -> Ok zone
+ | _ -> Error LogicError
+
+let get_predicate = function
+ | Property.IPCodeAnnot ica ->
+ begin
+ match ica.ica_ca.annot_content with
+ | AAssert (_, predicate) | AInvariant (_, _, predicate) ->
+ Ok predicate.tp_statement
+ | _ -> Error Irrelevant
+ end
+ | IPPropertyInstance { ii_pred = None } -> Error LogicError
+ | IPPropertyInstance { ii_pred = Some pred } -> Ok pred.ip_content.tp_statement
+ | _ -> Error Irrelevant
+
+let get_stmt ip =
+ let kinstr = Property.get_kinstr ip in
+ match kinstr with
+ | Kglobal -> Error Irrelevant
+ | Kstmt stmt -> Ok stmt
+
+let is_tainted_property ip =
+ let (let+) = Result.bind in
+ if not (Store.is_computed ()) then Error NotComputed else
+ let+ stmt = get_stmt ip in
+ let+ predicate = get_predicate ip in
+ match Store.get_stmt_state ~after:false stmt with
+ | `Bottom -> Ok false
+ | `Value state ->
+ let cvalue = Db.Value.get_stmt_state ~after:false stmt in
+ let env = Eval_terms.env_only_here cvalue in
+ let+ zone = zone_of_predicate env predicate in
+ let tainted = Zone.intersects zone state.locs_data in
+ Ok tainted
diff --git a/src/plugins/value/domains/taint_domain.mli b/src/plugins/value/domains/taint_domain.mli
index 9c56182033a67f5b66dbb83016deda4140863cd8..c77b897f5261739218eac5da790f18e06fd8ce32 100644
--- a/src/plugins/value/domains/taint_domain.mli
+++ b/src/plugins/value/domains/taint_domain.mli
@@ -27,3 +27,13 @@ include Abstract_domain.Leaf
and type location = Precise_locs.precise_location
val flag: Abstractions.flag
+
+type taint_error =
+ | NotComputed (** The Eva analysis has not been run, or the taint domain
+ was not enabled. *)
+ | Irrelevant (** Properties other than assertions, invariants and
+ preconditions are irrelevant here. *)
+ | LogicError (** The memory zone on which the property depends could not
+ be computed. *)
+
+val is_tainted_property: Property.t -> (bool, taint_error) result
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 4d517e199e2d2d44ea209f1a875ec0cf0d17a054..64f0a75318804c193951839e840b741787f50122 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -82,8 +82,7 @@ let pre_analysis () =
degeneration states *)
Value_util.DegenerationPoints.clear ();
Cvalue.V.clear_garbled_mix ();
- Value_util.clear_call_stack ();
- Db.Value.mark_as_computed ()
+ Value_util.clear_call_stack ()
let post_analysis_cleanup ~aborted =
Value_util.clear_call_stack ();
@@ -341,11 +340,13 @@ module Make (Abstract: Abstractions.Eva) = struct
let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
Value_util.pop_call_stack ();
Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
+ Abstract.Dom.Store.mark_as_computed ();
post_analysis ();
Abstract.Dom.post_analysis final_state;
Value_results.print_summary ();
with
| Db.Value.Aborted ->
+ Abstract.Dom.Store.mark_as_computed ();
post_analysis_cleanup ~aborted:true;
(* Signal that a degeneration occurred *)
if Value_util.DegenerationPoints.length () > 0 then
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 930c01942de58d96d47e0845553c4b4e9e249415..30680db8febe393703da2ba94fb8893bc40beccd 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -782,7 +782,6 @@ module Computer
with Db.Value.Aborted as e ->
(* analysis was aborted: pop the call stack and inform the caller *)
Dataflow.mark_degeneration ();
- Db.Value.mark_as_computed ();
Dataflow.merge_results ();
raise e
end
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index f57c412722830a9d1258773b1338a1df9eb57f72..42440721ae25d8f7b25c9e1809bc32bb6c808c6a 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -94,6 +94,24 @@ let add_red_property ki ip =
add_red_ap Kglobal (Prop ip')
| _ -> add_red_ap ki (Prop ip)
+let is_red ip =
+ let kinstr = Property.get_kinstr ip in
+ let ap =
+ match ip with
+ | Property.IPCodeAnnot ica ->
+ begin
+ match Alarms.find ica.ica_ca with
+ | Some a -> Alarm a
+ | None -> Prop ip
+ end
+ | _ -> Prop ip
+ in
+ try
+ let map = RedStatusesTable.find kinstr in
+ let callstacks = AlarmOrProp.Map.find ap map in
+ not (Callstacks.is_empty callstacks)
+ with Not_found -> false
+
let is_red_in_callstack kinstr ap callstack =
try
let map = RedStatusesTable.find kinstr in
diff --git a/src/plugins/value/utils/red_statuses.mli b/src/plugins/value/utils/red_statuses.mli
index b8443410be9fd6fa73169dfc9f436216640c759c..0a9f5f0f41622c062b23380ccac705afc6db186a 100644
--- a/src/plugins/value/utils/red_statuses.mli
+++ b/src/plugins/value/utils/red_statuses.mli
@@ -34,6 +34,9 @@ type alarm_or_property = Alarm of Alarms.t | Prop of Property.t
module AlarmOrProp : Datatype.S with type t := alarm_or_property
+(* Whether a red status has been emitted for a property in any callstack. *)
+val is_red: Property.t -> bool
+
(* Whether a red status has been emitted for an alarm or a property at the given
kinstr in the given callstack. *)
val is_red_in_callstack: