Java nondet test gen support #607
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Update test.desc files with correct outcomes Fix formatting issues
Update generic testcase
Remove test case with multiple test methods
Remove mistakenly-added txt files Fix formatting issues
Add nondet recursive expansion to typecheck_expr
Update nondet generic test cases
Removed CProver.class
The new block type is replaced by a nondet initializer during bytecode conversion and typechecking. Add missing test case Make small fixes to test cases Fix formatting issues
These tests don't work as expected at the moment, because nondetWithoutNull has not been implemented yet.
peterschrammel
requested changes
Mar 7, 2017
src/util/std_code.cpp
Outdated
| @@ -177,3 +177,4 @@ const codet &codet::last_statement() const | |||
|
|
|||
| return *this; | |||
| } | |||
|
|
|||
src/util/std_code.h
Outdated
| static inline const side_effect_expr_nondett & | ||
| to_side_effect_expr_nondet(const exprt &expr) | ||
| { | ||
| const auto &x = to_side_effect_expr(expr); |
src/util/std_code.h
Outdated
| static inline const side_effect_expr_nondett & | ||
| to_side_effect_expr_nondet(const exprt &expr) | ||
| { | ||
| const auto &x = to_side_effect_expr(expr); |
There was a problem hiding this comment.
better rename x to side_effect_expr
| @@ -47,11 +50,16 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr) | |||
| typecheck_expr_symbol(to_symbol_expr(expr)); | |||
| else if(expr.id()==ID_side_effect) | |||
| { | |||
| const irep_idt &statement=to_side_effect_expr(expr).get_statement(); | |||
| auto &side_effect_expr = to_side_effect_expr(expr); | |||
| @@ -43,7 +43,7 @@ class java_bytecode_typecheckt:public typecheckt | |||
| { | |||
| } | |||
|
|
|||
| virtual ~java_bytecode_typecheckt() { } | |||
| virtual ~java_bytecode_typecheckt() = default; | |||
There was a problem hiding this comment.
Let's keep the old version in this PR. We can change this consistently in the whole code base in separate PR.
| { | ||
| if(&(*it)==before_1) | ||
| { | ||
| assert(it+1!=end); |
There was a problem hiding this comment.
This makes an assumption about the implementation of exprt::operandst. Use a second iterator and increment to point at the next element.
| id_regex)) | ||
| { | ||
| assert(2<=parents.size()); | ||
| const auto before_1=*(parents.end()-1); |
There was a problem hiding this comment.
It's nicer to user decrements instead of pointer arithmetic here.
| template <typename Func> | ||
| static void traverse_expr_tree( | ||
| exprt &expr, | ||
| std::vector<exprt*> &parents, |
| std::vector<exprt*> &parents, | ||
| Func func) | ||
| { | ||
| const auto& parents_ref=parents; |
|
|
||
| \*******************************************************************/ | ||
|
|
||
| template <typename Func> |
There was a problem hiding this comment.
This function should go into util/expr_util.h
reuk
force-pushed
the
java-nondet-test-gen-support
branch
from
4671957 to
7fc5583
Compare
reuk
force-pushed
the
java-nondet-test-gen-support
branch
from
7fc5583 to
67697aa
Compare
|
There are failing tests: https://travis-ci.org/diffblue/cbmc/jobs/208984797#L1874 |
reuk
force-pushed
the
java-nondet-test-gen-support
branch
2 times, most recently
from
491ba2e to
08cb9f5
Compare
reuk
force-pushed
the
java-nondet-test-gen-support
branch
from
08cb9f5 to
101a65d
Compare
In the case where we really want to create a nondet java.lang.Object, the java compiler does not emit a checkcast instruction, which means that our attempt to divine the nondet type using checkcast fails. This commit changes the behaviour of nondetWithNull so that it will create an Object if the following instruction is not a checkcast. The test nondetCastToObject tests this behaviour.
reuk
force-pushed
the
java-nondet-test-gen-support
branch
from
ba4628e to
8321fa8
Compare
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Sep 6, 2018
Only allow "returnValue" value for location field in JSON rules file
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds support for modelling nondet values explicitly in Java code.
Tests demonstrating the new Java interface are located in
regression/cbmc-java/nondet*. For objects, the interface has been simplified:Foo f = CProver.nondetWithNull();Currently, all nondet objects may be initialised to
null, because of the opaque method stubbing behaviour. An extra methodCProver.nondetWithoutNull()could be added in the future, if the method stubbing were modified to allow non-null initialisation.The build succeeds but some of the added nondet tests fail.
The proper functioning of the code in this pull request depends on the opaque-stubbing behaviour (from java_opaque_method_stubs.h), which hasn't made its way into cbmc/test-gen-support yet. The feature will work properly once this feature is also merged in.