Skip to content

Commit

Permalink
AsmSim update
Browse files Browse the repository at this point in the history
  • Loading branch information
@HJLebbink
HJLebbink committed Jun 16, 2017
1 parent c46281a commit d5d14b6
Show file tree
Hide file tree
Showing 6 changed files with 190 additions and 65 deletions.
45 changes: 45 additions & 0 deletions VS/CPP/ConsoleTest/example_semantic_analysis2.asm
View file
Original file line number Diff line number Diff line change
@@ -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)

12 changes: 6 additions & 6 deletions VS/CSHARP/asm-dude-vsix/Resources/examples/example_semantic_analysis.asm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -16,22 +16,22 @@
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
mov rax, ptr qword [rax]
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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion VS/CSHARP/asm-dude-vsix/Squiggles/SquigglesTagger.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
};
Expand Down
8 changes: 4 additions & 4 deletions VS/CSHARP/asm-dude-vsix/Tools/AsmSimulator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<int, State>();
this._cached_States_Before = new Dictionary<int, State>();
Expand Down Expand Up @@ -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);
};

Expand All @@ -161,7 +162,6 @@ private AsmSimulator(ITextBuffer buffer, IBufferTagAggregatorFactoryService aggr
else
{
AsmDudeToolsStatic.Output_INFO("AsmSimulator:AsmSimulator: switched off");
this.Enabled = false;
}
}

Expand Down
17 changes: 7 additions & 10 deletions VS/CSHARP/asm-sim-lib/State.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Rn, Tv[]>();
this._cached_Flag_Values = new Dictionary<Flags, Tv>();
}

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"));
}

/// <summary>Regular constructor</summary>
Expand Down Expand Up @@ -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)
{
Expand Down
171 changes: 127 additions & 44 deletions VS/CSHARP/asm-sim-lib/ToolsZ3.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<string, string> settings = new Dictionary<string, string>();

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
Expand Down

0 comments on commit d5d14b6

Please sign in to comment.