cprover
Loading...
Searching...
No Matches
api.cpp
Go to the documentation of this file.
1// Author: Fotis Koutoulakis for Diffblue Ltd.
2
3#include "api.h"
4
5#include <util/cmdline.h>
6#include <util/config.h>
7#include <util/invariant.h>
8#include <util/message.h>
9#include <util/options.h>
10#include <util/ui_message.h>
11#include <util/version.h>
12
21
24#include <ansi-c/gcc_version.h>
28#include <langapi/mode.h>
30
31#include <memory>
32#include <string>
33#include <vector>
34
35extern configt config;
36
37std::unique_ptr<std::string> api_sessiont::get_api_version() const
38{
40}
41
43{
44 std::unique_ptr<goto_modelt> model;
45 std::unique_ptr<message_handlert> message_handler;
46 std::unique_ptr<optionst> options;
47};
48
52
55{
58 implementation->options = options.to_engine_options();
59 // Needed to initialise the language options correctly
60 cmdlinet cmdline;
61 // config is global in config.cpp
62 config.set(cmdline);
63 // Initialise C language mode
65 // configure gcc, if required -- get_goto_program will have set the config
67 {
68 gcc_versiont gcc_version;
69 gcc_version.get("gcc");
70 configure_gcc(gcc_version);
71 }
72}
73
75
77{
78 std::string string;
79 unsigned level;
80};
81
82const char *api_message_get_string(const api_messaget &message)
83{
84 return message.string.c_str();
85}
86
88{
90}
91
93{
94public:
95 explicit api_message_handlert(
98
99 void print(unsigned level, const std::string &message) override;
100
101 // Unimplemented for now. We may need to implement these as string conversions
102 // or something later.
103 void print(unsigned level, const xmlt &xml) override{};
104 void print(unsigned level, const jsont &json) override{};
105
106 void flush(unsigned) override{};
107
108private:
111};
112
114 api_message_callbackt callback,
116 : message_handlert{}, context{context}, callback{callback}
117{
118}
119
120void api_message_handlert::print(unsigned level, const std::string &message)
121{
122 if(!callback)
123 return;
124 api_messaget api_message{message, level};
126}
127
135
142
143std::unique_ptr<verification_resultt> api_sessiont::verify_model() const
144{
146
148 if(empty_result)
149 {
150 return {};
151 }
152
153 return run_verifier();
154}
155
156void api_sessiont::read_goto_binary(std::string &file) const
157{
159 auto read_opt_val =
160 ::read_goto_binary(file, *implementation->message_handler);
161 if(read_opt_val.has_value())
162 {
163 implementation->model =
165 }
166 else
167 {
168 log.error() << "Unable to read goto-binary from file " << file
169 << messaget::eom;
170 }
171}
172
173bool api_sessiont::is_goto_binary(std::string &file) const
174{
175 return ::is_goto_binary(file, *implementation->message_handler);
176}
177
179{
180 // Remove inline assembler; this needs to happen before adding the library.
181 remove_asm(*implementation->model);
182
183 // add the library
185 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
186 << messaget::eom;
188 *implementation->model,
189 *implementation->message_handler,
191
192 // Common removal of types and complex constructs
194 *implementation->model, *implementation->options, log))
195 {
196 return true;
197 }
198
199 // add failed symbols
200 // needs to be done before pointer analysis
201 add_failed_symbols(implementation->model->symbol_table);
202
203 // label the assertions
204 // This must be done after adding assertions and
205 // before using the argument of the "property" option.
206 // Do not re-label after using the property slicer because
207 // this would cause the property identifiers to change.
209
211 return false;
212}
213
214std::unique_ptr<verification_resultt> api_sessiont::run_verifier() const
215{
216 ui_message_handlert ui_message_handler(*implementation->message_handler);
218 verifier(
219 *implementation->options, ui_message_handler, *implementation->model);
220
222 auto results = verifier();
223
224 // Print messages collected to callback buffer.
225 verifier.report();
226 // Set results object before returning.
227 result.set_result(results);
228
229 auto properties = verifier.get_properties();
230 result.set_properties(properties);
232}
233
235{
236 INVARIANT(
237 implementation->model != nullptr,
238 "Model has not been loaded. Load it first using "
239 "api::load_model_from_files");
240
242 log.status() << "Performing instrumentation pass: dropping unused functions"
243 << messaget::eom;
244
246 *implementation->model, *implementation->message_handler);
247}
248
250{
251 INVARIANT(
252 implementation->model != nullptr,
253 "Model has not been loaded. Load it first using "
254 "api::load_model_from_files");
255
257 log.status() << "Validating consistency of goto-model supplied to API session"
258 << messaget::eom;
259
260 implementation->model->validate();
261}
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Pointer Dereferencing.
Goto verifier for verifying all properties that stores traces.
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
std::unique_ptr< languaget > new_ansi_c_language()
bool api_message_is_error(const api_messaget &message)
Definition api.cpp:87
const char * api_message_get_string(const api_messaget &message)
Given a api_message, this function returns that message expressed as a C language string.
Definition api.cpp:82
configt config
Definition config.cpp:25
message_handlert & message_handler
Definition ai.h:522
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
api_message_callbackt callback
Definition api.cpp:110
api_call_back_contextt context
Definition api.cpp:109
void print(unsigned level, const std::string &message) override
Definition api.cpp:120
void print(unsigned level, const jsont &json) override
Definition api.cpp:104
void flush(unsigned) override
Definition api.cpp:106
api_message_handlert(api_message_callbackt callback, api_call_back_contextt context)
Definition api.cpp:113
void print(unsigned level, const xmlt &xml) override
Definition api.cpp:103
std::unique_ptr< optionst > to_engine_options() const
Globally accessible architectural configuration.
Definition config.h:129
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
Definition json.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
message_handlert * message_handler
Definition message.h:439
@ M_ERROR
Definition message.h:170
static eomt eom
Definition message.h:297
Definition xml.h:21
void configure_gcc(const gcc_versiont &gcc_version)
Symbol Table + CFG.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition mode.cpp:39
Goto Checker using Multi-Path Symbolic Execution.
Options.
bool process_goto_program(goto_modelt &goto_model, const optionst &options, messaget &log)
Common processing and simplification of goto_programts.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Read Goto Programs.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
unsigned level
Definition api.cpp:79
std::string string
Definition api.cpp:78
std::unique_ptr< goto_modelt > model
Definition api.cpp:44
std::unique_ptr< optionst > options
Definition api.cpp:46
std::unique_ptr< message_handlert > message_handler
Definition api.cpp:45
std::unique_ptr< std::string > get_api_version() const
A simple API version information function.
Definition api.cpp:37
std::unique_ptr< verification_resultt > run_verifier() const
Process the model by running symex and the decision procedure.
Definition api.cpp:214
bool preprocess_model() const
Implement necessary transformations to reduce model to symex-ready-GOTO, before being fed to symex.
Definition api.cpp:178
void load_model_from_files(const std::vector< std::string > &files) const
Load a goto_model from a given vector of filenames.
Definition api.cpp:136
bool is_goto_binary(std::string &file) const
True if file is goto-binary.
Definition api.cpp:173
std::unique_ptr< verification_resultt > verify_model() const
Definition api.cpp:143
void set_message_callback(api_message_callbackt callback, api_call_back_contextt context)
Definition api.cpp:128
void drop_unused_functions() const
Drop unused functions from the loaded goto_model simplifying it.
Definition api.cpp:234
void validate_goto_model() const
Validate the loaded goto model.
Definition api.cpp:249
std::unique_ptr< api_session_implementationt > implementation
Definition api.h:100
api_sessiont()
Definition api.cpp:49
void read_goto_binary(std::string &file) const
Read a goto-binary from a given filename.
Definition api.cpp:156
Definition kdev_t.h:19
void set_result(resultt &result)
void set_properties(propertiest &properties)
const char * CBMC_VERSION