Skip to content

Commit 8a95d32

Browse files
muralitawsmuralitaws
authored
Merge pull request diffblue#4 from lefanz-amazon/lefan-abstraction
variable name: change the way to identify an entity in json files, pl…
2 parents 71a8c78 + 544746b commit 8a95d32

13 files changed

+90
-64
lines changed

‎regression/abstraction/aws_array_eq.json

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_eq_harness.c/aws_array_eq_harness",
6-
"name": "rhs",
5+
"function": "aws_array_eq_harness",
6+
"name": "aws_array_eq_harness::1::rhs",
77
"shape": {
88
"indices": ["lhs_cncrt", "rhs_cncrt"],
99
"assumptions": [
@@ -24,18 +24,18 @@
2424
"related-entities": [
2525
{
2626
"entity": "array",
27-
"path": "aws_array_eq_harness.c/aws_array_eq_harness",
28-
"name": "lhs"
27+
"function": "aws_array_eq_harness",
28+
"name": "aws_array_eq_harness::1::lhs"
2929
},
3030
{
3131
"entity": "scalar",
32-
"path": "aws_array_eq_harness.c/aws_array_eq_harness",
33-
"name": "rhs_len"
32+
"function": "aws_array_eq_harness",
33+
"name": "aws_array_eq_harness::1::rhs_len"
3434
},
3535
{
3636
"entity": "scalar",
37-
"path": "aws_array_eq_harness.c/aws_array_eq_harness",
38-
"name": "lhs_len"
37+
"function": "aws_array_eq_harness",
38+
"name": "aws_array_eq_harness::1::lhs_len"
3939
}
4040
]
4141

‎regression/abstraction/aws_array_eq_c_str_ignore_case.json

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
6-
"name": "c_str",
5+
"function": "aws_array_eq_c_str_ignore_case_harness",
6+
"name": "aws_array_eq_c_str_ignore_case_harness::1::c_str",
77
"shape": {
88
"indices": ["cncrt", "clast"],
99
"assumptions": [
@@ -24,18 +24,18 @@
2424
"related-entities": [
2525
{
2626
"entity": "array",
27-
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
28-
"name": "array"
27+
"function": "aws_array_eq_c_str_ignore_case_harness",
28+
"name": "aws_array_eq_c_str_ignore_case_harness::1::array"
2929
},
3030
{
3131
"entity": "scalar",
32-
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
33-
"name": "array_len"
32+
"function": "aws_array_eq_c_str_ignore_case_harness",
33+
"name": "aws_array_eq_c_str_ignore_case_harness::1::array_len"
3434
},
3535
{
3636
"entity": "scalar",
37-
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
38-
"name": "str_len"
37+
"function": "aws_array_eq_c_str_ignore_case_harness",
38+
"name": "aws_array_eq_c_str_ignore_case_harness::1::str_len"
3939
}
4040
]
4141

‎regression/abstraction/aws_array_eq_ignore_case.json

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
6-
"name": "rhs",
5+
"function": "aws_array_eq_ignore_case_harness",
6+
"name": "aws_array_eq_ignore_case_harness::1::rhs",
77
"shape": {
88
"indices": ["cncrt"],
99
"assumptions": [
@@ -23,18 +23,18 @@
2323
"related-entities": [
2424
{
2525
"entity": "array",
26-
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
27-
"name": "lhs"
26+
"function": "aws_array_eq_ignore_case_harness",
27+
"name": "aws_array_eq_ignore_case_harness::1::lhs"
2828
},
2929
{
3030
"entity": "scalar",
31-
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
32-
"name": "rhs_len"
31+
"function": "aws_array_eq_ignore_case_harness",
32+
"name": "aws_array_eq_ignore_case_harness::1::rhs_len"
3333
},
3434
{
3535
"entity": "scalar",
36-
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
37-
"name": "lhs_len"
36+
"function": "aws_array_eq_ignore_case_harness",
37+
"name": "aws_array_eq_ignore_case_harness::1::lhs_len"
3838
}
3939
]
4040

‎regression/abstraction/aws_array_list_comparator_string.json

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
6-
"name": "str_a->bytes",
5+
"function": "aws_array_list_comparator_string_harness",
6+
"name": "aws_array_list_comparator_string::1::str_a->bytes",
77
"shape": {
88
"indices": ["cncrt"],
99
"assumptions": [
@@ -23,18 +23,18 @@
2323
"related-entities": [
2424
{
2525
"entity": "array",
26-
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
27-
"name": "str_b->bytes"
26+
"function": "aws_array_list_comparator_string_harness",
27+
"name": "aws_array_list_comparator_string::1::str_b->bytes"
2828
},
2929
{
3030
"entity": "scalar",
31-
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
32-
"name": "str_a->len"
31+
"function": "aws_array_list_comparator_string_harness",
32+
"name": "aws_array_list_comparator_string::1::str_a->len"
3333
},
3434
{
3535
"entity": "scalar",
36-
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
37-
"name": "str_b->len"
36+
"function": "aws_array_list_comparator_string_harness",
37+
"name": "aws_array_list_comparator_string::1::str_b->len"
3838
}
3939
]
4040

‎regression/abstraction/aws_array_list_front.json

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_list_front_harness.c/aws_array_list_front_harness",
6-
"name": "list->data",
5+
"function": "aws_array_list_front_harness",
6+
"name": "aws_array_list_front_harness::1::list->data",
77
"shape": {
88
"indices": ["front", "cncrt"],
99
"assumptions": [
@@ -25,8 +25,8 @@
2525
"related-entities": [
2626
{
2727
"entity": "scalar",
28-
"path": "aws_array_list_front_harness.c/aws_array_list_front_harness",
29-
"name": "list->length"
28+
"function": "aws_array_list_front_harness",
29+
"name": "aws_array_list_front_harness::1::list->length"
3030
}
3131
]
3232

‎regression/abstraction/aws_array_list_get_at.json

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_list_get_at_harness.c/aws_array_list_get_at_harness",
6-
"name": "list->data",
5+
"function": "aws_array_list_get_at_harness",
6+
"name": "aws_array_list_get_at_harness::1::list->data",
77
"shape": {
88
"indices": ["c0", "c1"],
99
"assumptions": [
@@ -24,8 +24,8 @@
2424
"related-entities": [
2525
{
2626
"entity": "scalar",
27-
"path": "aws_array_list_get_at_harness.c/aws_array_list_get_at_harness",
28-
"name": "list->length"
27+
"function": "aws_array_list_get_at_harness",
28+
"name": "aws_array_list_get_at_harness::1::list->length"
2929
}
3030
]
3131

‎regression/abstraction/aws_array_list_pop_back.json

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
"entries": [
33
{
44
"entity": "array",
5-
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
6-
"name": "list->data",
5+
"function": "aws_array_list_pop_back_harness",
6+
"name": "aws_array_list_pop_back_harness::1::list->data",
77
"shape": {
88
"indices": ["c0", "c1"],
99
"assumptions": [
@@ -24,18 +24,18 @@
2424
"related-entities": [
2525
{
2626
"entity": "array",
27-
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
28-
"name": "old->data"
27+
"function": "aws_array_list_pop_back_harness",
28+
"name": "aws_array_list_pop_back_harness::1::old->data"
2929
},
3030
{
3131
"entity": "scalar",
32-
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
33-
"name": "old->length"
32+
"function": "aws_array_list_pop_back_harness",
33+
"name": "aws_array_list_pop_back_harness::1::old->length"
3434
},
3535
{
3636
"entity": "scalar",
37-
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
38-
"name": "list->length"
37+
"function": "aws_array_list_pop_back_harness",
38+
"name": "aws_array_list_pop_back_harness::1::list->length"
3939
}
4040
]
4141

‎regression/abstraction/skip_string.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33
"entries": [
44
{
55
"entity": "array",
6-
"path": "string_harness",
7-
"name": "json",
6+
"function": "main",
7+
"name": "main::1::json",
88
"shape": {
99
"indices": ["c0", "c1", "c2", "c3"],
1010
"assumptions": [

‎src/goto-instrument/abstraction.cpp

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,7 @@ void link_abst_functions(goto_modelt &goto_model, const abstraction_spect &abst_
126126
link_goto_model(goto_model, goto_model_for_abst_fns, msg_handler); // link goto model
127127
}
128128

129-
void abstract_goto_program(goto_modelt &goto_model, jsont json)
129+
const std::unordered_set<irep_idt> find_index_symbols(goto_modelt &goto_model, const irep_idt &array_name)
130130
{
131131
class show_index_exprt : public expr_visitort
132132
{
@@ -187,22 +187,21 @@ void abstract_goto_program(goto_modelt &goto_model, jsont json)
187187
}
188188
};
189189

190-
irep_idt abst_array_id = json["array_name"].value;
190+
irep_idt abst_array_id = array_name;
191191

192192
expr_type_relation etr(abst_array_id);
193193

194194
// for each function, rename all references to that variable
195-
Forall_goto_functions(it, goto_model.goto_functions)
195+
forall_goto_functions(it, goto_model.goto_functions)
196196
{
197-
std::cout << "**" << it->first << std::endl;
198197
if(std::string(abst_array_id.c_str()).rfind((it->first).c_str(), 0) == 0)
199198
{
200199
// this function is the one that contains the target variable
201200
// it->second is the goto_functiont
202-
goto_functiont &goto_function = it->second;
201+
const goto_functiont &goto_function = it->second;
203202

204203
// for each instruction, we change the referenced name of the target variable
205-
Forall_goto_program_instructions(it, goto_function.body)
204+
forall_goto_program_instructions(it, goto_function.body)
206205
{
207206
// go through conditions
208207
if(it->has_condition())
@@ -233,6 +232,18 @@ void abstract_goto_program(goto_modelt &goto_model, jsont json)
233232
}
234233

235234
etr.solve();
236-
for(auto v: etr.get_abst_variables())
237-
std::cout << v << std::endl;
235+
return etr.get_abst_variables();
236+
}
237+
238+
void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec)
239+
{
240+
for(const abstraction_spect::spect &s: abst_spec.get_specs())
241+
{
242+
std::cout << "=== Analyzing " << s.name << " ===" << std::endl;
243+
const std::unordered_set<irep_idt> &index_symbols = find_index_symbols(goto_model, s.name);
244+
for(const auto &v: index_symbols)
245+
{
246+
std::cout << v << std::endl;
247+
}
248+
}
238249
}

‎src/goto-instrument/abstraction.h

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ class expr_type_relation
4545
void link(size_t i1, size_t i2);
4646
size_t add_expr(const exprt &expr);
4747
void solve();
48-
const std::unordered_set<irep_idt> & get_abst_variables()
48+
const std::unordered_set<irep_idt> get_abst_variables()
4949
{
5050
return abst_variables;
5151
}
@@ -54,7 +54,10 @@ class expr_type_relation
5454
// link abst functions to goto programs
5555
void link_abst_functions(goto_modelt &goto_model, const abstraction_spect &abst_spec, ui_message_handlert &msg_handler, const optionst &options);
5656

57+
// find related variables within function
58+
const std::unordered_set<irep_idt> find_index_symbols(goto_modelt &goto_model, const irep_idt &array_name);
59+
5760
// abstract goto programs
58-
void abstract_goto_program(goto_modelt &goto_model, jsont json);
61+
void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec);
5962

6063
#endif // CPROVER_GOTO_INSTRUMENT_ABSTRACTION_H

‎src/goto-instrument/abstraction_spect.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ abstraction_spect::abstraction_spect(
2323
for(const jsont &entry : to_json_array(json["entries"]))
2424
{
2525
spect spec;
26-
spec.path = entry["path"].value;
26+
spec.function = entry["function"].value;
2727
spec.name = entry["name"].value;
2828
spec.abst_func_file = get_absolute_path(entry["abst-function-file"].value);
2929
specs.push_back(spec);
@@ -38,4 +38,9 @@ std::vector<std::string> abstraction_spect::get_abstraction_function_files() con
3838
files.push_back(s.abst_func_file);
3939
}
4040
return (files);
41+
}
42+
43+
std::vector<abstraction_spect::spect> &abstraction_spect::get_specs()
44+
{
45+
return specs;
4146
}

‎src/goto-instrument/abstraction_spect.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,13 +27,13 @@ class abstraction_spect
2727
std::vector<std::string> get_abstraction_function_files() const;
2828

2929

30-
protected:
30+
public:
3131
struct spect
3232
{
3333
//Hierarchical path to the array/list being abstracted
34-
std::string path;
34+
std::string function; // function name, no need to have path
3535
//Name of the array/list being abstracted
36-
std::string name;
36+
std::string name; // should be in the id format: function::x::name
3737
//Abstraction func file
3838
std::string abst_func_file;
3939
//Names of references in increasing order
@@ -70,6 +70,10 @@ class abstraction_spect
7070

7171
};
7272

73+
// gather specs
74+
std::vector<spect> &get_specs();
75+
76+
protected:
7377
std::vector<spect> specs;
7478

7579

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1139,6 +1139,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11391139
log.status() << "Reading in abst funcs goto-model" << messaget::eom;
11401140
link_abst_functions(goto_model, abst_spec, ui_message_handler, options);
11411141
log.status() << "Abst functions linked to goto-program" << messaget::eom;
1142+
1143+
log.status() << "Analyzing index variables related to the entity" << messaget::eom;
1144+
abstract_goto_program(goto_model, abst_spec);
11421145
}
11431146

11441147
// all checks supported by goto_check

0 commit comments

Comments
 (0)