Skip to content

Commit cf788d7

Browse files
martin-csmartin-cs
authored
Merge pull request #5637 from jezhiggins/flow-insensitivity-option
VSD flow insensitivity option
2 parents e24faec + 6631b23 commit cf788d7

File tree

20 files changed

+416
-241
lines changed

20 files changed

+416
-241
lines changed

‎regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
3+
int fun(int other)
4+
{
5+
if(other > 0)
6+
{
7+
int value = fun(other - 1);
8+
return value + 1;
9+
}
10+
else
11+
{
12+
return 0;
13+
}
14+
}
15+
16+
int main(int argc, char *argv[])
17+
{
18+
int z = fun(0);
19+
assert(
20+
z ==
21+
0); // Unknown as flow-insensitive fails to stop the recursive case being explored
22+
}

‎regression/goto-analyzer/flow-insensitive-function-call-recursive/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-flow-insensitive --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] .* assertion z == 0: UNKNOWN$
7+
--
8+
^warning: ignoring

‎regression/goto-analyzer/flow-insensitive-if/main.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
int y = 1;
6+
int z;
7+
if(y)
8+
{
9+
assert(y != 0);
10+
z = 1;
11+
}
12+
else
13+
{
14+
assert(y == 0);
15+
z = 0;
16+
}
17+
assert(z == 1);
18+
}

‎regression/goto-analyzer/flow-insensitive-if/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-flow-insensitive --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
7+
^\[main\.assertion\.2\] .* assertion y == 0: FAILURE \(if reachable\)$
8+
^\[main\.assertion\.3\] .* assertion z == 1: UNKNOWN$
9+
--
10+
^warning: ignoring

‎regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
3+
int fun(int other)
4+
{
5+
if(other > 0)
6+
{
7+
int value = fun(other - 1);
8+
return value + 1;
9+
}
10+
else
11+
{
12+
return 0;
13+
}
14+
}
15+
16+
int main(int argc, char *argv[])
17+
{
18+
int z = fun(0);
19+
assert(z == 0); // Success because flow-sensitivity blocks the branch
20+
}

‎regression/goto-analyzer/flow-sensitive-function-call-recursive/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] .* assertion z == 0: SUCCESS$
7+
--
8+
^warning: ignoring

‎regression/goto-analyzer/flow-sensitive-if/main.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
int y = 1;
6+
int z;
7+
if(y)
8+
{
9+
assert(y != 0);
10+
z = 1;
11+
}
12+
else
13+
{
14+
assert(y == 0);
15+
z = 0;
16+
}
17+
assert(z == 1);
18+
}

‎regression/goto-analyzer/flow-sensitive-if/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
7+
^\[main\.assertion\.2\] .* assertion y == 0: SUCCESS \(unreachable\)$
8+
^\[main\.assertion\.3\] .* assertion z == 1: SUCCESS$
9+
--
10+
^warning: ignoring

‎src/analyses/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ SRC = ai.cpp \
6060
variable-sensitivity/value_set_pointer_abstract_object.cpp \
6161
variable-sensitivity/value_set_array_abstract_object.cpp \
6262
variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
63+
variable-sensitivity/variable_sensitivity_configuration.cpp \
6364
# Empty last line
6465

6566
INCLUDES= -I ..

‎src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
/*******************************************************************\
2+
3+
Module: variable sensitivity domain configuration
4+
5+
Author: Jez Higgins
6+
7+
\*******************************************************************/
8+
/// \file
9+
/// Captures the user-supplied configuration for VSD, determining which
10+
/// domain abstractions are used, flow sensitivity, etc
11+
#include "variable_sensitivity_configuration.h"
12+
13+
vsd_configt vsd_configt::from_options(const optionst &options)
14+
{
15+
vsd_configt config{};
16+
17+
if(
18+
options.get_bool_option("value-set") &&
19+
options.get_bool_option("data-dependencies"))
20+
{
21+
throw invalid_command_line_argument_exceptiont{
22+
"Value set is not currently supported with data dependency analysis",
23+
"--value-set --data-dependencies",
24+
"--data-dependencies"};
25+
}
26+
27+
config.value_abstract_type =
28+
option_to_abstract_type(options, "values", value_option_mappings, CONSTANT);
29+
30+
config.pointer_abstract_type = option_to_abstract_type(
31+
options, "pointers", pointer_option_mappings, POINTER_INSENSITIVE);
32+
33+
config.struct_abstract_type = option_to_abstract_type(
34+
options, "structs", struct_option_mappings, STRUCT_INSENSITIVE);
35+
36+
config.array_abstract_type = option_to_abstract_type(
37+
options, "arrays", array_option_mappings, ARRAY_INSENSITIVE);
38+
39+
config.union_abstract_type = option_to_abstract_type(
40+
options, "unions", union_option_mappings, UNION_INSENSITIVE);
41+
42+
// This should always be on (for efficeny with 3-way merge)
43+
// Does not work with value set
44+
config.context_tracking.last_write_context =
45+
(config.value_abstract_type != VALUE_SET) &&
46+
(config.pointer_abstract_type != VALUE_SET);
47+
config.context_tracking.data_dependency_context =
48+
options.get_bool_option("data-dependencies");
49+
config.advanced_sensitivities.new_value_set =
50+
options.get_bool_option("new-value-set");
51+
52+
config.flow_sensitivity = (options.get_bool_option("flow-insensitive"))
53+
? flow_sensitivityt::insensitive
54+
: flow_sensitivityt::sensitive;
55+
56+
return config;
57+
}
58+
59+
vsd_configt vsd_configt::constant_domain()
60+
{
61+
vsd_configt config{};
62+
config.context_tracking.last_write_context = true;
63+
config.value_abstract_type = CONSTANT;
64+
config.pointer_abstract_type = POINTER_SENSITIVE;
65+
config.struct_abstract_type = STRUCT_SENSITIVE;
66+
config.array_abstract_type = ARRAY_SENSITIVE;
67+
return config;
68+
}
69+
70+
vsd_configt vsd_configt::value_set()
71+
{
72+
vsd_configt config{};
73+
config.value_abstract_type = VALUE_SET;
74+
config.pointer_abstract_type = VALUE_SET;
75+
config.struct_abstract_type = STRUCT_SENSITIVE;
76+
config.array_abstract_type = ARRAY_SENSITIVE;
77+
return config;
78+
}
79+
80+
vsd_configt vsd_configt::intervals()
81+
{
82+
vsd_configt config{};
83+
config.context_tracking.last_write_context = true;
84+
config.value_abstract_type = INTERVAL;
85+
config.pointer_abstract_type = POINTER_SENSITIVE;
86+
config.struct_abstract_type = STRUCT_SENSITIVE;
87+
config.array_abstract_type = ARRAY_SENSITIVE;
88+
return config;
89+
}
90+
91+
const vsd_configt::option_mappingt vsd_configt::value_option_mappings = {
92+
{"intervals", INTERVAL},
93+
{"constants", CONSTANT},
94+
{"set-of-constants", VALUE_SET}};
95+
96+
const vsd_configt::option_mappingt vsd_configt::pointer_option_mappings = {
97+
{"top-bottom", POINTER_INSENSITIVE},
98+
{"constants", POINTER_SENSITIVE},
99+
{"value-set", VALUE_SET}};
100+
101+
const vsd_configt::option_mappingt vsd_configt::struct_option_mappings = {
102+
{"top-bottom", STRUCT_INSENSITIVE},
103+
{"every-field", STRUCT_SENSITIVE}};
104+
105+
const vsd_configt::option_mappingt vsd_configt::array_option_mappings = {
106+
{"top-bottom", ARRAY_INSENSITIVE},
107+
{"every-element", ARRAY_SENSITIVE}};
108+
109+
const vsd_configt::option_mappingt vsd_configt::union_option_mappings = {
110+
{"top-bottom", UNION_INSENSITIVE}};
111+
112+
invalid_command_line_argument_exceptiont vsd_configt::invalid_argument(
113+
const std::string &option_name,
114+
const std::string &bad_argument,
115+
const option_mappingt &mapping)
116+
{
117+
auto option = "--vsd-" + option_name;
118+
auto choices = std::string("");
119+
for(auto &kv : mapping)
120+
{
121+
choices += (!choices.empty() ? "|" : "");
122+
choices += kv.first;
123+
}
124+
125+
return invalid_command_line_argument_exceptiont{
126+
"Unknown argument '" + bad_argument + "'", option, option + " " + choices};
127+
}
128+
129+
ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type(
130+
const optionst &options,
131+
const std::string &option_name,
132+
const option_mappingt &mapping,
133+
ABSTRACT_OBJECT_TYPET default_type)
134+
{
135+
const auto argument = options.get_option(option_name);
136+
137+
if(argument.empty())
138+
return default_type;
139+
140+
auto selected = mapping.find(argument);
141+
if(selected == mapping.end())
142+
{
143+
throw invalid_argument(option_name, argument, mapping);
144+
}
145+
return selected->second;
146+
}

‎src/analyses/variable-sensitivity/variable_sensitivity_configuration.h

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
/*******************************************************************\
2+
3+
Module: variable sensitivity configuration
4+
5+
Author: Jez Higgins
6+
7+
\*******************************************************************/
8+
/// \file
9+
/// Captures the user-supplied configuration for VSD, determining which
10+
/// domain abstractions are used, flow sensitivity, etc
11+
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
12+
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
13+
14+
#include <util/exception_utils.h>
15+
#include <util/options.h>
16+
17+
enum ABSTRACT_OBJECT_TYPET
18+
{
19+
TWO_VALUE,
20+
CONSTANT,
21+
INTERVAL,
22+
ARRAY_SENSITIVE,
23+
ARRAY_INSENSITIVE,
24+
POINTER_SENSITIVE,
25+
POINTER_INSENSITIVE,
26+
STRUCT_SENSITIVE,
27+
STRUCT_INSENSITIVE,
28+
// TODO: plug in UNION_SENSITIVE HERE
29+
UNION_INSENSITIVE,
30+
VALUE_SET
31+
};
32+
33+
enum class flow_sensitivityt
34+
{
35+
sensitive,
36+
insensitive
37+
};
38+
39+
struct vsd_configt
40+
{
41+
ABSTRACT_OBJECT_TYPET value_abstract_type;
42+
ABSTRACT_OBJECT_TYPET pointer_abstract_type;
43+
ABSTRACT_OBJECT_TYPET struct_abstract_type;
44+
ABSTRACT_OBJECT_TYPET array_abstract_type;
45+
ABSTRACT_OBJECT_TYPET union_abstract_type;
46+
47+
flow_sensitivityt flow_sensitivity;
48+
49+
struct
50+
{
51+
bool data_dependency_context;
52+
bool last_write_context;
53+
} context_tracking;
54+
55+
struct
56+
{
57+
bool new_value_set;
58+
} advanced_sensitivities;
59+
60+
static vsd_configt from_options(const optionst &options);
61+
62+
static vsd_configt constant_domain();
63+
static vsd_configt value_set();
64+
static vsd_configt intervals();
65+
66+
vsd_configt()
67+
: value_abstract_type{CONSTANT},
68+
pointer_abstract_type{POINTER_INSENSITIVE},
69+
struct_abstract_type{STRUCT_INSENSITIVE},
70+
array_abstract_type{ARRAY_INSENSITIVE},
71+
union_abstract_type{UNION_INSENSITIVE},
72+
flow_sensitivity{flow_sensitivityt::sensitive},
73+
context_tracking{false, true},
74+
advanced_sensitivities{false}
75+
{
76+
}
77+
78+
private:
79+
using option_mappingt = std::map<std::string, ABSTRACT_OBJECT_TYPET>;
80+
81+
static ABSTRACT_OBJECT_TYPET option_to_abstract_type(
82+
const optionst &options,
83+
const std::string &option_name,
84+
const option_mappingt &mapping,
85+
ABSTRACT_OBJECT_TYPET default_type);
86+
87+
static invalid_command_line_argument_exceptiont invalid_argument(
88+
const std::string &option_name,
89+
const std::string &bad_argument,
90+
const option_mappingt &mapping);
91+
92+
static const option_mappingt value_option_mappings;
93+
static const option_mappingt pointer_option_mappings;
94+
static const option_mappingt struct_option_mappings;
95+
static const option_mappingt array_option_mappings;
96+
static const option_mappingt union_option_mappings;
97+
};
98+
99+
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H // NOLINT(*)

0 commit comments

Comments
 (0)