Prevent empty arrays from being passed to the solver

[romainbrenguier]

Passing empty arrays causes segmentation fault.

[tautschnig]

1. Why are empty arrays even created?
2. Shouldn't there be a check in the place that does the conversion towards the SAT solver? (I am aware that there had previously been a PR that would catch this case in the SAT solver, which is too late.)

[romainbrenguier]

@tautschnig

Why are empty arrays even created?

What do you expect to get as a model for a symbol of type array which has size 0 ?

Shouldn't there be a check in the place that does the conversion towards the SAT solver? (I am aware that there had previously been a PR that would catch this case in the SAT solver, which is too late.)

What would be the result in that case? SAT/UNSAT/ERROR ?

[allredj]

Is there a Jira issue for that?
Can we create a regression test?

[allredj]

I love these iterators and lambda expressions!

[tautschnig]

What do you expect to get as a model for a symbol of type array which has size 0 ?

Ok, so these are part of the input? I wasn't aware of that.

What would be the result in that case? SAT/UNSAT/ERROR ?

If the code being touched here is the only layer between user input and the SAT solver then the changes as they are are good. If there is a further layer that does the conversion towards the SAT solver, then that code should be returning an ERROR (rather than a segmentation fault).

[romainbrenguier]

@allredj

Is there a Jira issue for that?

It's a problem I encountered while working on TG-592 but not directly related.

Can we create a regression test?

Actually I cannot find an example at the moment. I will make it into a precondition instead so that when it happens again, we have a better error message than just segmentation fault.

[martin-cs]

#include <assert.h>
#include <stdlib.h>

struct clause {
  int size;
  int variables[0];
};

int main (int argc, char **argv) {
  struct clause *p = malloc(sizeof(struct clause) + 3 * sizeof(int));

  p->size = 3;
  p->variables[0] = 1;
  p->variables[1] = 2;
  p->variables[2] = 3;

  struct clause *q = malloc(sizeof(struct clause) + 3 * sizeof(int));

  *q = *p;

  assert(q->variables[0] == 1);
  assert(q->variables[1] == 2);
  assert(q->variables[2] == 3);

  free(p);
  free(q);
  
  return 0;
}

A legitimate example of a zero-sized array. Seems to work FWIW.

[martin-cs]

I like the idea of a PRECONDITION but I'm not quite sure where it should go. Presumably the same thing happens when the solver is used without --refine-strings ? Do you know where it crashes?

[romainbrenguier]

@martin-cs the following code is a unit test that cause the error (Process finished with exit code 134 (interrupted by signal 6: SIGABRT))
The formula is i < 0 && i>= 0 ==> { }[i] == 12.
I'm not sure whether the solver should answer with satisfiable or error, but preferably it should not terminate the program that way.

#include <testing-utils/catch.hpp>
#include <solvers/refinement/bv_refinement.h>
#include <solvers/sat/satcheck.h>
#include <util/symbol_table.h>
#include <java_bytecode/java_types.h>
#include <util/arith_tools.h>
#include <iostream>

SCENARIO("empty array in bv_refinement",
"[core][solvers][refinement][bv_refinement]")
{
  symbol_tablet symtbl;
  const namespacet ns(symtbl);
  satcheck_no_simplifiert sat_check;
  bv_refinementt::infot info;
  info.ns=&ns;
  info.prop=&sat_check;
  info.refine_arithmetic=true;
  info.refine_arrays=true;
  info.max_node_refinement=5;
  bv_refinementt solver(info);

  const typet int_type = java_int_type();
  const symbol_exprt i("i", int_type);
  const array_exprt arr(array_typet(int_type, from_integer(0, int_type)));

  WHEN("axiom contains empty array")
  {
    const implies_exprt axiom(
      and_exprt(
        binary_relation_exprt(i, ID_lt, from_integer(0, int_type)),
        binary_relation_exprt(i, ID_ge, from_integer(0, int_type))),
      equal_exprt(index_exprt(arr, i), from_integer(12, int_type)));
    solver << axiom;

    if(solver() == decision_proceduret::resultt::D_SATISFIABLE)
      std::cout << "i = " << numeric_cast_v<std::size_t>(solver.get(i)) << std::endl;
    else
      std::cout << "unsatisfiable";
  }
}

[tautschnig]

Given that @martin-cs' example works, while the lower-level version compiled by @romainbrenguier doesn't I am starting to wonder whether the problem just resides in the refinement code? From the example I'd certainly say that there is a problem in a middle layer, which ought to be coming up with a correct answer.

1. Please add the tests posted here to the code base.
2. Please debug more thoroughly to make sure the refinement code answers such requests properly.

[romainbrenguier]

closing this PR as #1668 should fix the root cause of the bug