Skip to content

Loop invariants cause va_list to fail #7199

@feliperodri

Description

@feliperodri

CBMC version: 5.67.0
Operating system: N/A

For the following program:

int my_f(int x, ...)
{
  __builtin_va_list list;
  __builtin_va_start(list, x);

  int value;
  unsigned i;

  for(i=0; i<x; i++)
  __CPROVER_loop_invariant (
     list == __CPROVER_loop_entry(list) + i && (value == 10 || i == 0)
  )
  {
    value=__builtin_va_arg(list, int);
  }
  return value;
}

int main()
{
  assert(my_f(1, 10)==10);
}

CBMC fails to prove that the invariant preserves.

I suppose the cause of failure is that __builtin_va_arg(p, int) is statically rewritten to va_args[j] where va_args is the build-in array of arguments. However, after havocing, p becomes a nondet pointer; hence __builtin_va_arg(p, int) cannot be correctly rewritten (and will be rewritten to symex::invalid_object!0#0 as an example).
To resolve the issue, we could rewrite __builtin_va_arg(p, int) to

  1. check if p is the same object as va_args: assert(same_object(p,va_args))
  2. check if the offset of p is valid: assert(offset(p) < object_size(va_args))
  3. substitute __builtin_va_arg(p, int) with (int)(*p)

Metadata

Metadata

Assignees

Labels

Code ContractsFunction and loop contractsawsBugs or features of importance to AWS CBMC usersbug

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions