diff --git a/VS/CPP/ConsoleTest/example_semantic_analysis2.asm b/VS/CPP/ConsoleTest/example_semantic_analysis2.asm new file mode 100644 index 00000000..85bdff8b --- /dev/null +++ b/VS/CPP/ConsoleTest/example_semantic_analysis2.asm @@ -0,0 +1,45 @@ + ;mov rax, 10 + cmp rax, 0 + jz label1 + xor rax, rax + mov rcx, rax + add rax, 1 +label1: + inc rax + mov rbx, rax + mov rax, rbx + + + + mov rcx, 10 +labelx: + dec rcx + jnz labelx + mov rax, rcx + + aaa + + mov rcx, 10 + mov r10, rcx ; store the parameter rcx in r10 +;mod3 PROC +; parameter 1: rcx + mov r8, 0aaaaaaaaaaaaaaabH ;; (scaled) reciprocal of 3 + mov rax, rcx + mul r8 ;; multiply with reciprocal + shr rdx, 1 ;; quotient + lea r9, QWORD PTR [rdx+rdx*2] ;; back multiply with 3 + neg r9 + add rcx, r9 ;; subtract from dividend + ;mov rax, rcx ;; remainder + ; rcx has the result (mod3) + +; ret +;mod3 ENDP + + + mov rax, r10 + xor rdx, rdx + mov r8, 3 + idiv r8 + ; rdx has the result (mod3) + diff --git a/VS/CSHARP/asm-dude-vsix/Resources/examples/example_semantic_analysis.asm b/VS/CSHARP/asm-dude-vsix/Resources/examples/example_semantic_analysis.asm index 0afd6926..8eaef7c7 100644 --- a/VS/CSHARP/asm-dude-vsix/Resources/examples/example_semantic_analysis.asm +++ b/VS/CSHARP/asm-dude-vsix/Resources/examples/example_semantic_analysis.asm @@ -7,7 +7,7 @@ inc rax #endregion - vaddpd xmm1, xmm2, xmm3 ; inimplemented instruction to stop the simulator + vaddpd xmm1, xmm2, xmm3 ; unimplemented instruction to stop the simulator #region Semantic Error: usage of undefined carry @@ -16,14 +16,14 @@ add eax, 1 #endregion - vaddpd xmm1, xmm2, xmm3 ; inimplemented instruction to stop the simulator + vaddpd xmm1, xmm2, xmm3 ; unimplemented instruction to stop the simulator #region move value to memory mov ptr qword [rax], 10 mov rax, ptr qword [rax] #endregion - vaddpd xmm1, xmm2, xmm3 ; inimplemented instruction to stop the simulator + vaddpd xmm1, xmm2, xmm3 ; unimplemented instruction to stop the simulator #region slow (expensive) instruction mov ptr qword [rax], 10 @@ -31,7 +31,7 @@ popcnt rbx, rax #endregion - vaddpd xmm1, xmm2, xmm3 ; inimplemented instruction to stop the simulator + vaddpd xmm1, xmm2, xmm3 ; unimplemented instruction to stop the simulator #region moving undefined values to memory and retrieving it. mov cx, 0 @@ -40,14 +40,14 @@ mov rcx, ptr qword [rbx] #endregion - ;vaddpd xmm1, xmm2, xmm3 ; inimplemented instruction to stop the simulator + ;vaddpd xmm1, xmm2, xmm3 ; unimplemented instruction to stop the simulator #region Redundant instruction warning mov rax, rbx mov rbx, rax #endregion - #region Redundant instruction warning in memory + #region Redundant instruction warning in memory (but AsmSim does not find it simply because it times out) mov qword [rcx], rax mov qword [rcx], rbx #endregion diff --git a/VS/CSHARP/asm-dude-vsix/Squiggles/SquigglesTagger.cs b/VS/CSHARP/asm-dude-vsix/Squiggles/SquigglesTagger.cs index 13e919b9..8107a356 100644 --- a/VS/CSHARP/asm-dude-vsix/Squiggles/SquigglesTagger.cs +++ b/VS/CSHARP/asm-dude-vsix/Squiggles/SquigglesTagger.cs @@ -82,7 +82,7 @@ internal SquigglesTagger( { this._asmSimulator.Line_Updated_Event += (o, e) => { - AsmDudeToolsStatic.Output_INFO("SquigglesTagger:Handling _asmSimulator.Line_Updated_Event: event from " + o + ". Line " + e.LineNumber + ": "+e.Message); + //AsmDudeToolsStatic.Output_INFO("SquigglesTagger:Handling _asmSimulator.Line_Updated_Event: event from " + o + ". Line " + e.LineNumber + ": "+e.Message); this.Update_Squiggles_Tasks(e.LineNumber); this.Update_Error_Task_AsmSim(e.LineNumber, e.Message); }; diff --git a/VS/CSHARP/asm-dude-vsix/Tools/AsmSimulator.cs b/VS/CSHARP/asm-dude-vsix/Tools/AsmSimulator.cs index 1658b6a2..ad8b08c6 100644 --- a/VS/CSHARP/asm-dude-vsix/Tools/AsmSimulator.cs +++ b/VS/CSHARP/asm-dude-vsix/Tools/AsmSimulator.cs @@ -82,10 +82,10 @@ private AsmSimulator(ITextBuffer buffer, IBufferTagAggregatorFactoryService aggr this._buffer = buffer; this._aggregator = AsmDudeToolsStatic.GetOrCreate_Aggregator(buffer, aggregatorFactory); - if (Settings.Default.AsmSim_On) + this.Enabled = Settings.Default.AsmSim_On; + if (this.Enabled) { AsmDudeToolsStatic.Output_INFO("AsmSimulator:AsmSimulator: swithed on"); - this.Enabled = true; this._cached_States_After = new Dictionary(); this._cached_States_Before = new Dictionary(); @@ -139,11 +139,12 @@ private AsmSimulator(ITextBuffer buffer, IBufferTagAggregatorFactoryService aggr this._delay = new Delay(AsmDudePackage.msSleepBeforeAsyncExecution, 100, this._threadPool); this._delay.Done_Event += (o, i) => { - if ((this._thread_Result != null) && !this._thread_Result.IsCanceled) { + AsmDudeToolsStatic.Output_INFO("AsmSimulator:AsmSimulator: cancaling a reset thread."); this._thread_Result.Cancel(); } + AsmDudeToolsStatic.Output_INFO("AsmSimulator:AsmSimulator: delay_done event: going to start a reset event in a new thread."); this._thread_Result = this._threadPool.QueueWorkItem(this.Reset_Private); }; @@ -161,7 +162,6 @@ private AsmSimulator(ITextBuffer buffer, IBufferTagAggregatorFactoryService aggr else { AsmDudeToolsStatic.Output_INFO("AsmSimulator:AsmSimulator: switched off"); - this.Enabled = false; } } diff --git a/VS/CSHARP/asm-sim-lib/State.cs b/VS/CSHARP/asm-sim-lib/State.cs index f19a1e8d..cd30bb2b 100644 --- a/VS/CSHARP/asm-sim-lib/State.cs +++ b/VS/CSHARP/asm-sim-lib/State.cs @@ -68,19 +68,16 @@ private State(Tools tools) { this._tools = new Tools(tools); this._ctx = new Context(this._tools.Settings); - this.Solver = CreateSolver_LOCAL(); - this.Solver_U = CreateSolver_LOCAL(); + this.Solver = State.MakeSolver(this._ctx); + this.Solver_U = State.MakeSolver(this._ctx); this._branchInfoStore = new BranchInfoStore(this._ctx); this._cached_Reg_Values = new Dictionary(); this._cached_Flag_Values = new Dictionary(); + } - Solver CreateSolver_LOCAL() - { - return this._ctx.MkSolver(this._ctx.MkTactic("qfbv")); - //return this._ctx.MkSolver("QF_ABV"); - //return this._ctx.MkSolver(); - //return this._ctx.MkSolver("QF_BV"); - } + public static Solver MakeSolver(Context ctx) + { + return ctx.MkSolver(ctx.MkTactic("qfbv")); } /// Regular constructor @@ -386,7 +383,7 @@ public Tv Is_Redundant_Mem(string key1, string key2) Expr e1 = Tools.Mem_Key(key1, this._ctx); Expr e2 = Tools.Mem_Key(key2, this._ctx); BoolExpr e = this._ctx.MkEq(e1, e2); - Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this._ctx); + Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this._ctx, true); if (popNeeded) { diff --git a/VS/CSHARP/asm-sim-lib/ToolsZ3.cs b/VS/CSHARP/asm-sim-lib/ToolsZ3.cs index 008bcbe4..0ca34a99 100644 --- a/VS/CSHARP/asm-sim-lib/ToolsZ3.cs +++ b/VS/CSHARP/asm-sim-lib/ToolsZ3.cs @@ -616,76 +616,159 @@ public static Tv[] GetTvArray(BitVecExpr value, int nBits, Solver solver, Contex return results; } - public static Tv GetTv(BoolExpr value, BoolExpr undef, Solver solver, Solver solver_U, Context ctx) + public static Tv GetTv(BoolExpr value, BoolExpr undef, Solver solver, Solver solver_U, Context ctx, bool freshSolver = false) { try { - bool tvTrue; + return (freshSolver) + ? GetTv_Method1(value, undef, solver, solver_U, ctx) + : GetTv_Method2(value, undef, solver, solver_U, ctx); + } + catch (Exception e) + { + Console.WriteLine("ERROR: ToolsZ3: GetTv: e=" + e.ToString()); + return Tv.UNDETERMINED; + } + } + private static Tv GetTv_Method1(BoolExpr value, BoolExpr undef, Solver solver, Solver solver_U, Context ctx) + { + bool tvTrue; + { + Status status = solver.Check(value); + if (status == Status.UNKNOWN) { - Status status = solver.Check(value); + //Console.WriteLine("ToolsZ3:getTv5: A: value=" + value + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + return Tv.UNDETERMINED; + } + tvTrue = (status == Status.SATISFIABLE); + } + + //if (!tvTrue) return Tv5.ZERO; + + bool tvFalse; + { + Status status = solver.Check(ctx.MkNot(value)); + if (status == Status.UNKNOWN) + { + //Console.WriteLine("ToolsZ3:getTv5: B: value=" + ctx.MkNot(value) + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + return Tv.UNDETERMINED; + } + tvFalse = (status == Status.SATISFIABLE); + } + // if it consistent to assert that the provided bit is true, + // and seperately that it is consistent to be false, the model in the solver + // is indifferent about the truth-value of bit. + + if (!tvTrue && !tvFalse) return Tv.INCONSISTENT; // TODO: if inconsistent does not occur and !tvTrue is observed we can directly return Tv5.ZERO + if (!tvTrue && tvFalse) return Tv.ZERO; + if (tvTrue && !tvFalse) return Tv.ONE; + if (tvTrue && tvFalse) // truth value of bit cannot be determined is not known: it is either UNKNOWN or UNDEFINED + { + if (solver_U == null) return Tv.UNKNOWN; + bool tvFalseU; + { + Status status = solver_U.Check(ctx.MkNot(undef)); if (status == Status.UNKNOWN) { - //Console.WriteLine("ToolsZ3:getTv5: A: value=" + value + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + //Console.WriteLine("ToolsZ3:getTv5: C: undef=" + ctx.MkNot(undef) + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); return Tv.UNDETERMINED; } - tvTrue = (status == Status.SATISFIABLE); + tvFalseU = (status == Status.SATISFIABLE); } + // if (!tvFalseU) return Tv5.UNKNOWN; - //if (!tvTrue) return Tv5.ZERO; - - bool tvFalse; + bool tvTrueU; { - Status status = solver.Check(ctx.MkNot(value)); + Status status = solver_U.Check(undef); if (status == Status.UNKNOWN) { - //Console.WriteLine("ToolsZ3:getTv5: B: value=" + ctx.MkNot(value) + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + //Console.WriteLine("ToolsZ3:getTv5: D: undef=" + undef + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); return Tv.UNDETERMINED; } - tvFalse = (status == Status.SATISFIABLE); + tvTrueU = (status == Status.SATISFIABLE); } - // if it consistent to assert that the provided bit is true, - // and seperately that it is consistent to be false, the model in the solver - // is indifferent about the truth-value of bit. + return (tvTrueU && tvFalseU) ? Tv.UNDEFINED : Tv.UNKNOWN; + } + // unreachable + throw new Exception(); + } + private static Tv GetTv_Method2(BoolExpr value, BoolExpr undef, Solver solver, Solver solver_U, Context ctx) + { + Dictionary settings = new Dictionary(); - if (!tvTrue && !tvFalse) return Tv.INCONSISTENT; // TODO: if inconsistent does not occur and !tvTrue is observed we can directly return Tv5.ZERO - if (!tvTrue && tvFalse) return Tv.ZERO; - if (tvTrue && !tvFalse) return Tv.ONE; - if (tvTrue && tvFalse) // truth value of bit cannot be determined is not known: it is either UNKNOWN or UNDEFINED + bool tvTrue; + { + Solver s = State.MakeSolver(ctx); + s.Assert(solver.Assertions); + s.Assert(value); + Status status = s.Check(); + if (status == Status.UNKNOWN) { - if (solver_U == null) return Tv.UNKNOWN; - bool tvFalseU; + //Console.WriteLine("ToolsZ3:getTv5: A: value=" + value + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + return Tv.UNDETERMINED; + } + tvTrue = (status == Status.SATISFIABLE); + } + + //if (!tvTrue) return Tv5.ZERO; + + bool tvFalse; + { + Solver s = State.MakeSolver(ctx); + s.Assert(solver.Assertions); + s.Assert(ctx.MkNot(value)); + Status status = s.Check(); + if (status == Status.UNKNOWN) + { + //Console.WriteLine("ToolsZ3:getTv5: B: value=" + ctx.MkNot(value) + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + return Tv.UNDETERMINED; + } + tvFalse = (status == Status.SATISFIABLE); + } + // if it consistent to assert that the provided bit is true, + // and seperately that it is consistent to be false, the model in the solver + // is indifferent about the truth-value of bit. + + if (!tvTrue && !tvFalse) return Tv.INCONSISTENT; // TODO: if inconsistent does not occur and !tvTrue is observed we can directly return Tv5.ZERO + if (!tvTrue && tvFalse) return Tv.ZERO; + if (tvTrue && !tvFalse) return Tv.ONE; + if (tvTrue && tvFalse) // truth value of bit cannot be determined is not known: it is either UNKNOWN or UNDEFINED + { + if (solver_U == null) return Tv.UNKNOWN; + bool tvFalseU; + { + Solver s = State.MakeSolver(ctx); + s.Assert(solver_U.Assertions); + s.Assert(ctx.MkNot(undef)); + Status status = s.Check(); + if (status == Status.UNKNOWN) { - Status status = solver_U.Check(ctx.MkNot(undef)); - if (status == Status.UNKNOWN) - { - //Console.WriteLine("ToolsZ3:getTv5: C: undef=" + ctx.MkNot(undef) + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); - return Tv.UNDETERMINED; - } - tvFalseU = (status == Status.SATISFIABLE); + //Console.WriteLine("ToolsZ3:getTv5: C: undef=" + ctx.MkNot(undef) + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + return Tv.UNDETERMINED; } - // if (!tvFalseU) return Tv5.UNKNOWN; + tvFalseU = (status == Status.SATISFIABLE); + } + // if (!tvFalseU) return Tv5.UNKNOWN; - bool tvTrueU; + bool tvTrueU; + { + Solver s = State.MakeSolver(ctx); + s.Assert(solver_U.Assertions); + s.Assert(value); + Status status = s.Check(); + if (status == Status.UNKNOWN) { - Status status = solver_U.Check(undef); - if (status == Status.UNKNOWN) - { - //Console.WriteLine("ToolsZ3:getTv5: D: undef=" + undef + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); - return Tv.UNDETERMINED; - } - tvTrueU = (status == Status.SATISFIABLE); + //Console.WriteLine("ToolsZ3:getTv5: D: undef=" + undef + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); + return Tv.UNDETERMINED; } - return (tvTrueU && tvFalseU) ? Tv.UNDEFINED : Tv.UNKNOWN; + tvTrueU = (status == Status.SATISFIABLE); } - // unreachable - throw new Exception(); - } - catch (Exception e) - { - Console.WriteLine("ERROR: ToolsZ3: GetTv: e=" + e.ToString()); - return Tv.UNDETERMINED; + return (tvTrueU && tvFalseU) ? Tv.UNDEFINED : Tv.UNKNOWN; } + // unreachable + throw new Exception(); } + public static Tv GetTv(BoolExpr value, Solver solver, Context ctx) { try