Skip to content

Commit 71a8c78

Browse files
author
Lefan Zhang
authored
Merge pull request diffblue#3 from lefanz-amazon/lefan-abstraction
abstration: actually link abst functions specified in json files into
2 parents 91ebd42 + d2abec9 commit 71a8c78

15 files changed

+148
-67
lines changed

‎regression/abstraction/aws_array_eq.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,15 @@
1111
],
1212
"shape-type": "*c+c*"
1313
},
14+
"abst-function-file": "./abst-funcs.c",
1415
"abst-functions":{
15-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17-
"precise-check": "../abst-funcs.c/is_precise",
18-
"abstract-index": "../abst-funcs.c/four_abs",
19-
"concretize-index": "../abst-funcs.c/concretize",
20-
"multiply-indices": "none",
21-
"mod-indices": "none"
16+
"add-abs-conc": "add_abs_to_conc",
17+
"sub-abs-conc": "sub_conc_from_abs",
18+
"precise-check": "is_precise",
19+
"abstract-index": "four_abs",
20+
"concretize-index": "concretize",
21+
"multiply-indices": null,
22+
"mod-indices": null
2223
},
2324
"related-entities": [
2425
{

‎regression/abstraction/aws_array_eq_c_str_ignore_case.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,15 @@
1111
],
1212
"shape-type": "*c*c*"
1313
},
14+
"abst-function-file": "./abst-funcs.c",
1415
"abst-functions":{
15-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17-
"precise-check": "../abst-funcs.c/is_precise",
18-
"abstract-index": "../abst-funcs.c/two_abs",
19-
"concretize-index": "../abst-funcs.c/concretize",
20-
"multiply-indices": "none",
21-
"mod-indices": "none"
16+
"add-abs-conc": "add_abs_to_conc",
17+
"sub-abs-conc": "sub_conc_from_abs",
18+
"precise-check": "is_precise",
19+
"abstract-index": "two_abs",
20+
"concretize-index": "concretize",
21+
"multiply-indices": null,
22+
"mod-indices": null
2223
},
2324
"related-entities": [
2425
{

‎regression/abstraction/aws_array_eq_ignore_case.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,15 @@
1010
],
1111
"shape-type": "*c*"
1212
},
13+
"abst-function-file": "./abst-funcs.c",
1314
"abst-functions":{
14-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
15-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
16-
"precise-check": "../abst-funcs.c/is_precise",
17-
"abstract-index": "../abst-funcs.c/one_abs",
18-
"concretize-index": "../abst-funcs.c/concretize",
19-
"multiply-indices": "none",
20-
"mod-indices": "none"
15+
"add-abs-conc": "add_abs_to_conc",
16+
"sub-abs-conc": "sub_conc_from_abs",
17+
"precise-check": "is_precise",
18+
"abstract-index": "one_abs",
19+
"concretize-index": "concretize",
20+
"multiply-indices": null,
21+
"mod-indices": null
2122
},
2223
"related-entities": [
2324
{

‎regression/abstraction/aws_array_list_comparator_string.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,15 @@
1010
],
1111
"shape-type": "*c*"
1212
},
13+
"abst-function-file": "./abst-funcs.c",
1314
"abst-functions":{
14-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
15-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
16-
"precise-check": "../abst-funcs.c/is_precise",
17-
"abstract-index": "../abst-funcs.c/one_abs",
18-
"concretize-index": "../abst-funcs.c/concretize",
19-
"multiply-indices": "none",
20-
"mod-indices": "none"
15+
"add-abs-conc": "add_abs_to_conc",
16+
"sub-abs-conc": "sub_conc_from_abs",
17+
"precise-check": "is_precise",
18+
"abstract-index": "one_abs",
19+
"concretize-index": "concretize",
20+
"multiply-indices": null,
21+
"mod-indices": null
2122
},
2223
"related-entities": [
2324
{

‎regression/abstraction/aws_array_list_front.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,14 +12,15 @@
1212
],
1313
"shape-type": "c*c*"
1414
},
15+
"abst-function-file": "./abst-funcs.c",
1516
"abst-functions":{
16-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
17-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
18-
"precise-check": "../abst-funcs.c/is_precise",
19-
"abstract-index": "../abst-funcs.c/two_abs",
20-
"concretize-index": "../abst-funcs.c/concretize",
21-
"multiply-indices": "none",
22-
"mod-indices": "none"
17+
"add-abs-conc": "add_abs_to_conc",
18+
"sub-abs-conc": "sub_conc_from_abs",
19+
"precise-check": "is_precise",
20+
"abstract-index": "two_abs",
21+
"concretize-index": "concretize",
22+
"multiply-indices": null,
23+
"mod-indices": null
2324
},
2425
"related-entities": [
2526
{

‎regression/abstraction/aws_array_list_get_at.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,15 @@
1111
],
1212
"shape-type": "*c*c*"
1313
},
14+
"abst-function-file": "./abst-funcs.c",
1415
"abst-functions":{
15-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17-
"precise-check": "../abst-funcs.c/is_precise",
18-
"abstract-index": "../abst-funcs.c/two_abs",
19-
"concretize-index": "../abst-funcs.c/concretize",
20-
"multiply-indices": "none",
21-
"mod-indices": "none"
16+
"add-abs-conc": "add_abs_to_conc",
17+
"sub-abs-conc": "sub_conc_from_abs",
18+
"precise-check": "is_precise",
19+
"abstract-index": "two_abs",
20+
"concretize-index": "concretize",
21+
"multiply-indices": null,
22+
"mod-indices": null
2223
},
2324
"related-entities": [
2425
{

‎regression/abstraction/aws_array_list_pop_back.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,15 @@
1111
],
1212
"shape-type": "*cc*"
1313
},
14+
"abst-function-file": "./abst-funcs.c",
1415
"abst-functions":{
15-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17-
"precise-check": "../abst-funcs.c/is_precise",
18-
"abstract-index": "../abst-funcs.c/two_abs",
19-
"concretize-index": "../abst-funcs.c/concretize",
20-
"multiply-indices": "none",
21-
"mod-indices": "none"
16+
"add-abs-conc": "add_abs_to_conc",
17+
"sub-abs-conc": "sub_conc_from_abs",
18+
"precise-check": "is_precise",
19+
"abstract-index": "two_abs",
20+
"concretize-index": "concretize",
21+
"multiply-indices": null,
22+
"mod-indices": null
2223
},
2324
"related-entities": [
2425
{

‎regression/abstraction/skip_string.json

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,15 @@
1414
],
1515
"shape-type": "*cc+cc*"
1616
},
17+
"abst-function-file": "./abst-funcs.c",
1718
"abst-functions":{
18-
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
19-
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
20-
"precise-check": "../abst-funcs.c/is_precise",
21-
"abstract-index": "../abst-funcs.c/four_abs",
22-
"concretize-index": "../abst-funcs.c/concretize",
23-
"multiply-indices": "none",
24-
"mod-indices": "none"
19+
"add-abs-conc": "add_abs_to_conc",
20+
"sub-abs-conc": "sub_conc_from_abs",
21+
"precise-check": "is_precise",
22+
"abstract-index": "four_abs",
23+
"concretize-index": "concretize",
24+
"multiply-indices": null,
25+
"mod-indices": null
2526
},
2627
"related-entities": []
2728
}

‎src/goto-instrument/abstraction.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Lefan Zhang, [email protected]
1414
#include <iostream>
1515

1616
#include <util/std_expr.h>
17+
#include <goto-programs/initialize_goto_model.h>
18+
#include <goto-programs/link_goto_model.h>
1719

1820
#include "abstraction.h"
1921

@@ -117,6 +119,13 @@ void expr_type_relation::solve()
117119
}
118120
}
119121

122+
void link_abst_functions(goto_modelt &goto_model, const abstraction_spect &abst_spec, ui_message_handlert &msg_handler, const optionst &options)
123+
{
124+
std::vector<std::string> abstfiles = abst_spec.get_abstraction_function_files(); // get abst function file names
125+
goto_modelt goto_model_for_abst_fns = initialize_goto_model(abstfiles, msg_handler, options); // read files
126+
link_goto_model(goto_model, goto_model_for_abst_fns, msg_handler); // link goto model
127+
}
128+
120129
void abstract_goto_program(goto_modelt &goto_model, jsont json)
121130
{
122131
class show_index_exprt : public expr_visitort

‎src/goto-instrument/abstraction.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,10 @@ Author: Lefan Zhang, [email protected]
1818
#include <util/json.h>
1919

2020
#include <goto-programs/goto_model.h>
21+
#include <util/ui_message.h>
22+
#include <util/options.h>
23+
24+
#include "abstraction_spect.h"
2125

2226
// class to find out type relations between exprs
2327
// this is used to identify symbols we need to abstract given a target array
@@ -47,6 +51,9 @@ class expr_type_relation
4751
}
4852
};
4953

54+
// link abst functions to goto programs
55+
void link_abst_functions(goto_modelt &goto_model, const abstraction_spect &abst_spec, ui_message_handlert &msg_handler, const optionst &options);
56+
5057
// abstract goto programs
5158
void abstract_goto_program(goto_modelt &goto_model, jsont json);
5259

‎src/goto-instrument/abstraction_spect.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Authors: Murali Talupur [email protected]
1010
#include <iostream>
1111

1212
#include <json/json_parser.h>
13+
#include <util/file_util.h>
1314

1415
#include "abstraction_spect.h"
1516

@@ -24,14 +25,17 @@ abstraction_spect::abstraction_spect(
2425
spect spec;
2526
spec.path = entry["path"].value;
2627
spec.name = entry["name"].value;
28+
spec.abst_func_file = get_absolute_path(entry["abst-function-file"].value);
2729
specs.push_back(spec);
2830
}
2931
}
3032

31-
std::vector<std::string> abstraction_spect::get_abstraction_function_files()
33+
std::vector<std::string> abstraction_spect::get_abstraction_function_files() const
3234
{
33-
std::string file =
34-
"/Users/talupur/workspaces/abstract-cbmc/cbmc/regression/abstraction";
35-
std::vector<std::string> files(1, file);
35+
std::vector<std::string> files;
36+
for (const spect &s: specs)
37+
{
38+
files.push_back(s.abst_func_file);
39+
}
3640
return (files);
3741
}

‎src/goto-instrument/abstraction_spect.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ class abstraction_spect
2424
abstraction_spect(std::string, message_handlert &);
2525

2626
//gathers file names from all the individual specs and returns a list.
27-
std::vector<std::string> get_abstraction_function_files();
27+
std::vector<std::string> get_abstraction_function_files() const;
2828

2929

3030
protected:

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,9 @@ Author: Daniel Kroening, [email protected]
3131
#include <goto-programs/goto_convert_functions.h>
3232
#include <goto-programs/goto_inline.h>
3333
#include <goto-programs/interpreter.h>
34+
#include <goto-programs/initialize_goto_model.h>
3435
#include <goto-programs/label_function_pointer_call_sites.h>
36+
#include <goto-programs/link_goto_model.h>
3537
#include <goto-programs/link_to_library.h>
3638
#include <goto-programs/loop_ids.h>
3739
#include <goto-programs/parameter_assignments.h>
@@ -82,6 +84,7 @@ Author: Daniel Kroening, [email protected]
8284
#include <cpp/cprover_library.h>
8385

8486
#include "abstraction.h"
87+
#include "abstraction_spect.h"
8588
#include "accelerate/accelerate.h"
8689
#include "alignment_checks.h"
8790
#include "branch.h"
@@ -762,14 +765,14 @@ int goto_instrument_parse_optionst::doit()
762765

763766
if(cmdline.isset("use-abstraction"))
764767
{
765-
std::string filename = cmdline.get_value("use-abstraction");
766-
jsont json;
767-
parse_json(filename, ui_message_handler, json);
768+
// std::string filename = cmdline.get_value("use-abstraction");
769+
// jsont json;
770+
// parse_json(filename, ui_message_handler, json);
768771

769-
abstract_goto_program(goto_model, json);
770-
std::cout << "abstract finished" << std::endl;
772+
// abstract_goto_program(goto_model, json);
773+
std::cout << "abstract" << std::endl;
771774

772-
return CPROVER_EXIT_SUCCESS;
775+
// return CPROVER_EXIT_SUCCESS;
773776
}
774777

775778
if(
@@ -1125,6 +1128,19 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11251128
else
11261129
options.set_option("assert-to-assume", false);
11271130

1131+
if(cmdline.isset("use-abstraction"))
1132+
{
1133+
std::string abs_file = cmdline.get_value("use-abstraction");
1134+
1135+
abstraction_spect abst_spec(abs_file, ui_message_handler);
1136+
1137+
std::vector<std::string> abstfiles = abst_spec.get_abstraction_function_files();
1138+
1139+
log.status() << "Reading in abst funcs goto-model" << messaget::eom;
1140+
link_abst_functions(goto_model, abst_spec, ui_message_handler, options);
1141+
log.status() << "Abst functions linked to goto-program" << messaget::eom;
1142+
}
1143+
11281144
// all checks supported by goto_check
11291145
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
11301146

‎src/util/file_util.cpp

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Date: January 2012
1717

1818
#include <cerrno>
1919
#include <cstring>
20+
#include <filesystem>
2021

2122
#if defined(__linux__) || \
2223
defined(__FreeBSD_kernel__) || \
@@ -77,6 +78,39 @@ std::string get_current_working_directory()
7778
return working_directory;
7879
}
7980

81+
/// \param rel_path: relative path
82+
/// \return absolute path
83+
std::string get_absolute_path(const std::string &rel_path)
84+
{
85+
#ifndef _WIN32
86+
errno=0;
87+
char rp[4096];
88+
strcpy(rp, rel_path.c_str());
89+
char *wd=realpath(rel_path.c_str(), nullptr);
90+
91+
if(wd == nullptr || errno != 0)
92+
throw system_exceptiont(
93+
std::string("realpath failed: ") + std::strerror(errno));
94+
95+
std::string abs_path=wd;
96+
free(wd);
97+
#else
98+
TCHAR buffer[4096];
99+
DWORD retval=GetFullPathName(rel_path, 4096, buffer, "")
100+
if(retval == 0)
101+
throw system_exceptiont("failed to get current directory of process");
102+
103+
# ifdef UNICODE
104+
std::string abs_path(narrow(buffer));
105+
# else
106+
std::string abs_path(buffer);
107+
# endif
108+
109+
#endif
110+
111+
return abs_path;
112+
}
113+
80114
/// Set working directory.
81115
/// \param path: New working directory to change to
82116
void set_current_path(const std::string &path)

‎src/util/file_util.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@ void delete_directory(const std::string &path);
2020
std::string get_current_working_directory();
2121
void set_current_path(const std::string &path);
2222

23+
// C++17 will allow us to use std::filesystem::absolute
24+
std::string get_absolute_path(const std::string &rel_path);
25+
2326
// C++17 will allow us to use std::filesystem::path(dir).append(file)
2427
std::string concat_dir_file(const std::string &directory,
2528
const std::string &file_name);

0 commit comments

Comments
 (0)