一种高效的嵌套存储操作方法
一种高效的嵌套存储操作方法
提问于 2017-05-26 15:52:57
在在Z3中表示内存缓冲区的最有效方法中，关于如何提高嵌套存储操作的效率的问题是，可以用selects (嵌套)存储操作替换(嵌套)存储操作，如in：(assert (= (select A i1) v1))。但是，我需要存储操作，因为以前的约束必须替换为新的约束。
例如:以下约束模拟以下程序集：
mov qword ptr [rax], rbx
mov rcx, qword ptr [rax]我喜欢证明rbx和rcx是相等的，我断言(= RBX！2RCX！2)并期望模型能够满足。这工作得很好。我断言(not (= RBX!2 RCX!2))，并期望模型不能满足。当我将以下约束提供给Z3 (例如这里)时，它给出了一个几乎即时的答案: UNSAT。然而，如果我在一个C#程序中证明了同样的问题(见下面)，它就无法推断出UNSAT (在合理的时间内)。
问题：我可以尝试怎样使C#程序与SMT2.0程序一样快速？
(declare-fun RAX!0 () (_ BitVec 64))
(declare-fun RAX!1 () (_ BitVec 64))
(declare-fun RAX!2 () (_ BitVec 64))
(declare-fun RBX!0 () (_ BitVec 64))
(declare-fun RBX!1 () (_ BitVec 64))
(declare-fun RBX!2 () (_ BitVec 64))
(declare-fun RCX!0 () (_ BitVec 64))
(declare-fun RCX!1 () (_ BitVec 64))
(declare-fun RCX!2 () (_ BitVec 64))
(declare-fun MEM!0 () (Array (_ BitVec 64) (_ BitVec 8)))
(declare-fun MEM!1 () (Array (_ BitVec 64) (_ BitVec 8)))
(declare-fun MEM!2 () (Array (_ BitVec 64) (_ BitVec 8)))
(assert (= RAX!1 RAX!0))
(assert (= RBX!1 RBX!0))
(assert (= RCX!1 RCX!0))
(assert (let ((a!1 (store (store (store MEM!0 RAX!0 ((_ extract 7 0) RBX!0))
(bvadd #x0000000000000001 RAX!0)
((_ extract 15 8) RBX!0))
(bvadd #x0000000000000002 RAX!0)
((_ extract 23 16) RBX!0))))
(let ((a!2 (store (store (store a!1
(bvadd #x0000000000000003 RAX!0)
((_ extract 31 24) RBX!0))
(bvadd #x0000000000000004 RAX!0)
((_ extract 39 32) RBX!0))
(bvadd #x0000000000000005 RAX!0)
((_ extract 47 40) RBX!0))))
(= MEM!1
(store (store a!2
(bvadd #x0000000000000006 RAX!0)
((_ extract 55 48) RBX!0))
(bvadd #x0000000000000007 RAX!0)
((_ extract 63 56) RBX!0))))))
(assert (= RAX!2 RAX!1))
(assert (= RBX!2 RBX!1))
(assert (= RCX!2
(concat (select MEM!1 (bvadd #x0000000000000007 RAX!1))
(select MEM!1 (bvadd #x0000000000000006 RAX!1))
(select MEM!1 (bvadd #x0000000000000005 RAX!1))
(select MEM!1 (bvadd #x0000000000000004 RAX!1))
(select MEM!1 (bvadd #x0000000000000003 RAX!1))
(select MEM!1 (bvadd #x0000000000000002 RAX!1))
(select MEM!1 (bvadd #x0000000000000001 RAX!1))
(select MEM!1 RAX!1))))
(assert (= MEM!2 MEM!1))
(assert (not (= RBX!2 RCX!2)))C#代码：
Dictionary<string, string> settings = new Dictionary<string, string>
{
{ "unsat-core", "false" }, // enable generation of unsat cores
{ "model", "false" }, // enable model generation
{ "proof", "false" }, // enable proof generation
{ "timeout", "60000" } // 60000=1min
};
Context ctx = new Context(settings);
Solver solver = ctx.MkSolver(ctx.MkTactic("qfbv"));
BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64);
BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64);
BitVecExpr rax2 = ctx.MkBVConst("RAX!2", 64);
BitVecExpr rbx0 = ctx.MkBVConst("RBX!0", 64);
BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64);
BitVecExpr rbx2 = ctx.MkBVConst("RBX!2", 64);
BitVecExpr rcx0 = ctx.MkBVConst("RCX!0", 64);
BitVecExpr rcx1 = ctx.MkBVConst("RCX!1", 64);
BitVecExpr rcx2 = ctx.MkBVConst("RCX!2", 64);
ArrayExpr mem0 = ctx.MkArrayConst("MEM!0", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8));
ArrayExpr mem1 = ctx.MkArrayConst("MEM!1", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8));
ArrayExpr mem2 = ctx.MkArrayConst("MEM!2", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8));
solver.Assert(ctx.MkEq(rax1, rax0));
solver.Assert(ctx.MkEq(rbx1, rbx0));
solver.Assert(ctx.MkEq(rcx1, rcx0));
ArrayExpr memX0 = ctx.MkStore(mem0, ctx.MkBVAdd(ctx.MkBV(0, 64), rax0), ctx.MkExtract((1 * 8) - 1, 0 * 8, rbx0));
ArrayExpr memX1 = ctx.MkStore(memX0, ctx.MkBVAdd(ctx.MkBV(1, 64), rax0), ctx.MkExtract((2 * 8) - 1, 1 * 8, rbx0));
ArrayExpr memX2 = ctx.MkStore(memX1, ctx.MkBVAdd(ctx.MkBV(2, 64), rax0), ctx.MkExtract((3 * 8) - 1, 2 * 8, rbx0));
ArrayExpr memX3 = ctx.MkStore(memX2, ctx.MkBVAdd(ctx.MkBV(3, 64), rax0), ctx.MkExtract((4 * 8) - 1, 3 * 8, rbx0));
ArrayExpr memX4 = ctx.MkStore(memX3, ctx.MkBVAdd(ctx.MkBV(4, 64), rax0), ctx.MkExtract((5 * 8) - 1, 4 * 8, rbx0));
ArrayExpr memX5 = ctx.MkStore(memX4, ctx.MkBVAdd(ctx.MkBV(5, 64), rax0), ctx.MkExtract((6 * 8) - 1, 5 * 8, rbx0));
ArrayExpr memX6 = ctx.MkStore(memX5, ctx.MkBVAdd(ctx.MkBV(6, 64), rax0), ctx.MkExtract((7 * 8) - 1, 6 * 8, rbx0));
memX7 = ctx.MkStore(memX6, ctx.MkBVAdd(ctx.MkBV(7, 64), rax0), ctx.MkExtract((8 * 8) - 1, 7 * 8, rbx0));
solver.Assert(ctx.MkEq(mem1, memX7).Simplify() as BoolExpr);
solver.Assert(ctx.MkEq(rax2, rax1));
solver.Assert(ctx.MkEq(rbx2, rbx1));
BitVecExpr y0 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(0, 64), rax1)) as BitVecExpr;
BitVecExpr y1 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(1, 64), rax1)) as BitVecExpr;
BitVecExpr y2 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(2, 64), rax1)) as BitVecExpr;
BitVecExpr y3 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(3, 64), rax1)) as BitVecExpr;
BitVecExpr y4 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(4, 64), rax1)) as BitVecExpr;
BitVecExpr y5 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(5, 64), rax1)) as BitVecExpr;
BitVecExpr y6 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(6, 64), rax1)) as BitVecExpr;
BitVecExpr y7 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(7, 64), rax1)) as BitVecExpr;
BitVecExpr y = ctx.MkConcat(y7, ctx.MkConcat(y6, ctx.MkConcat(y5, ctx.MkConcat(y4, ctx.MkConcat(y3, ctx.MkConcat(y2, ctx.MkConcat(y1, y0)))))));
solver.Assert(ctx.MkEq(rcx2, y).Simplify() as BoolExpr);
solver.Assert(ctx.MkEq(mem2, mem1));
Status status_Neg = solver.Check(ctx.MkNot(ctx.MkEq(rbx2, rcx2)));
Console.WriteLine("Status Neg = "+status_Neg); // Go on holiday...回答 1
Stack Overflow用户
发布于 2017-06-01 03:36:58
不幸的是，我没有办法运行C#程序来玩它。但我注意到你接到了Simplify的电话
solver.Assert(ctx.MkEq(mem1, memX7).Simplify() as BoolExpr);我很好奇你为什么需要那个电话？也许这就是罪魁祸首？
另一件事是使用未解释的函数来表示内存，而不是Array。UF通常更容易处理，在我的个人经验中它们提供了大致相同的抽象。
看看SMT生成的C#接口，看看翻译结果是否与你想象的有很大不同，这可能是个好主意。我想您可以使用以下函数来实现这一点：https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/AST.cs#L195
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/44205635
复制相关文章
相似问题
腾讯云开发者
