goto-synthesizer cannot handle empty loop

[tautschnig]

CBMC version: current develop (cf084e6)
Operating system: Ubuntu 20.04
Exact command line resulting in the issue:

goto-cc main.c
goto-instrument --pointer-check a.out a.out
goto-synthesizer --dump-loop-contracts a.out

What behaviour did you expect: no violated invariant
What happened instead:

I tried running goto-synthesizer on https://github.com/diffblue/2ls/blob/master/regression/memsafety/simple_true/main.c with the above sequence of commands and got:

Reading GOTO program from 'a.out'
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-synthesizer/synthesizer_utils.cpp:31 function: get_loop_end_from_loop_head_and_content
Condition: loop_head != loop_end
Reason: Could not find end of the loop starting at: file main.c line 8 function exit
Backtrace:
[...]
Aborted (core dumped)

Also, I tried to replace the loop in line 8 by __CPROVER_assume(0);. This got me a new invariant failure:

Reading GOTO program from 'a.out'
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-synthesizer/cegis_verifier.cpp:195 function: get_cause_loop_id_for_assigns
Condition: !result.empty()
Reason: The assignable violation is not in a loop.
Backtrace:
[...]
--- end invariant violation report ---
Aborted (core dumped)

[qinheping]

Hi Michael, I fixed the first issue in #7602, and found that the cause of the second issue is the lack of alias analysis to infer/synthesize assigns target with type ID_member---we now only infer alias for lhs with type ID_dereference. For example, in the following program

#include <stdlib.h>

typedef struct node
{
  int h;
  struct node *n;
} *List;

int main()
{
  List t = (List)malloc(sizeof(struct node));
  List end = (List)malloc(sizeof(struct node));
  while(__VERIFIER_nondet_int())
    {
      t = end;
      t->n = 0;
    }
}

We write to t and t->n in the loop. However, the assigns clause should be

__CPROVER_assigns(t, end->n)

instead of (t, t->n), which infered by the current assigns inference algorithm. I will create another issue for this problem.

[qinheping]

Also, another blocker of synthesizing loop contracts for the problem in the link is allocating memory in loops. We don't support is_fresh and shape analysis in loop contracts yet.