Comments (5)
Yes, you should be able to implement that dataflow analysis without much effort.
As an example you can look at the code of the liveness analysis.
Just for curiosity, why do you need reaching definitions?
Coming from LLVM bitcode we never had the need for doing that.
from crab.
Hello caballa, thank you for your response!
I skimmed the code and implemented the reaching definitions analysis using the same varset_domain as in liveness.hpp.
It does work for an intraprocedural example, however, I am interested in the respective basic blocks not the variables.
If I use the default basic_block_label_t a compile error is thrown in write(crab::crab_os &o) of patricia_trees.hpp because it uses it->write(o); which is not defined on std::string.
If I create a wrapping class inheriting from writeable and overload the crab::cfg_impl::get_label_str(T e) I get even more compile errors, boiling down to my class not being derived from ikos::XXX.
Do you have a small example at hand how I can use crab::domains::flat_killgen_domain; with V being my basic_block_label_t?
Just for curiosity, why do you need reaching definitions?
I am currently tinkering with regression testing for a language similar to PASCAL. The test cases are generated using some kind of coverage criterion, either structural such as branch coverage or property-based, by converting the program under test into a set of horn clauses and quering z3 spacer for a counter-example which serves as the witness for testing.
I thought the program dependence graph could help me in order to identify which parts of the code are affected by a change, such that I can identify obsolete test cases and regenerate the test cases affected by the change.
I am still reading literature on this topic, so I can not really tell if that is the correct way to do it.
from crab.
I looked at the code and all examples use variable
as the template parameter for flat_killgen_domain
. But you were going in the right direction. You just need a wrapper that implements two operations index_t index() const
and void write(crab_os &) const
.
Btw, I strongly recommend you to use the branch dev
. Apart from the fact that it's the development branch and we plan to make it master
really soon, there are new features that might help you. I would still perform the dataflow analysis using a crab variable. Then I would keep separately a map from definitions (variables) to crab statements. From there, a crab statement has a new method get_parent()
that gives you the basic block.
from crab.
Hello caballa, I appreciate your input. I decided against wrapping the basic_block_label_t
in a class deriving from indexable
. I also switched the branch to dev
, thank you for the hint.
Using a map from variables to statements is not straightforward as basic_block
returns references to statement_t
, which is an abstract class. I could not bother to type-cast every statement_t
into its respective type using either the m_stmt_code
or a custom statement_visitor
, so I decided to use a variable to basic block map.
This allows me to compute kill and gen maps inside the analyze function and derive an out map relating each variable to the respective reaching definition of the corresponding basic block. The computed out map will be used as the in map for the next call to analyze. However, this obviously does not work in the general case.
What breaks my neck is the merge(varset_domain_t d1, varset_domain_t d2)
function and handling in and out maps with regards to varset_domain_t
.
I simply can not find a way to control this information on the reaching_definitions_analysis_operations
layer -- even though it is possible to map from basic_block_label_t
to varset_domain_t
and retrieve the corresponding in and out maps, I never know whether I am merging information before analyze
or afterwards. One could use a boolean flag to indicate whether analyze
was called to be certain that merge
is called on the in or out map, but then again it makes it even more hacky :/
I think my best bet would be to create a basic block label factory and use the indexed strings as the domain for the killgen_api. That way, I do not need to keep auxillary maps for conversion and the merging shouldn't be a problem either. What do you think?
from crab.
Something quick, sorry I don't have much time this morning.
The lattice for reaching definitions is an environment (i.e., map) from variables to a set of definitions. A definition typically is identified as the instruction where that definition happens (probably a pointer to statement_t
is a good choice in your case). This is the textbook way. I think what you are trying to do is far too complicated.
You mention that it's a problem for you that statement_t
is an abstract class, why? Note two things about statement_t
- the
statement_t
class has an ID that tells which statement actually is so you can always do static casts so performance is not an issue. You can also use the visitor class as you mentioned. - the
statement_t
class has two key methods for you:defs()
anduses()
that says which variables are defined and used. So I don't think you really need to caststatement_t
to their derived classes. You can usedefs()
to know which variables are defined by the statement. I think typically is only one definition at most but calls can return multiple outputs so they can define multiple variables.
from crab.
Related Issues (20)
- Make generic weights of adaptative sparse graph
- More precise bitwise AND HOT 1
- Valgrind warnings HOT 1
- none-optional dereference on array-expansion domain with elina-pk HOT 3
- Elina does not compile on mac: `'stdlib.h' file not found` HOT 4
- Enhance top-down inter-procedural analysis HOT 1
- CMake Options
- Does crab support running on MacOS? HOT 8
- Question: "range of intervals" HOT 14
- How to correctly represent "else" when manually working with `powerset_domain` HOT 9
- Compiler warning with `dev` HOT 1
- "compress" `powerset_domain` domain after projection HOT 4
- General question on "backward_assign_operations" HOT 1
- Question regarding the CFG input encoding for the analysis HOT 7
- Create tree expressions and adapt abstract domains to use them
- Question regarding "cyclic" encoding and propagation of analysis results HOT 9
- What is the difference between the wrapped_interval implemented in crab and the one implemented in TOPLAS15 paper? HOT 2
- Should we add the bitwise complement (~) operation in Crab? HOT 2
- Bug in flat_boolean_domain HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from crab.