Comments (11)
Replacing '.'
in the variable names will be necessary in java test case generation, as it is not allowed in java identfiers. Doing it already before would reduce work there, too.
from cbmc.
I have added regression/cbmc-java/recursion1 for this.
from cbmc.
I'm afraid recursion is still broken: see #163.
from cbmc.
tail recursion does work:
public class recursion1
{
static int f(int n)
{
if(n <= 0)
return 1;
else
return n * f(n-1);
}
static int g(int n, int acc)
{
if(n <= 0)
return acc;
else
return g(n-1, n*acc);
}
public static void main(String[] args)
{
assert f(1)==1;
assert g(1, 1) == 1;
}
}
from cbmc.
Seems likely that the cause is Java locals not getting declared or added to the symtab (while temp variables are registered), so goto_symext::locality
doesn't spot it as a thing to rename at inlining sites. However straightforwardly adding symbol registration and variable declaration in the same way as new_tmp_symbol
doesn't seem to fix matters.
from cbmc.
Doh. ssa_exprt.h:73
assumes that identifiers can't contain periods, but Java package names do, leading to symbol identifiers like package.function::arg0, leading to a bad l1 object identifier and use of the wrong version of a variable.
Solutions:
(1) Escape Java package identifiers (I bet there are some sites looking for last-instance-of-period to find a class name that'll need finding and fixing)
(2) Allow periods in identifier names. Likely there are more places in the codebase that don't like them?
(1) sounds like marginally less pain. Put an assert in the symtab / symbol_exprt code to check for a legal name on registration / lookup.
In the meantime flipping #if 0
at line 67 results in correct behaviour. @kroening want to give an opinion of god on this?
Note that the fix for locality above is still required however, but it takes a slightly different test case to show it.
from cbmc.
smowton@48118d5: Local variable registration
smowton@3f8bab9: Workaround to tolerate Java IDs
smowton@75e46e8: Test case exhibiting need for local registration (otherwise int arg_copy
gets overwritten by the recursive call)
from cbmc.
@mgudemann at the symtab level we'll need to use something illegal in Java IDs anyhow though, otherwise the uniqueing to avoid clashes between e.g. java_lang_Object_equals
and a local that actually has that name will drive us insane
I won't make the change right now since I'm about to go on holiday and it'd seem rude to do it and leave everyone to find all the knock-on consequences, so for now just noting it needs doing :)
from cbmc.
Fixed in Cristina's test_gen branch
from cbmc.
@kroening having taken a fresh look at this today, possible options:
- Mangle Java (and other language) names to remove syntactic ambiguity for struct member vs. namespace (i.e.
s/./::/
) (substantial cleanup of every instance using.
to find the class/namespace boundary) - Change
ssa_exprt::build_identifier
to use a different character for the object/member boundary (less natural, risk of code assuming that.
is used) - Change
ssa_exprt::build_identifier
to store the L1 object identifier, or its offset, as a separate attribute ofssa_exprt
(extra memory usage)
Any preference?
from cbmc.
No comment being forthcoming, how about just doing this: https://github.com/smowton/cbmc/tree/ssa_l1_id
from cbmc.
Related Issues (20)
- CBMC contracts crash when dynamic allocation is not in the harness. HOT 5
- Non-termination of proof on simple array copy example HOT 3
- CBMC 6.0.0-preview fails with mal-formed SMT HOT 13
- Opened in error - apologies. Please delete or close.
- CBMC-6.0.0 fails if local variable name overloads name of quantified variable in contract HOT 2
- no bounds check assertion HOT 1
- Unwind Issue: How to make a loop inductive? HOT 49
- aarch64: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE HOT 1
- goto-cc 6.0.0 fails compilation of s2n-tls unit on Linux, but works on macOS HOT 10
- Simple error message if --smt2 set and no Z3 on PATH HOT 1
- Non-termination of CBMC on use of size_t as type of a quantified variable HOT 14
- Simple modular reasoning example with contracts fails HOT 9
- List of C/C++ Compiler Support HOT 1
- centos compile cbmc 6.0.1 failed HOT 6
- Model loop invariant with __CPROVER_loop_entry and __CPROVER_loop_old HOT 4
- Multiplication of complex number is modelled incorrectly HOT 1
- Bitwuzla reports error on simple function verification HOT 1
- Run CBMC regression tests with Bitwuzla HOT 1
- Big performance regression of cbmc --cover in 6.0.1 HOT 7
- goto-instrument for k-induction fails invariant check on SV-COMP style single loop reachability problem
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 cbmc.