diff --git a/VS/CSHARP/asm-sim-lib/DynamicFlow.cs b/VS/CSHARP/asm-sim-lib/DynamicFlow.cs index 4b067bed..99e5c2b9 100644 --- a/VS/CSHARP/asm-sim-lib/DynamicFlow.cs +++ b/VS/CSHARP/asm-sim-lib/DynamicFlow.cs @@ -799,7 +799,7 @@ State Merge_State_Update_LOCAL( BoolExpr bc = null; { - using (Context ctx = new Context(this.tools_.Settings)) + using (Context ctx = new Context(this.tools_.ContextSettings)) { string branchKey = GraphTools<(bool, StateUpdate)>.Get_Branch_Point(source1, source2, this.graph_); BranchInfo branchInfo = Get_Branch_Condition_LOCAL(branchKey); diff --git a/VS/CSHARP/asm-sim-lib/Mnemonics.cs b/VS/CSHARP/asm-sim-lib/Mnemonics.cs index e686cc1e..c10c3374 100644 --- a/VS/CSHARP/asm-sim-lib/Mnemonics.cs +++ b/VS/CSHARP/asm-sim-lib/Mnemonics.cs @@ -106,7 +106,7 @@ public OpcodeBase(Mnemonic m, string[] args, (string prevKey, string nextKey, st this.args_ = args; this.tools_ = t; this.keys_ = keys; - this.ctx_ = new Context(t.Settings); + this.ctx_ = new Context(t.ContextSettings); } public abstract void Execute(); diff --git a/VS/CSHARP/asm-sim-lib/Runner.cs b/VS/CSHARP/asm-sim-lib/Runner.cs index 660c9e4f..d45a05b1 100644 --- a/VS/CSHARP/asm-sim-lib/Runner.cs +++ b/VS/CSHARP/asm-sim-lib/Runner.cs @@ -68,8 +68,8 @@ public static State SimpleStep_Forward(string line, State state) Tools tools = state.Tools; string nextKey = Tools.CreateKey(tools.Rand); string nextKeyBranch = "DUMMY_NOT_USED"; - (string label, Mnemonic mnemonic, string[] args, string remark) content = AsmSourceTools.ParseLine(line); - using (OpcodeBase opcodeBase = InstantiateOpcode(content.mnemonic, content.args, (state.HeadKey, nextKey, nextKeyBranch), tools)) + (string label, Mnemonic mnemonic, string[] args, string remark) = AsmSourceTools.ParseLine(line); + using (OpcodeBase opcodeBase = InstantiateOpcode(mnemonic, args, (state.HeadKey, nextKey, nextKeyBranch), tools)) { if (opcodeBase == null) { diff --git a/VS/CSHARP/asm-sim-lib/State.cs b/VS/CSHARP/asm-sim-lib/State.cs index 58942882..0b4a23e2 100644 --- a/VS/CSHARP/asm-sim-lib/State.cs +++ b/VS/CSHARP/asm-sim-lib/State.cs @@ -77,19 +77,22 @@ public class State : IDisposable private State(Tools tools) { this.tools_ = new Tools(tools); - this.ctx_ = new Context(this.tools_.Settings); // housekeeping in Dispose(); - this.Solver = MakeSolver(this.ctx_); - this.Solver_U = MakeSolver(this.ctx_); + this.ctx_ = new Context(this.tools_.ContextSettings); // housekeeping in Dispose(); + this.Solver = MakeSolver(this.ctx_, this.tools_.SolverSetting); + this.Solver_U = MakeSolver(this.ctx_, this.tools_.SolverSetting); this.branchInfoStore_ = new BranchInfoStore(this.ctx_); this.cached_Reg_Values_ = new Dictionary(); this.cached_Flag_Values_ = new Dictionary(); } - public static Solver MakeSolver(Context ctx) + public static Solver MakeSolver(Context ctx, string solverSetting = "qfbv") { Contract.Requires(ctx != null); - Solver s = ctx.MkSolver(ctx.MkTactic("qfbv")); + Solver s = (string.IsNullOrEmpty(solverSetting)) + ? ctx.MkSolver() + : ctx.MkSolver(ctx.MkTactic(solverSetting)); + //Params p = ctx.MkParams(); //p.Add("mbqi", false); // use Model-based Quantifier Instantiation //s.Parameters = p; @@ -897,22 +900,14 @@ public string ToStringConstraints(string identStr) if (this.Solver.NumAssertions > 0) { sb.AppendLine(identStr + "Current Value constraints:"); - for (int i = 0; i < (int)this.Solver.NumAssertions; ++i) - { - BoolExpr e = this.Solver.Assertions[i]; - sb.AppendLine(identStr + string.Format(Culture, " {0}: {1}", i, ToolsZ3.ToString(e))); - } + sb.AppendLine(ToolsZ3.ToString(this.Solver, identStr)); } if (this.Tools.ShowUndefConstraints) { //if (this.Solver_U.NumAssertions > 0) { sb.AppendLine(identStr + "Current Undef constraints:"); - for (int i = 0; i < (int)this.Solver_U.NumAssertions; ++i) - { - BoolExpr e = this.Solver_U.Assertions[i]; - sb.AppendLine(identStr + string.Format(Culture, " {0}: {1}", i, ToolsZ3.ToString(e))); - } + sb.AppendLine(ToolsZ3.ToString(this.Solver_U, identStr)); } } sb.AppendLine(this.BranchInfoStore.ToString()); diff --git a/VS/CSHARP/asm-sim-lib/StateUpdate.cs b/VS/CSHARP/asm-sim-lib/StateUpdate.cs index 861f6388..69f81e26 100644 --- a/VS/CSHARP/asm-sim-lib/StateUpdate.cs +++ b/VS/CSHARP/asm-sim-lib/StateUpdate.cs @@ -132,7 +132,7 @@ public StateUpdate(string prevKey, string nextKey, Tools tools) this.prevKey_Branch_ = null; this.nextKey_ = nextKey; this.tools_ = tools; - this.ctx_ = new Context(tools.Settings); // housekeeping in Dispose(); + this.ctx_ = new Context(tools.ContextSettings); // housekeeping in Dispose(); this.Empty = true; } @@ -144,7 +144,7 @@ public StateUpdate(BoolExpr branchCondition, string prevKey_Regular, string prev Contract.Requires(tools != null); Contract.Requires(branchCondition != null); - this.ctx_ = new Context(tools.Settings); // housekeeping in Dispose(); + this.ctx_ = new Context(tools.ContextSettings); // housekeeping in Dispose(); this.branch_Condition_ = branchCondition.Translate(this.ctx_) as BoolExpr; this.prevKey_Regular_ = prevKey_Regular; this.prevKey_Branch_ = prevKey_Branch; diff --git a/VS/CSHARP/asm-sim-lib/Tools.cs b/VS/CSHARP/asm-sim-lib/Tools.cs index 6afdfa97..90dddb2a 100644 --- a/VS/CSHARP/asm-sim-lib/Tools.cs +++ b/VS/CSHARP/asm-sim-lib/Tools.cs @@ -39,13 +39,13 @@ public class Tools public bool ShowUndefConstraints { get; set; } public Tools() - : this(new Dictionary()) { } + : this(new Dictionary(), string.Empty) { } public Tools(Tools other) { Contract.Requires(other != null); - this.Settings = new Dictionary(other.Settings); + this.ContextSettings = new Dictionary(other.ContextSettings); this.rand_ = other.Rand; //new Random(); this.p_ = other.p_; this.Quiet = other.Quiet; @@ -53,9 +53,10 @@ public Tools(Tools other) this.StateConfig = other.StateConfig; } - public Tools(Dictionary settings) + public Tools(Dictionary contextSettings, string solverSetting = "") { - this.Settings = settings; + this.ContextSettings = contextSettings; + this.SolverSetting = solverSetting; this.rand_ = new Random(); this.p_ = new AsmParameters(); this.Quiet = true; @@ -64,7 +65,9 @@ public Tools(Dictionary settings) this.StateConfig.GetRegOn(); } - public Dictionary Settings { get; private set; } + public Dictionary ContextSettings { get; private set; } + + public string SolverSetting { get; private set; } public Random Rand { get { return this.rand_; } } diff --git a/VS/CSHARP/asm-sim-lib/ToolsZ3.cs b/VS/CSHARP/asm-sim-lib/ToolsZ3.cs index 645a7e0b..923c2ae7 100644 --- a/VS/CSHARP/asm-sim-lib/ToolsZ3.cs +++ b/VS/CSHARP/asm-sim-lib/ToolsZ3.cs @@ -25,6 +25,7 @@ namespace AsmSim using System; using System.Collections.Generic; using System.Diagnostics.Contracts; + using System.Globalization; using System.Text; using AsmTools; using Microsoft.Z3; @@ -428,6 +429,19 @@ public static string ToString(Expr e) } } + public static string ToString(Solver solver, string identStr) + { + Contract.Requires(solver != null); + + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < (int)solver.NumAssertions; ++i) + { + BoolExpr e = solver.Assertions[i]; + sb.AppendLine(identStr + string.Format(CultureInfo.InvariantCulture, " {0}: {1}", i, ToolsZ3.ToString(e))); + } + return sb.ToString(); + } + #region Print Methods public static string ToStringBin(Tv[] a) @@ -986,8 +1000,6 @@ private static Tv GetTv_Method1(BoolExpr value, BoolExpr undef, Solver solver, S private static Tv GetTv_Method2(BoolExpr value, BoolExpr undef, Solver solver, Solver solver_U, Context ctx) { - Dictionary settings = new Dictionary(); - bool tvTrue; { using (Solver s = State.MakeSolver(ctx)) diff --git a/VS/CSHARP/asm-sim-main/ProgramZ3.cs b/VS/CSHARP/asm-sim-main/ProgramZ3.cs index ec49ffd9..0c9382d3 100644 --- a/VS/CSHARP/asm-sim-main/ProgramZ3.cs +++ b/VS/CSHARP/asm-sim-main/ProgramZ3.cs @@ -54,8 +54,8 @@ private static void Main(string[] args) // Test_Usage(); if (true) { - TestMemorySpeed(); - TestMemorySpeed2(); + TestMemorySpeed_mov_mov(); + TestMemorySpeed_push_pop(); } // TestDynamicFlow(); // TestSIMD(); @@ -186,7 +186,7 @@ private static void TestSIMD() } } - private static void TestMemorySpeed() + private static void TestMemorySpeed_mov_mov() { /* string line1 = "mov qword ptr [rax], rbx"; @@ -281,7 +281,9 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax }; using (Context ctx = new Context(settings)) { - Solver solver = ctx.MkSolver(); + // Solver solver = ctx.MkSolver(); + Solver solver = ctx.MkSolver(ctx.MkTactic("qfbv")); + #region Create 3 64bit-registers and 1 64-bit memory location, at 3 time stamps BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); @@ -301,7 +303,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax ArrayExpr mem2 = ctx.MkArrayConst("MEM!2", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); #endregion - if (false) + if (true) { #region mov qword ptr [rax], rbx solver.Assert(ctx.MkEq(rax1, rax0)); // unchanged register state @@ -333,8 +335,11 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax solver.Assert(ctx.MkEq(mem2, mem1)); // unchanged memory state #endregion } - // Console.WriteLine(solver); + + Console.WriteLine(ToolsZ3.ToString(solver, "solver mov_mov")); Console.WriteLine("========================"); + //Console.WriteLine(solver); + //Console.WriteLine("========================"); bool method1 = false; bool method2 = false; @@ -462,7 +467,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax } } - private static void TestMemorySpeed2() + private static void TestMemorySpeed_push_pop() { ArrayExpr store_mem_method1_LOCAL(Context ctx, ArrayExpr member_before, BitVecExpr destination_reg, BitVecExpr source_reg) { @@ -518,101 +523,86 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax { "proof", "false" }, // enable proof generation { "timeout", "60000" }, // 60000=1min }; + + // push rax + // pop rbx + + //0: (= RAX!3D50632C10EAA838 RAX!0) + //1: (= RSP!3D50632C10EAA838(bvadd #xfffffffffffffff8 RSP!0)) + //2: (let((a!1(store(store(store MEM!0 RSP!0((_ extract 7 0) RAX!0))(bvadd #x0000000000000001 RSP!0) ((_ extract 15 8) RAX!0)) (bvadd #x0000000000000002 RSP!0) ((_ extract 23 16) RAX!0)))) (let ((a!2 (store (store (store a!1 (bvadd #x0000000000000003 RSP!0) ((_ extract 31 24) RAX!0)) (bvadd #x0000000000000004 RSP!0) ((_ extract 39 32) RAX!0)) (bvadd #x0000000000000005 RSP!0) ((_ extract 47 40) RAX!0)))) (= MEM!3D50632C10EAA838 (store (store a!2 (bvadd #x0000000000000006 RSP!0) ((_ extract 55 48) RAX!0)) (bvadd #x0000000000000007 RSP!0) ((_ extract 63 56) RAX!0))))) + //3: (= RAX!6DE3EBEB4605B058 RAX!3D50632C10EAA838) + //4: (= RBX!6DE3EBEB4605B058(concat(select MEM!3D50632C10EAA838(bvadd #x000000000000000f RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x000000000000000e RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x000000000000000d RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x000000000000000c RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x000000000000000b RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x000000000000000a RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x0000000000000009 RSP!3D50632C10EAA838)) (select MEM!3D50632C10EAA838 (bvadd #x0000000000000008 RSP!3D50632C10EAA838)))) + //5: (= RSP!6DE3EBEB4605B058(bvadd #x0000000000000008 RSP!3D50632C10EAA838)) + //6: (= MEM!6DE3EBEB4605B058 MEM!3D50632C10EAA838) + + using (Context ctx = new Context(settings)) { - Solver solver = ctx.MkSolver(); + // Solver solver = ctx.MkSolver(); + Solver solver = ctx.MkSolver(ctx.MkTactic("qfbv")); #region Create 3 64bit-registers and 1 64-bit memory location, at 3 time stamps BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); BitVecExpr rax2 = ctx.MkBVConst("RAX!2", 64); - BitVecExpr rax3 = ctx.MkBVConst("RAX!3", 64); - BitVecExpr rax4 = ctx.MkBVConst("RAX!4", 64); BitVecExpr rbx0 = ctx.MkBVConst("RBX!0", 64); BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64); BitVecExpr rbx2 = ctx.MkBVConst("RBX!2", 64); - BitVecExpr rbx3 = ctx.MkBVConst("RBX!3", 64); - BitVecExpr rbx4 = ctx.MkBVConst("RBX!4", 64); - BitVecExpr rcx0 = ctx.MkBVConst("RCX!0", 64); - BitVecExpr rcx1 = ctx.MkBVConst("RCX!1", 64); - BitVecExpr rcx2 = ctx.MkBVConst("RCX!2", 64); - BitVecExpr rcx3 = ctx.MkBVConst("RCX!3", 64); - BitVecExpr rcx4 = ctx.MkBVConst("RCX!4", 64); - - BitVecExpr rdx0 = ctx.MkBVConst("RDX!0", 64); - BitVecExpr rdx1 = ctx.MkBVConst("RDX!1", 64); - BitVecExpr rdx2 = ctx.MkBVConst("RDX!2", 64); - BitVecExpr rdx3 = ctx.MkBVConst("RDX!3", 64); - BitVecExpr rdx4 = ctx.MkBVConst("RDX!4", 64); + BitVecExpr rsp0 = ctx.MkBVConst("RSP!0", 64); + BitVecExpr rsp1 = ctx.MkBVConst("RSP!1", 64); + BitVecExpr rsp2 = ctx.MkBVConst("RSP!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)); - ArrayExpr mem3 = ctx.MkArrayConst("MEM!3", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); - ArrayExpr mem4 = ctx.MkArrayConst("MEM!4", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); #endregion if (true) { - #region mov qword ptr [rax], rbx + #region push rax solver.Assert(ctx.MkEq(rax1, rax0)); // unchanged register state solver.Assert(ctx.MkEq(rbx1, rbx0)); // unchanged register state - solver.Assert(ctx.MkEq(rcx1, rcx0)); // unchanged register state - solver.Assert(ctx.MkEq(rdx1, rdx0)); // unchanged register state - solver.Assert(ctx.MkEq(mem1, store_mem_method1_LOCAL(ctx, mem0, rax0, rbx0))); // mov qword ptr [rax], rbx + solver.Assert(ctx.MkEq(rsp1, ctx.MkBVSub(rsp0, ctx.MkBV(8, 64)))); + solver.Assert(ctx.MkEq(mem1, store_mem_method1_LOCAL(ctx, mem0, rsp0, rax0))); #endregion - #region mov rcx, qword ptr [rax] - solver.Assert(ctx.MkEq(rax2, rax1)); // rax at t=2 is equal to rax at t=1, although we do not know the exact value - solver.Assert(ctx.MkEq(rbx2, rbx1)); // rbx at t=2 is equal to rbx at t=1, although we do not know the exact value - solver.Assert(ctx.MkEq(rcx2, retrieve_mem_method_LOCAL(ctx, mem1, rax1))); // mov rcx, qword ptr [rax] - solver.Assert(ctx.MkEq(rdx2, rdx1)); // unchanged register state + #region mov pop rbx + solver.Assert(ctx.MkEq(rax2, rax1)); // unchanged register state + solver.Assert(ctx.MkEq(rbx2, retrieve_mem_method_LOCAL(ctx, mem1, rsp1))); + solver.Assert(ctx.MkEq(rsp2, ctx.MkBVAdd(rsp1, ctx.MkBV(8, 64)))); solver.Assert(ctx.MkEq(mem2, mem1)); // unchanged memory state #endregion - - #region mov qword ptr [rdx], rcx - solver.Assert(ctx.MkEq(rax3, rax2)); // unchanged register state - solver.Assert(ctx.MkEq(rbx3, rbx2)); // unchanged register state - solver.Assert(ctx.MkEq(rcx3, rcx2)); // unchanged register state - solver.Assert(ctx.MkEq(rdx3, rdx2)); // unchanged register state - solver.Assert(ctx.MkEq(mem3, store_mem_method1_LOCAL(ctx, mem2, rdx2, rbx2))); // mov qword ptr [rdx], rcx - #endregion - - #region mov rax, qword ptr [rdx] - solver.Assert(ctx.MkEq(rax4, retrieve_mem_method_LOCAL(ctx, mem3, rdx3))); // mov rax, qword ptr [rdx] - solver.Assert(ctx.MkEq(rbx4, rbx3)); // unchanged register state - solver.Assert(ctx.MkEq(rcx4, rcx3)); // unchanged register state - solver.Assert(ctx.MkEq(rdx4, rdx3)); // unchanged register state - solver.Assert(ctx.MkEq(mem4, mem3)); // unchanged memory state - #endregion } else { - #region mov qword ptr [rax], rbx + #region push rax solver.Assert(ctx.MkEq(rax1, rax0)); // unchanged register state solver.Assert(ctx.MkEq(rbx1, rbx0)); // unchanged register state - solver.Assert(ctx.MkEq(rcx1, rcx0)); // unchanged register state - store_mem_method2_LOCAL(ctx, solver, mem0, mem1, rax0, rbx0); + solver.Assert(ctx.MkEq(rsp1, ctx.MkBVSub(rsp0, ctx.MkBV(8, 64)))); + store_mem_method2_LOCAL(ctx, solver, mem0, mem1, rsp0, rax0); #endregion - #region mov rcx, qword ptr [rax] + #region mov pop rbx solver.Assert(ctx.MkEq(rax2, rax1)); // unchanged register state - solver.Assert(ctx.MkEq(rbx2, rbx1)); // unchanged register state - solver.Assert(ctx.MkEq(rcx2, retrieve_mem_method_LOCAL(ctx, mem1, rax1))); // mov rcx, qword ptr [rax] + solver.Assert(ctx.MkEq(rbx2, retrieve_mem_method_LOCAL(ctx, mem1, rsp1))); + solver.Assert(ctx.MkEq(rsp2, ctx.MkBVAdd(rsp1, ctx.MkBV(8, 64)))); solver.Assert(ctx.MkEq(mem2, mem1)); // unchanged memory state #endregion } - // Console.WriteLine(solver); + + Console.WriteLine(ToolsZ3.ToString(solver, "solver push-pop")); Console.WriteLine("========================"); + //Console.WriteLine(solver); + //Console.WriteLine("========================"); bool method1 = false; bool method2 = false; BoolExpr[] constraints = solver.Assertions; { - BoolExpr t = ctx.MkNot(ctx.MkEq(rax4, rdx4)); + BoolExpr t = ctx.MkNot(ctx.MkEq(rax2, rbx2)); Console.WriteLine("test=" + t); Status status; DateTime startTime = DateTime.Now; @@ -652,7 +642,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax } } { - BoolExpr t = ctx.MkEq(rax4, rdx4); + BoolExpr t = ctx.MkEq(rax2, rbx2); Console.WriteLine("test=" + t); Status status; DateTime startTime = DateTime.Now; @@ -691,7 +681,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax } } { - BoolExpr t = ctx.MkNot(ctx.MkEq(rax4, rdx4)); + BoolExpr t = ctx.MkNot(ctx.MkEq(rsp0, rsp2)); Console.WriteLine("test=" + t); Status status; DateTime startTime = DateTime.Now; diff --git a/VS/CSHARP/unit-tests-asm-sim/Test_Mnemonic.cs b/VS/CSHARP/unit-tests-asm-sim/Test_Mnemonic.cs index 19f8c48c..a2a6cab5 100644 --- a/VS/CSHARP/unit-tests-asm-sim/Test_Mnemonic.cs +++ b/VS/CSHARP/unit-tests-asm-sim/Test_Mnemonic.cs @@ -42,7 +42,7 @@ public Test_Mnemonic() Console.WriteLine("logToDisplay=" + LogToDisplay); } - private Tools CreateTools(int timeOut = AsmTestTools.DEFAULT_TIMEOUT) + private Tools CreateTools(string solverSetting = "", int timeOut = AsmTestTools.DEFAULT_TIMEOUT) { /* The following parameters can be set: - proof (Boolean) Enable proof generation @@ -66,9 +66,8 @@ global and module parameters. For this purpose we should now use { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", timeOut.ToString(CultureInfo.InvariantCulture) }, - { "parallel", "true" }, }; - return new Tools(settings); + return new Tools(settings, solverSetting); } private State CreateState(Tools tools) @@ -3843,7 +3842,7 @@ public void Test_MnemonicZ3_PushPop_64bit_2() [TestMethod] public void Test_MnemonicZ3_PushPop_64bit_3() { - Tools tools = this.CreateTools(40000); // 10000=10sec + Tools tools = this.CreateTools(string.Empty, 60000); // 10000=10sec tools.StateConfig.Set_All_Off(); tools.StateConfig.RAX = true; tools.StateConfig.RBX = true; @@ -3859,7 +3858,7 @@ public void Test_MnemonicZ3_PushPop_64bit_3() state = Runner.SimpleStep_Forward(line1, state); if (LogToDisplay) { - Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + //Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); } AsmTestTools.AreUnrelated(Rn.RAX, Rn.RBX, state); @@ -3876,7 +3875,7 @@ public void Test_MnemonicZ3_PushPop_64bit_3() [TestMethod] public void Test_MnemonicZ3_PushPop_64bit_4() { - Tools tools = this.CreateTools(40000); + Tools tools = this.CreateTools(); tools.StateConfig.Set_All_Off(); tools.StateConfig.RAX = true; tools.StateConfig.RBX = true; @@ -3898,7 +3897,7 @@ public void Test_MnemonicZ3_PushPop_64bit_4() state = Runner.SimpleStep_Forward(line2, state); if (LogToDisplay) { - Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); + //Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); } AsmTestTools.AreEqual(Rn.RAX, Rn.RBX, state);