Как упростить формат ввода Z3 (например, операции удаления и слияния) и перенести их в обычные выражения типа bool? - PullRequest
Новая
       146

Как упростить формат ввода Z3 (например, операции удаления и слияния) и перенести их в обычные выражения типа bool?

0 голосов
/ 14 июля 2020

Например, целевая программа выглядит следующим образом: 

    pragma solidity >=0.4.24 <0.6.0;
    contract Simple {
        function f(uint a) payable public{
        a += 1;
            if (a == 66 && a+3<100) {
               a = a+3;
            }
        }
    }

Я получил сложные ограничения пути, выраженные форматом z3: 

(declare-fun TXVALUE () (_ BitVec 256))
(declare-fun a_19 () (_ BitVec 256))(assert (= a_19 #x0000000000000000000000000000000000000000000000000000000000000001))
(declare-fun a_20 () (_ BitVec 256))(assert (= a_20 (bvadd TXVALUE a_19)))
(declare-fun a_21 () (_ BitVec 256))(assert (= a_21 #x0000000000000000000000000000000000000000000000000000000000000042))
(declare-fun a_22 () Bool)(assert (= a_22 (= a_20 a_21)))
(declare-fun a_23 () (_ BitVec 256))(assert (= a_23 #x0000000000000000000000000000000000000000000000000000000000000001))
(declare-fun a_24 () (_ BitVec 256))(assert (= a_24 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_25 () (_ BitVec 256))(assert (= a_25 (ite a_22 a_23 a_24)))
(declare-fun a_26 () (_ BitVec 256))(assert (= a_26 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_27 () Bool)(assert (= a_27 (= a_25 a_26)))
(declare-fun a_28 () (_ BitVec 256))(assert (= a_28 #x0000000000000000000000000000000000000000000000000000000000000001))
(declare-fun a_29 () (_ BitVec 256))(assert (= a_29 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_30 () (_ BitVec 256))(assert (= a_30 (ite a_27 a_28 a_29)))
(declare-fun a_31 () (_ BitVec 256))(assert (= a_31 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_32 () Bool)(assert (= a_32 (= a_30 a_31)))
(declare-fun a_33 () (_ BitVec 256))(assert (= a_33 #x000000000000000000000000000000000000000000000000000000000000007a))
(declare-fun a_34 () (_ BitVec 256))(assert (= a_34 #x0000000000000000000000000000000000000000000000000000000000000072))
(declare-fun a_35 () (_ BitVec 256))(assert (= a_35 (ite (not a_32) a_33 a_34)))
(declare-fun a_36 () (_ BitVec 256))(assert (= a_36 #x0000000000000000000000000000000000000000000000000000000000000072))
(assert (= a_35 a_36))

Слишком много переменных. Фактически, я хочу: a+1 ==6 && a+1+3<100

Есть ли способ реализовать это?

1 Ответ

1 голос
/ 14 июля 2020

Это действительно вопрос солидности, а не z3. (Добавлен соответствующий тег.)

В общем, то, что вы считаете «простым», и то, что эти инструменты считают «простым», вряд ли когда-либо совпадет, и вы не можете контролировать эту внутреннюю форму. Но, возможно, у самой солидности (с которой я не знаком) есть некоторые хитрости в рукаве.

Есть ли конкретная задача, которую вы пытаетесь решить, кроме возможности увидеть результат более человечным -читаемую форму?

...