Symex taint analysis #247
Symex taint analysis #247
Conversation
src/path-symex/path_symex_history.h
Outdated
| #include <limits> | ||
| #include <cassert> |
There was a problem hiding this comment.
What's the rationale for this change?
src/goto-programs/remove_ternary.h
Outdated
| #include <goto-programs/goto_model.h> | ||
|
|
||
| class remove_ternaryt | ||
| { |
There was a problem hiding this comment.
This class definition should probably be moved to the .cpp file as is done in other transformations.
src/goto-programs/remove_ternary.cpp
Outdated
| if(expr.id() == ID_code) | ||
| { | ||
| codet &code=to_code(expr); | ||
| if(to_code(expr).get_statement() == ID_assign) |
There was a problem hiding this comment.
Should use code instead of re-doing to_code(...)
src/goto-programs/remove_ternary.cpp
Outdated
| void remove_ternaryt::operator()(goto_functionst &goto_functions) | ||
| { | ||
| Forall_goto_functions(f_it, goto_functions){ | ||
| goto_programt &goto_program=f_it->second.body; |
src/goto-programs/remove_ternary.h
Outdated
|
|
||
| void contains_ternary(exprt &expr, bool &contains); | ||
|
|
||
| bool contains_ternary(exprt &expr); |
There was a problem hiding this comment.
Neither the "contains_ternary" nor "replaced" are used anywhere; the former is really dangerous as it will kill all sharing (well, actually contains_ternary would have to take a const exprt and be const).
src/path-symex/path_symex_state.h
Outdated
| @@ -13,15 +13,18 @@ Author: Daniel Kroening, [email protected] | |||
| #include "var_map.h" | |||
| #include "path_symex_history.h" | |||
|
|
|||
| #include <path-symex/path_symex_taint_data.h> | |||
There was a problem hiding this comment.
Use "path_symex_taint_data.h" for consistency
| assert(src.op0().op0().id() == ID_index); | ||
| assert(src.op0().op0().op0().id() == ID_string_constant); | ||
|
|
||
| dstring symbol_name=src.op0().op0().op0().get_string(ID_value); |
|
|
||
| #include "path_symex_taint_data.h" | ||
|
|
||
| taint_datat::taint_rulet::taint_rulet() |
There was a problem hiding this comment.
Use :loc(0), taint(0), ...
src/symex/path_search.cpp
Outdated
| @@ -36,10 +36,16 @@ path_searcht::resultt path_searcht::operator()( | |||
|
|
|||
| locs.build(goto_functions); | |||
|
|
|||
| // this is the container for the history-forest | |||
| // Perform a non-comprehensive check on JSON file. | |||
| if(taint_engine->enabled && | |||
There was a problem hiding this comment.
Isn't this lacking a test for taint_engine being non-null?
There was a problem hiding this comment.
Indeed. Is there a preferred syntax within CProver for checking for null-ness?
(C++ supports a few methods)
| @@ -41,6 +41,8 @@ class optionst; | |||
| "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ | |||
| "(show-locs)(show-vcc)(show-properties)(show-goto-functions)" \ | |||
| "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \ | |||
| "(taint):(show-taint-data)(taint-file):" \ | |||
| "(remove-ternary)" \ | |||
There was a problem hiding this comment.
--help output for all of these, please
|
Thanks Michael. Appreciated. Will sort. |
…ecks on taint_engine dereference.
|
@DanielNeville can you rebase, please, and comment whether you think this is ready to be reviewed? |
catch by const ref instead of by value or non-const ref
…ies-of-function-entry-points Control dependencies of function entry points
|
This is obsolete. Part of this apparently made it into the dependency analysis in VSD according to @chrisr-diffblue |
|
At the moment VSD doesn't do taint analysis. I think the larger issue is that the single-path symex was merged into the main CBMC. |
|
This seems to be for https://github.com/diffblue/symex, which was moved out of CBMC. |
Feedback and corrections welcomed.