4

Z3 を使用してプログラムのメモリ アクセスをモデリングしていますが、共有したいパフォーマンスについて疑問があります。

次のようなコンパクトな方法でモデル化したかったのです。

memset(dst, 0, 1000);

私が最初に試みたのは配列理論を使用することでしたが、それは、同様の用語を 1,000 個作成するか(assert (and (= (select mem 0) 0) (= (select mem 1) 0) ...、同様のストアを 1,000 個作成するか、次のような定量化された式を作成することを意味していました。

(forall (x Int) (implies (and (>= x 0) (< x 1000)) (= (select mem x) 0))

しかし、配列を使用している間は量指定子を避けるように言われました。

次のアイデアは、UF を定義することでした。

 (define-fun newmemfun ((idx Int)) Int (
   ite (and (>= idx 0) (< idx 1000)) 0 (prevmemfun idx)
 ))

ただし、これは、メモリ書き込み操作ごとに新しい関数を定義する必要があることを意味します (memset や memcpy のような複数のストアだけでなく、個々のストア操作についても)。これは、同じインデックスの「古い」値を保存する非常にネストされた ITE 構造を作成することになります。すなわち:

mem[0] = 1;
mem[0] = 2;

would be:
(ite (= idx 0) 2 (ite (= idx 0) 1 ...

これは機能的には正しいですが、式のサイズ (および生成された AST を推測します) は非常に速く蓄積する傾向があり、Z3 がこのケースを検出して処理するように最適化されているかどうかはわかりません。

したがって、問題は、上記の例のような大規模な複数のストアと個々のストアを同時に処理できるメモリ操作をエンコードする最もパフォーマンスの高い方法は何であるかということです。

ありがとう、パブロ。

PS: 閉じていないかっこが一致しない意図:P.

4

1 に答える 1

2

メモリアクセスのモデリング（たとえば、検証、テストケースの生成などを行う予定ですか？）を除いて、最終目標についてもう少し詳しく知らなければ、多くのオプションがあるため、答えるのはやや困難です。ただし、APIのいずれかに依存している場合は、パフォーマンスの問題を制御するための柔軟性が最も高い場合があります。たとえば、次のように独自のメモリアクセスを定義できます（z3pyスクリプトへのリンク：http：//rise4fun.com/Z3Py/gO6i ）：

address_bits = 7
data_bits = 8

s = Solver()

# mem is a list of length program step, of a list of length 2^address_bits of bitvectors of size 2^data_bits
mem =[]

# modify a single address addr to value at program step step
def modifyAddr(addr, value, step):
  mem.append([]) # add new step
  for i in range(0,2**address_bits):
    mem[step+1].append( BitVec('m' + str(step + 1) + '_' + str(i), data_bits) )

    if i != addr:
      s.add(mem[step+1][i] == mem[step][i])
    else:
      s.add(mem[step+1][i] == value)

# set all memory addresses to a specified value at program step step
def memSet(value, step):
  mem.append([])
  for i in range(0,2**address_bits):
    mem[step+1].append( BitVec('m' + str(step + 1) + '_' + str(i), data_bits) )
    s.add(mem[step+1][i] == value)

modaddr = 23 # example address
step = -1
# initialize all addresses to 0
memSet(0, step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]] # print all step values for modaddr

modifyAddr(modaddr,3,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

modifyAddr(modaddr,4,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

modifyAddr(modaddr,2**6,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

memSet(1,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

for a in range(0,2**address_bits): # set all address values to their address number
  modifyAddr(a,a,step)
  step += 1

print s.check()
print "values for modaddr at all steps"
for i in range(0,step+1): print s.model()[mem[i][modaddr]] # print all values at each step for modaddr

print "values at final step"
for i in range(0,2**address_bits): print s.model()[mem[step][i]] # print all memory addresses at final step

この単純な実装では、（a）すべてのメモリアドレスを特定の値（memsetなど）に設定するか、（b）単一のメモリアドレスを変更して、他のすべてのアドレスを同じ値に制限することができます。私の場合、128アドレスの約128ステップを実行してエンコードするのに数秒かかったので、それぞれ8ビットの約20000ビットベクトル式がありました。

ここで、実行していることに応じて（たとえば、このmemsetのような複数のアドレスへのアトミック書き込みを許可しますか、それともすべてを個別の書き込みとしてモデル化しますか？）、アドレスのサブセットを変更するなど、さらに関数を追加できます。プログラムステップのいくつかの値。これにより、モデリングの精度とパフォーマンスのトレードオフを柔軟に行うことができます（たとえば、メモリブロックへのアトミック書き込みと、一度に1つのアドレスを変更することで、パフォーマンスの問題が発生します）。また、この実装にはAPIは必要ありません。これを、SMT-LIBファイルとしてエンコードすることもできますが、 APIの1つ。

于 2012-11-26T20:46:08.933 に答える