Skip to content

Remove invariant on full_lhs_value in printing goto_tracet #4153

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Remove invariant on full_lhs_value in printing goto_tracet #4153

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 0 additions & 3 deletions src/goto-programs/json_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,9 +132,6 @@ void convert_decl(
}
else
{
DATA_INVARIANT(
step.full_lhs_value.is_not_nil(),
"full_lhs_value in assignment must not be nil");
full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's already worth investigating why we even end up in this branch. That means that the symbol on the LHS is not in the namespace, which should only be happening if it is a symbol that symex has introduced. Even then that's got a justification for why the full_lhs_value should be nil. We've probably got some bug in goto-symex in that case, but I have no idea which one that is.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Am I correct in my understanding of this comment that this invariant should hold for both the branch where the symbol is found and when it is not?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that should be the case, yes - and that observation of yours might be the key to resolving this: either it is an invariant, or it should go away completely. For debugging purposes I'd suggest copying this into symex_target_equationt to figure out where the invariant is first violated.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added in symex_target_equationt::assignment the following invariants:

  DATA_INVARIANT(
    ssa_full_lhs.is_not_nil(),
    "full_lhs_value in assignment must not be nil");
  DATA_INVARIANT(
    original_full_lhs.is_not_nil(),
    "full_lhs_value in assignment must not be nil");
  DATA_INVARIANT(
    ssa_rhs.is_not_nil(),
    "full_lhs_value in assignment must not be nil");

And none of them trigger on the failing case (i.e. still see unknown in the trace). Is that what you meant? I can look at the assignment calls to see what these values are, but don't really know what I'd be looking for.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@thk123 Many thanks, that's good to know. Thus things must be going wrong in goto-symex/build_goto_trace.cpp line 344 I'd say. Would you mind inserting an appropriate invariant in there? I think we end up in boolbvt::bv_get_unbounded_array, which actually does return nil_exprt on a couple of branches (but I'm not sure that's a good idea). Actually there are quite a few occurrences of nil_exprt in solvers/flattening/boolbv_get.cpp. I'm not sure anyone of them is a good idea (and the hard-coded 100 in line 361 isn't good either). Could you work with @kroening to resolve this?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So it comes down to:

boolbvt::bv_get_unbounded_array

Which is failing to evaluate the size expr. The reason for this failure is the expression is (rewritten for readability):

if (&symex_dynamic::dynamic_object1 == constant(18000000000000))
  4;
else
  symex::invalid_object.length;

Note the constant exprt on the rhs of the if is:

constant
  * type: pointer
      * width: 64
  * value: 18000000000000
  0: address_of
      0: symbol
          * identifier: symex_dynamic::dynamic_object1
          * expression: symbol
              * identifier: symex_dynamic::dynamic_object1
          * #SSA_symbol: 1
          * L1_object_identifier: symex_dynamic::dynamic_object1

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So fixing the underling problem seems hard - the safe_pointers is not able to see through the GOTO:

        ASSUME !((struct java::array[reference] *)a == null) // Null pointer check
        ASSERT ((struct java::array[reference] *)a)->length >= 0 // Array size should be >= 0
        ASSUME ((struct java::array[reference] *)a)->length >= 0 // Array size should be >= 0
        newarray_tmp1 = ALLOCATE(struct java::array[float], 16ul, false);
        *newarray_tmp1 = { [email protected]={ .@class_identifier="java::array[float]" },
    .length=0, .data=null };
        newarray_tmp1->length = ((struct java::array[reference] *)a)->length;

Obviously this can be fixed by maybe making safe pointers smarter or the front end put the null check nearer, but shouldn't fundamentally a trace still be produced without a fix here? Should bv_get_unbounded_array stumble on, looking up the array and disregarding the size? I don't think I have enough insight into the expected behaviour to realistically do this unfortunately.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have created #4197 to address the limitations in bv_get_unbounded_array. Input, and in particular tests would be very much appreciated.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

symbol on the LHS is not in the namespace, which should only be happening if it is a symbol that symex has introduced.

Even that shouldn't happen if the correct namespace was used (which at least the new goto-checker implementations should be doing).

}

Expand Down