Skip to content

Commit

Permalink
cleanup asm-sim
Browse files Browse the repository at this point in the history
  • Loading branch information
@HJLebbink
HJLebbink committed Oct 4, 2023
1 parent 3f13c63 commit b3b9046
Show file tree
Hide file tree
Showing 19 changed files with 1,243 additions and 1,311 deletions.
20 changes: 10 additions & 10 deletions VS/CSHARP/asm-sim-lib/BitOperations.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ public static class BitOperations
Contract.Requires(a != null);

BitVecExpr zero = ctx.MkBV(0, a.SortSize);
return Substract(zero, a, ctx);
return Subtract(zero, a, ctx);
}

#endregion
Expand All @@ -54,7 +54,7 @@ public static class BitOperations
BoolExpr cf = ToolsFlags.Create_CF_Add(a, b, a.SortSize, ctx);
BoolExpr of = ToolsFlags.Create_OF_Add(a, b, a.SortSize, ctx);
BoolExpr af = ToolsFlags.Create_AF_Add(a, b, ctx);
return (result: result, cf: cf, of: of, af: af);
return (result, cf, of, af);
}

public static (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) Addition(
Expand All @@ -80,10 +80,10 @@ public static class BitOperations
BoolExpr cf = ToolsFlags.Create_CF_Add(ax, bx2, nBits, ctx);
BoolExpr of = ToolsFlags.Create_OF_Add(ax, bx2, nBits, ctx);
BoolExpr af = ToolsFlags.Create_AF_Add(ax, bx2, ctx);
return (result: result, cf: cf, of: of, af: af);
return (result, cf, of, af);
}

public static (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) Substract(
public static (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) Subtract(
BitVecExpr a, BitVecExpr b, Context ctx)
{
Contract.Requires(ctx != null);
Expand All @@ -94,10 +94,10 @@ public static class BitOperations
BoolExpr cf = ToolsFlags.Create_CF_Sub(a, b, nBits, ctx);
BoolExpr of = ToolsFlags.Create_OF_Sub(a, b, nBits, ctx);
BoolExpr af = ToolsFlags.Create_AF_Sub(a, b, ctx);
return (result: result, cf: cf, of: of, af: af);
return (result, cf, of, af);
}

public static (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) Substract(
public static (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) Subtract(
BitVecExpr a, BitVecExpr b, BoolExpr carry, Context ctx)
{
Contract.Requires(a != null);
Expand All @@ -107,7 +107,7 @@ public static class BitOperations

if (carry.IsFalse)
{
return Substract(a, b, ctx);
return Subtract(a, b, ctx);
}

uint nBits = a.SortSize;
Expand All @@ -124,7 +124,7 @@ public static class BitOperations
BoolExpr cf = ToolsFlags.Create_CF_Sub(ax, bx2, nBits, ctx);
BoolExpr of = ToolsFlags.Create_OF_Sub(ax, bx2, nBits, ctx);
BoolExpr af = ToolsFlags.Create_AF_Sub(ax, bx2, ctx);
return (result: result, cf: cf, of: of, af: af);
return (result, cf, of, af);
}

#endregion
Expand Down Expand Up @@ -189,7 +189,7 @@ public static class BitOperations

BoolExpr cF_undef = Tools.Create_Flag_Key_Fresh(Flags.CF, rand, ctx);
BoolExpr cf = ctx.MkITE(ctx.MkEq(nShifts, ctx.MkBV(0, 8)), cF_undef, bitValue) as BoolExpr;
return (result: value_out, cf: cf);
return (result: value_out, cf);
}

public static (BitVecExpr result, BoolExpr cf) ShiftOperations(
Expand Down Expand Up @@ -238,7 +238,7 @@ public static class BitOperations

BoolExpr cf = ctx.MkITE(ctx.MkEq(nShifts, ctx.MkBV(0, 8)), cf_current, bitValue) as BoolExpr;
//Console.WriteLine("ShiftOperations:cf=" + cf);
return (result: value_out, cf: cf);
return (result: value_out, cf);
}
#endregion
}
Expand Down
4 changes: 3 additions & 1 deletion VS/CSHARP/asm-sim-lib/BranchInfo.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ public class BranchInfo
public BranchInfo(BoolExpr condition, bool taken)
{
Contract.Requires(condition != null);

Contract.Assert(condition != null);
this.BranchCondition = condition;
this.Key = condition.ToString();
this.BranchTaken = taken;
Expand All @@ -48,6 +48,8 @@ public BranchInfo Translate(Context ctx)
public BoolExpr GetData(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Assert(ctx != null);

if (false)
{
BoolExpr bc = this.BranchCondition.Translate(ctx) as BoolExpr;
Expand Down
4 changes: 2 additions & 2 deletions VS/CSHARP/asm-sim-lib/BranchInfoStore.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ public void Clear()
}
}

BranchInfoStore mergeBranchStore = new BranchInfoStore(ctx);
BranchInfoStore mergeBranchStore = new(ctx);
if (sharedKeys.Count == 0)
{
if (store1.branchInfo_ != null)
Expand Down Expand Up @@ -232,7 +232,7 @@ public void Add(IDictionary<string, BranchInfo> branchInfo, bool translate)

public override string ToString()
{
StringBuilder sb = new StringBuilder();
StringBuilder sb = new();
if ((this.branchInfo_ != null) && (this.branchInfo_.Count > 0))
{
sb.AppendLine("Branch control flow constraints:");
Expand Down
199 changes: 97 additions & 102 deletions VS/CSHARP/asm-sim-lib/DynamicFlow.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -616,7 +616,7 @@ private void ToString(string key, StaticFlow sFlow, ref StringBuilder sb)
}
}

public string ToStringOverview(StaticFlow flow, bool showRegisterValues = false)
public static string ToStringOverview(StaticFlow flow, bool showRegisterValues = false)
{
return "TODO";
}
Expand Down Expand Up @@ -680,8 +680,8 @@ private State Create_State_Private(string key, bool after)
}
default:
{
(string source, StateUpdate stateUpdate) incoming_Regular = this.Get_Regular(this.graph_.InEdges(key_LOCAL));
IEnumerable<(string source, StateUpdate stateUpdate)> incoming_Branches = this.Get_Branches(this.graph_.InEdges(key_LOCAL));
(string source, StateUpdate stateUpdate) incoming_Regular = Get_Regular(this.graph_.InEdges(key_LOCAL));
IEnumerable<(string source, StateUpdate stateUpdate)> incoming_Branches = Get_Branches(this.graph_.InEdges(key_LOCAL));
result = Merge_State_Update_LOCAL(key_LOCAL, incoming_Regular, incoming_Branches, visited_LOCAL);
if (result == null)
{
Expand Down Expand Up @@ -738,128 +738,123 @@ private State Create_State_Private(string key, bool after)
ICollection<string> visited2)
{
string source1 = incoming_Regular.source;
using (State state1 = Construct_State_Private_LOCAL(source1, false, new List<string>(visited2)))
using State state1 = Construct_State_Private_LOCAL(source1, false, new List<string>(visited2));
if (state1 == null)
{
if (state1 == null)
{
return null;
}
return null;
}

string nextKey1 = target + "A0";
{
StateUpdate update1 = incoming_Regular.stateUpdate;
update1.NextKey = nextKey1;
state1.Update_Forward(update1);
}
State result_State = new(this.tools_, state1.TailKey, state1.HeadKey);
string nextKey1 = target + "A0";
{
StateUpdate update1 = incoming_Regular.stateUpdate;
update1.NextKey = nextKey1;
state1.Update_Forward(update1);
}
State result_State = new(this.tools_, state1.TailKey, state1.HeadKey);

IList<StateUpdate> mergeStateUpdates = new List<StateUpdate>();
HashSet<BoolExpr> tempSet1 = new();
HashSet<BoolExpr> tempSet2 = new();
HashSet<string> sharedBranchConditions = new();
List<BranchInfo> allBranchConditions = new();
IList<StateUpdate> mergeStateUpdates = new List<StateUpdate>();
HashSet<BoolExpr> tempSet1 = new();
HashSet<BoolExpr> tempSet2 = new();
HashSet<string> sharedBranchConditions = new();
List<BranchInfo> allBranchConditions = new();

foreach (BoolExpr v1 in state1.Solver.Assertions)
{
tempSet1.Add(v1);
}
foreach (BoolExpr v1 in state1.Solver.Assertions)
{
tempSet1.Add(v1);
}

foreach (BoolExpr v1 in state1.Solver_U.Assertions)
{
tempSet2.Add(v1);
}

foreach (BoolExpr v1 in state1.Solver_U.Assertions)
foreach (BranchInfo v1 in state1.BranchInfoStore.Values)
{
allBranchConditions.Add(v1);
}

int counter = 0;
List<(string source, StateUpdate stateUpdate)> incoming_Branches_list = new(incoming_Branches);
incoming_Branches_list.Reverse(); //TODO does this always works??
int nBranches = incoming_Branches_list.Count;
foreach ((string source, StateUpdate stateUpdate) incoming_Branch in incoming_Branches_list)
{
string source2 = incoming_Branch.source;
using State state2 = Construct_State_Private_LOCAL(source2, false, new List<string>(visited2));
// recursive call
if (state2 == null)
{
tempSet2.Add(v1);
return null;
}

foreach (BranchInfo v1 in state1.BranchInfoStore.Values)
string nextKey2 = target + "B" + counter;
counter++;
{
allBranchConditions.Add(v1);
StateUpdate update2 = incoming_Branch.stateUpdate;
update2.NextKey = nextKey2; //TODO BUG here, is the reference updated???
state2.Update_Forward(update2);
}

int counter = 0;
List<(string source, StateUpdate stateUpdate)> incoming_Branches_list = new(incoming_Branches);
incoming_Branches_list.Reverse(); //TODO does this always works??
int nBranches = incoming_Branches_list.Count;
foreach ((string source, StateUpdate stateUpdate) incoming_Branch in incoming_Branches_list)
BoolExpr bc = null;
{
string source2 = incoming_Branch.source;
using (State state2 = Construct_State_Private_LOCAL(source2, false, new List<string>(visited2)))
{ // recursive call
if (state2 == null)
{
return null;
}

string nextKey2 = target + "B" + counter;
counter++;
{
StateUpdate update2 = incoming_Branch.stateUpdate;
update2.NextKey = nextKey2; //TODO BUG here, is the reference updated???
state2.Update_Forward(update2);
}

BoolExpr bc = null;
using (Context ctx = new(this.tools_.ContextSettings))
{
string branchKey = GraphTools<(bool, StateUpdate)>.Get_Branch_Point(source1, source2, this.graph_);
BranchInfo branchInfo = Get_Branch_Condition_LOCAL(branchKey);
if (branchInfo == null)
{
using (Context ctx = new(this.tools_.ContextSettings))
{
string branchKey = GraphTools<(bool, StateUpdate)>.Get_Branch_Point(source1, source2, this.graph_);
BranchInfo branchInfo = Get_Branch_Condition_LOCAL(branchKey);
if (branchInfo == null)
{
Console.WriteLine("WARNING: DynamicFlow:Construct_State_Private:GetStates_LOCAL: branchInfo is null. source1=" + source1 + "; source2=" + source2);
bc = ctx.MkBoolConst("BC" + target);
}
else
{
bc = branchInfo.BranchCondition;
sharedBranchConditions.Add(bc.ToString());
}
}
string nextKey3 = (counter == nBranches) ? target : target + "A" + counter;

using (StateUpdate stateUpdate = new(bc, nextKey2, nextKey1, nextKey3, this.tools_))
{
nextKey1 = nextKey3;
mergeStateUpdates.Add(stateUpdate);
}
Console.WriteLine("WARNING: DynamicFlow:Construct_State_Private:GetStates_LOCAL: branchInfo is null. source1=" + source1 + "; source2=" + source2);
bc = ctx.MkBoolConst("BC" + target);
}
if (state1.TailKey != state2.TailKey)
else
{
Console.WriteLine("WARNING: DynamicFlow: Merge_State_Update_LOCAL: tails are unequal: tail1=" + state1.TailKey + "; tail2=" + state2.TailKey);
bc = branchInfo.BranchCondition;
sharedBranchConditions.Add(bc.ToString());
}
{ // merge the states state1 and state2 into state3
foreach (BoolExpr v1 in state2.Solver.Assertions)
{
tempSet1.Add(v1);
}
}
string nextKey3 = (counter == nBranches) ? target : target + "A" + counter;

foreach (BoolExpr v1 in state2.Solver_U.Assertions)
{
tempSet2.Add(v1);
}
using StateUpdate stateUpdate = new(bc, nextKey2, nextKey1, nextKey3, this.tools_);
nextKey1 = nextKey3;
mergeStateUpdates.Add(stateUpdate);
}
if (state1.TailKey != state2.TailKey)
{
Console.WriteLine("WARNING: DynamicFlow: Merge_State_Update_LOCAL: tails are unequal: tail1=" + state1.TailKey + "; tail2=" + state2.TailKey);
}
{ // merge the states state1 and state2 into state3
foreach (BoolExpr v1 in state2.Solver.Assertions)
{
tempSet1.Add(v1);
}

foreach (BranchInfo v1 in state2.BranchInfoStore.Values)
{
allBranchConditions.Add(v1);
}
}
foreach (BoolExpr v1 in state2.Solver_U.Assertions)
{
tempSet2.Add(v1);
}
}
result_State.Assert(tempSet1, false, true);
result_State.Assert(tempSet2, true, true);

foreach (BranchInfo v1 in allBranchConditions)
{
if (!sharedBranchConditions.Contains(v1.BranchCondition.ToString()))
foreach (BranchInfo v1 in state2.BranchInfoStore.Values)
{
result_State.Add(v1);
allBranchConditions.Add(v1);
}
}
foreach (StateUpdate v1 in mergeStateUpdates)
}
result_State.Assert(tempSet1, false, true);
result_State.Assert(tempSet2, true, true);

foreach (BranchInfo v1 in allBranchConditions)
{
if (!sharedBranchConditions.Contains(v1.BranchCondition.ToString()))
{
result_State.Update_Forward(v1);
v1.Dispose();
result_State.Add(v1);
}
return result_State;
}
foreach (StateUpdate v1 in mergeStateUpdates)
{
result_State.Update_Forward(v1);
v1.Dispose();
}
return result_State;
}

BranchInfo? Get_Branch_Condition_LOCAL(string branchKey)
Expand Down Expand Up @@ -892,7 +887,7 @@ private State Create_State_Private(string key, bool after)
#endregion
}

private (string source, StateUpdate stateUpdate) Get_Regular(IEnumerable<TaggedEdge<string, (bool branch, StateUpdate stateUpdate)>> inEdges)
private static (string source, StateUpdate stateUpdate) Get_Regular(IEnumerable<TaggedEdge<string, (bool branch, StateUpdate stateUpdate)>> inEdges)
{
foreach (TaggedEdge<string, (bool branch, StateUpdate stateUpdate)> v in inEdges)
{
Expand All @@ -905,13 +900,13 @@ private State Create_State_Private(string key, bool after)
return (source: "NOKEY", stateUpdate: null);
}

private IEnumerable<(string source, StateUpdate stateUpdate)> Get_Branches(IEnumerable<TaggedEdge<string, (bool branch, StateUpdate stateUpdate)>> inEdges)
private static IEnumerable<(string source, StateUpdate stateUpdate)> Get_Branches(IEnumerable<TaggedEdge<string, (bool branch, StateUpdate stateUpdate)>> inEdges)
{
foreach (TaggedEdge<string, (bool branch, StateUpdate stateUpdate)> v in inEdges)
{
if (v.Tag.branch)
{
yield return (source: v.Source, stateUpdate: v.Tag.stateUpdate);
yield return (source: v.Source, v.Tag.stateUpdate);
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion VS/CSHARP/asm-sim-lib/ExecutionTree.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ public ExecutionTree(Tools tools)
this.states_ = new Dictionary<string, State>();
}

public void Init(DynamicFlow dFlow, int startLineNumber)
public static void Init(DynamicFlow dFlow, int startLineNumber)
{
// Unroll the provided dFlow in depth first until either the maximum depth is reached or the state is inconsistent.
/*
Expand Down
Loading

0 comments on commit b3b9046

Please sign in to comment.