Как создать модель для моего кода с помощью Boolector? - PullRequest
Новая
       36

Как создать модель для моего кода с помощью Boolector?

0 голосов
/ 21 марта 2020

Я немного экспериментирую с boolector , поэтому я пытаюсь создать модель для простого кода. Предположим, что у меня есть следующий псевдокод: 

int a = 5;
int b = 4;
int c = 3;

Для этого простого набора инструкций я могу создать модель, и все отлично работает. Проблема в том, что после этого у меня есть другие инструкции, такие как 

b = 10;
c = 20;

Очевидно, что не удается сгенерировать модель, потому что b не может быть равно 4 и 10 в том же модуле. Один из сопровождающих предложил мне использовать boolector_push и boolector_pop для создания новых Context s при необходимости.

Код для boolector_push: 

void
boolector_push (Btor *btor, uint32_t level)
{
  BTOR_ABORT_ARG_NULL (btor);
  BTOR_TRAPI ("%u", level);
  BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
              "incremental usage has not been enabled");

  if (level == 0) return;

  uint32_t i;
  for (i = 0; i < level; i++)
  {
    BTOR_PUSH_STACK (btor->assertions_trail,
                     BTOR_COUNT_STACK (btor->assertions));
  }
  btor->num_push_pop++;
}

Вместо этого для boolector_pop есть 

void
boolector_pop (Btor *btor, uint32_t level)
{
  BTOR_ABORT_ARG_NULL (btor);
  BTOR_TRAPI ("%u", level);
  BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
              "incremental usage has not been enabled");
  BTOR_ABORT (level > BTOR_COUNT_STACK (btor->assertions_trail),
              "can not pop more levels (%u) than created via push (%u).",
              level,
              BTOR_COUNT_STACK (btor->assertions_trail));

  if (level == 0) return;

  uint32_t i, pos;
  BtorNode *cur;

  for (i = 0, pos = 0; i < level; i++)
    pos = BTOR_POP_STACK (btor->assertions_trail);

  while (BTOR_COUNT_STACK (btor->assertions) > pos)
  {
    cur = BTOR_POP_STACK (btor->assertions);
    btor_hashint_table_remove (btor->assertions_cache, btor_node_get_id (cur));
    btor_node_release (btor, cur);
  }
  btor->num_push_pop++;
}

По моему мнению, эти две функции отслеживают утверждения, сгенерированные с помощью boolector_assert, так как можно получить окончательную и правильную модель с использованием boolector_push и boolector_pop учитывая, что ограничения будут одинаковыми?

Чего мне не хватает?

Спасибо

1 Ответ

1 голос
/ 21 марта 2020

Как вы и подозревали, методы push и pop решателя - это не то, что вы ищете здесь. Вместо этого вам нужно превратить моделируемую программу в форму, известную как SSA (Stati c Single Assignment). Вот статья в Википедии, которая довольно информативна: https://en.wikipedia.org/wiki/Static_single_assignment_form

Основная идея c состоит в том, что вы «обрабатываете» свои изменяемые переменные как изменяющиеся во времени значения и даете их уникальные имена, как вы делаете несколько назначений им. Итак, следующее: 

a = 5
b = a + 2
c = b + 3
c = c + 1
b = c + 6

становится: 

a0 = 5
b0 = a0 + 2
c0 = b0 + 3
c1 = c0 + 1
b1 = c1 + 6

et c. Обратите внимание, что с условностями сложно разобраться, и обычно требуется то, что известно как фи-узлы. (т. е. слияние значений ветвей.) Большинство компиляторов автоматически выполняют такие преобразования для вас, поскольку это позволяет проводить много оптимизаций в будущем. Вы можете сделать это вручную или использовать алгоритм, который сделает это за вас, в зависимости от вашей конкретной проблемы.

Вот еще один вопрос о переполнении стека, который по сути требует чего-то похожего: Z3 Conditional Заявление

Надеюсь, это поможет!

...