add parameter for depth of recursive objects #567
Conversation
2ad3479 to
0c8aded
Compare
There was a problem hiding this comment.
I'm not convinced this is the correct algorithm. The commit message should mention that this fixes #561.
| @@ -1153,6 +1153,8 @@ void cbmc_parse_optionst::help() | |||
| " --classpath dir/jar set the classpath\n" | |||
| " --main-class class-name set the name of the main class\n" | |||
| // NOLINTNEXTLINE(whitespace/line_length) | |||
| "--java-max-recursion-depth max recursion depth for nondet init of recursive objects\n" | |||
There was a problem hiding this comment.
While I do accept that the initialisation code currently exists for Java only: I don't think this command-line option should remain as specific. Furthermore the option name suggests that functional recursion is limited, whereas this is all about object initialisation. How about: "recursive-object-bound"?
|
|
||
| return; | ||
| if(recursion_depth<max_recursion_depth) | ||
| recursion_depth++; |
There was a problem hiding this comment.
Isn't this going to count the total number of recursive steps, across multiple "branches" of the data structures? For instance, for mutual recursion, the number of objects of a type X would actually just be max_recursion_depth/2.
There was a problem hiding this comment.
@mgudemann, what is the intended semantics of the parameter? I agree with @tautschnig that the current solution is rather unintuitive from the user's perspective.
There was a problem hiding this comment.
There is a problem with null initialization of objects. In the original implementation, a recursion set was used that would in an object hierarchy prevent instantiation of object types already seen. There were cases where this was problematic, if an object contained a recursive instantation, effectively this lead to a null value and due to various options (--assertions-as-assumptions etc.) created an ASSUME non null for that exact member, leading to inconsistent model.
The idea of this parameter was to create a solution between using exclusively the recursion set and not using it at all, i.e., having a bounded initialization of hierarchical objects.
There was a problem hiding this comment.
Shouldn't the solution be passing the recursion_depth as a parameter? Decrement (or increment) it on each recursive call, and check for 0 (respectively a chosen maximum). Yes, you need the recursion set to detect the fact that you are doing a recursive step, but counters need to be branch-specific, not global across the structure.
There was a problem hiding this comment.
you are perfectly right with this
The original implementation could enter an infinite loop for recursive objects, this patch adds a maximal recursion depth to prevent this and at the same time to allow for having non-null object members.
0c8aded to
259c59d
Compare
|
done in #824 |
…ng-base Don't add bases that aren't defined in the trace file
The original implementation could enter an infinite loop for recursive objects,
this patch adds a maximal recursion depth to prevent this and at the same time
to allow for having non-null object members.
fixes #561