From b3b904689824a87a3e3e44239668724d8f6d425e Mon Sep 17 00:00:00 2001 From: Henk-Jan Lebbink Date: Wed, 4 Oct 2023 08:38:17 +0200 Subject: [PATCH] cleanup asm-sim --- VS/CSHARP/asm-sim-lib/BitOperations.cs | 20 +- VS/CSHARP/asm-sim-lib/BranchInfo.cs | 4 +- VS/CSHARP/asm-sim-lib/BranchInfoStore.cs | 4 +- VS/CSHARP/asm-sim-lib/DynamicFlow.cs | 199 ++- VS/CSHARP/asm-sim-lib/ExecutionTree.cs | 2 +- VS/CSHARP/asm-sim-lib/GraphTools.cs | 14 +- VS/CSHARP/asm-sim-lib/Mnemonics.cs | 76 +- VS/CSHARP/asm-sim-lib/ProgramGenerator.cs | 12 +- VS/CSHARP/asm-sim-lib/ProgramSyntesizer.cs | 56 +- VS/CSHARP/asm-sim-lib/Runner.cs | 19 +- VS/CSHARP/asm-sim-lib/State.cs | 214 ++- VS/CSHARP/asm-sim-lib/StateUpdate.cs | 68 +- VS/CSHARP/asm-sim-lib/StaticFlow.cs | 54 +- VS/CSHARP/asm-sim-lib/Tools.cs | 20 +- VS/CSHARP/asm-sim-lib/ToolsFlags.cs | 12 +- VS/CSHARP/asm-sim-lib/ToolsZ3.cs | 221 ++- VS/CSHARP/asm-sim-lib/asm-sim-lib.csproj | 10 +- VS/CSHARP/asm-sim-main/DotVisualizer.cs | 6 +- VS/CSHARP/asm-sim-main/ProgramZ3.cs | 1543 ++++++++++---------- 19 files changed, 1243 insertions(+), 1311 deletions(-) diff --git a/VS/CSHARP/asm-sim-lib/BitOperations.cs b/VS/CSHARP/asm-sim-lib/BitOperations.cs index b76d6927..54662fa5 100644 --- a/VS/CSHARP/asm-sim-lib/BitOperations.cs +++ b/VS/CSHARP/asm-sim-lib/BitOperations.cs @@ -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 @@ -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( @@ -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); @@ -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); @@ -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; @@ -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 @@ -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( @@ -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 } diff --git a/VS/CSHARP/asm-sim-lib/BranchInfo.cs b/VS/CSHARP/asm-sim-lib/BranchInfo.cs index c5553729..2e873f63 100644 --- a/VS/CSHARP/asm-sim-lib/BranchInfo.cs +++ b/VS/CSHARP/asm-sim-lib/BranchInfo.cs @@ -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; @@ -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; diff --git a/VS/CSHARP/asm-sim-lib/BranchInfoStore.cs b/VS/CSHARP/asm-sim-lib/BranchInfoStore.cs index 5259b6cc..8d1df527 100644 --- a/VS/CSHARP/asm-sim-lib/BranchInfoStore.cs +++ b/VS/CSHARP/asm-sim-lib/BranchInfoStore.cs @@ -126,7 +126,7 @@ public void Clear() } } - BranchInfoStore mergeBranchStore = new BranchInfoStore(ctx); + BranchInfoStore mergeBranchStore = new(ctx); if (sharedKeys.Count == 0) { if (store1.branchInfo_ != null) @@ -232,7 +232,7 @@ public void Add(IDictionary 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:"); diff --git a/VS/CSHARP/asm-sim-lib/DynamicFlow.cs b/VS/CSHARP/asm-sim-lib/DynamicFlow.cs index 8b0f622f..68bc7e4f 100644 --- a/VS/CSHARP/asm-sim-lib/DynamicFlow.cs +++ b/VS/CSHARP/asm-sim-lib/DynamicFlow.cs @@ -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"; } @@ -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) { @@ -738,128 +738,123 @@ private State Create_State_Private(string key, bool after) ICollection visited2) { string source1 = incoming_Regular.source; - using (State state1 = Construct_State_Private_LOCAL(source1, false, new List(visited2))) + using State state1 = Construct_State_Private_LOCAL(source1, false, new List(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 mergeStateUpdates = new List(); - HashSet tempSet1 = new(); - HashSet tempSet2 = new(); - HashSet sharedBranchConditions = new(); - List allBranchConditions = new(); + IList mergeStateUpdates = new List(); + HashSet tempSet1 = new(); + HashSet tempSet2 = new(); + HashSet sharedBranchConditions = new(); + List 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(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(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) @@ -892,7 +887,7 @@ private State Create_State_Private(string key, bool after) #endregion } - private (string source, StateUpdate stateUpdate) Get_Regular(IEnumerable> inEdges) + private static (string source, StateUpdate stateUpdate) Get_Regular(IEnumerable> inEdges) { foreach (TaggedEdge v in inEdges) { @@ -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> inEdges) + private static IEnumerable<(string source, StateUpdate stateUpdate)> Get_Branches(IEnumerable> inEdges) { foreach (TaggedEdge v in inEdges) { if (v.Tag.branch) { - yield return (source: v.Source, stateUpdate: v.Tag.stateUpdate); + yield return (source: v.Source, v.Tag.stateUpdate); } } } diff --git a/VS/CSHARP/asm-sim-lib/ExecutionTree.cs b/VS/CSHARP/asm-sim-lib/ExecutionTree.cs index 57746683..effe2f1e 100644 --- a/VS/CSHARP/asm-sim-lib/ExecutionTree.cs +++ b/VS/CSHARP/asm-sim-lib/ExecutionTree.cs @@ -41,7 +41,7 @@ public ExecutionTree(Tools tools) this.states_ = new Dictionary(); } - 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. /* diff --git a/VS/CSHARP/asm-sim-lib/GraphTools.cs b/VS/CSHARP/asm-sim-lib/GraphTools.cs index 975c4336..3d657bd9 100644 --- a/VS/CSHARP/asm-sim-lib/GraphTools.cs +++ b/VS/CSHARP/asm-sim-lib/GraphTools.cs @@ -34,7 +34,7 @@ public static IEnumerable Get_Branch_Points_Backwards(string vertex, Bid { Contract.Requires(graph != null); - HashSet visited = new HashSet(); + HashSet visited = new(); return Get_Branch_Points_Backwards_LOCAL(vertex); #region Local Method @@ -72,7 +72,7 @@ public static IEnumerable Get_First_Branch_Point_Backwards(string vertex { Contract.Requires(graph != null); - HashSet visited = new HashSet(); + HashSet visited = new(); return Get_Branch_Point_Backwards_LOCAL(vertex); #region Local Method @@ -129,8 +129,8 @@ public static IEnumerable Get_First_Mutual_Branch_Point_Backwards(string if (s1 != s2) { - HashSet branchPoints1 = new HashSet(); - HashSet branchPoints2 = new HashSet(); + HashSet branchPoints1 = new(); + HashSet branchPoints2 = new(); foreach (string v in Get_First_Branch_Point_Backwards(s1, graph)) { @@ -162,8 +162,8 @@ public static string Get_Branch_Point(string vertex1, string vertex2, Bidirectio return vertex1; } - HashSet branchPoints1 = new HashSet(); - HashSet branchPoints2 = new HashSet(); + HashSet branchPoints1 = new(); + HashSet branchPoints2 = new(); foreach (string v in Get_Branch_Points_Backwards(vertex1, graph)) { @@ -175,7 +175,7 @@ public static string Get_Branch_Point(string vertex1, string vertex2, Bidirectio branchPoints2.Add(v); } - List m = new List(branchPoints1.Intersect(branchPoints2)); + List m = new(branchPoints1.Intersect(branchPoints2)); switch (m.Count) { case 0: diff --git a/VS/CSHARP/asm-sim-lib/Mnemonics.cs b/VS/CSHARP/asm-sim-lib/Mnemonics.cs index df22a25f..cb1df24e 100644 --- a/VS/CSHARP/asm-sim-lib/Mnemonics.cs +++ b/VS/CSHARP/asm-sim-lib/Mnemonics.cs @@ -57,29 +57,19 @@ public abstract class OpcodeBase : IDisposable protected void Create_RegularUpdate() { - if (this.regularUpdate_ == null) - { - this.regularUpdate_ = new StateUpdate(this.keys_.prevKey, this.keys_.nextKey, this.tools_); - } + this.regularUpdate_ ??= new StateUpdate(this.keys_.prevKey, this.keys_.nextKey, this.tools_); } protected void Create_BranchUpdate() { - if (this.branchUpdate_ == null) - { - this.branchUpdate_ = new StateUpdate(this.keys_.prevKey, this.keys_.nextKeyBranch, this.tools_); - } + this.branchUpdate_ ??= new StateUpdate(this.keys_.prevKey, this.keys_.nextKeyBranch, this.tools_); } protected StateUpdate RegularUpdate { get { - if (this.regularUpdate_ == null) - { - this.regularUpdate_ = new StateUpdate(this.keys_.prevKey, this.keys_.nextKey, this.tools_); - } - + this.regularUpdate_ ??= new StateUpdate(this.keys_.prevKey, this.keys_.nextKey, this.tools_); return this.regularUpdate_; } } @@ -88,11 +78,7 @@ protected StateUpdate BranchUpdate { get { - if (this.branchUpdate_ == null) - { - this.branchUpdate_ = new StateUpdate(this.keys_.prevKey, this.keys_.nextKeyBranch, this.tools_); - } - + this.branchUpdate_ ??= new StateUpdate(this.keys_.prevKey, this.keys_.nextKeyBranch, this.tools_); return this.branchUpdate_; } } @@ -101,6 +87,8 @@ public OpcodeBase(Mnemonic m, string[] args, (string prevKey, string nextKey, st { Contract.Requires(t != null); Contract.Requires(args != null); + Contract.Assume(t != null); + Contract.Assume(args != null); this.mnemonic_ = m; this.args_ = args; @@ -215,7 +203,7 @@ protected set public bool IsHalted { get { return this.halted_; } } - public string SyntaxError + public string? SyntaxError { get { @@ -224,7 +212,7 @@ public string SyntaxError protected set { - if (this.haltMessage_ == null) + if (string.IsNullOrEmpty(this.haltMessage_)) { this.haltMessage_ = value; } @@ -246,7 +234,7 @@ public override string ToString() /// Gets number of operand of the arguments of this instruction protected int NOperands { get { return this.args_.Length; } } - public static BitVecExpr OpValue( + public static BitVecExpr? OpValue( Operand operand, string key, Context ctx, @@ -254,6 +242,9 @@ public override string ToString() { Contract.Requires(operand != null); Contract.Requires(ctx != null); + Contract.Assume(operand != null); + Contract.Assume(ctx != null); + try { @@ -296,17 +287,17 @@ public override string ToString() } } - protected bool ToMemReadWrite(Operand op1) + protected static bool ToMemReadWrite(Operand op1) { return (op1 == null) ? false : op1.IsMem; } - protected bool ToMemReadWrite(Operand op1, Operand op2) + protected static bool ToMemReadWrite(Operand op1, Operand op2) { return ((op1 == null) ? false : op1.IsMem) || ((op2 == null) ? false : op2.IsMem); } - protected bool ToMemReadWrite(Operand op1, Operand op2, Operand op3) + protected static bool ToMemReadWrite(Operand op1, Operand op2, Operand op3) { return ((op1 == null) ? false : op1.IsMem) || ((op2 == null) ? false : op2.IsMem) || ((op3 == null) ? false : op3.IsMem); } @@ -410,6 +401,8 @@ protected void CreateSyntaxError1(Operand op1, Operand op2) { Contract.Requires(op1 != null); Contract.Requires(op2 != null); + Contract.Assume(op1 != null); + Contract.Assume(op2 != null); this.SyntaxError = string.Format(Culture, "\"{0}\": Operand 1 and 2 should have same number of bits. Operand1={1} ({2}, bits={3}); Operand2={4} ({5}, bits={6})", this.ToString(), op1, op1.Type, op1.NBits, op2, op2.Type, op2.NBits); } @@ -457,6 +450,7 @@ public Opcode0Base(Mnemonic mnemonic, string[] args, (string prevKey, string nex : base(mnemonic, args, keys, t) { Contract.Requires(args != null); + Contract.Assume(args != null); if (this.NOperands != 0) { @@ -469,7 +463,7 @@ public Opcode0Base(Mnemonic mnemonic, string[] args, (string prevKey, string nex public abstract class Opcode1Base : OpcodeBase { - protected readonly Operand op1_; + protected readonly Operand? op1_; public Opcode1Base(Mnemonic mnemonic, string[] args, (string prevKey, string nextKey, string nextKeyBranch) keys, Tools t) : base(mnemonic, args, keys, t) @@ -513,9 +507,9 @@ public Opcode1Base(Mnemonic mnemonic, string[] args, Ot1 allowedOperands1, (stri public BitVecExpr Op1Value { get { return OpValue(this.op1_, this.keys_.prevKey, this.ctx_); } } - public override bool MemReadStatic { get { return this.ToMemReadWrite(this.op1_); } } + public override bool MemReadStatic { get { return ToMemReadWrite(this.op1_); } } - public override bool MemWriteStatic { get { return this.ToMemReadWrite(this.op1_); } } + public override bool MemWriteStatic { get { return ToMemReadWrite(this.op1_); } } } public abstract class Opcode2Base : OpcodeBase @@ -575,9 +569,9 @@ public Opcode2Base(Mnemonic mnemonic, string[] args, Ot2 allowedOperands2, (stri public BitVecExpr Op2Value { get { return OpValue(this.op2_, this.keys_.prevKey, this.ctx_); } } - public override bool MemReadStatic { get { return this.ToMemReadWrite(this.op1_, this.op2_); } } + public override bool MemReadStatic { get { return ToMemReadWrite(this.op1_, this.op2_); } } - public override bool MemWriteStatic { get { return this.ToMemReadWrite(this.op1_, this.op2_); } } + public override bool MemWriteStatic { get { return ToMemReadWrite(this.op1_, this.op2_); } } } public abstract class Opcode3Base : OpcodeBase @@ -645,9 +639,9 @@ public Opcode3Base(Mnemonic mnemonic, string[] args, Ot3 allowedOperands3, (stri public BitVecExpr Op3Value { get { return OpValue(this.op3_, this.keys_.prevKey, this.ctx_); } } - public override bool MemReadStatic { get { return this.ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } + public override bool MemReadStatic { get { return ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } - public override bool MemWriteStatic { get { return this.ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } + public override bool MemWriteStatic { get { return ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } } public abstract class OpcodeNBase : OpcodeBase @@ -697,9 +691,9 @@ public OpcodeNBase(Mnemonic mnemonic, string[] args, int maxNArgs, (string prevK public BitVecExpr Op3Value { get { return OpValue(this.op3_, this.keys_.prevKey, this.ctx_); } } - public override bool MemReadStatic { get { return this.ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } + public override bool MemReadStatic { get { return ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } - public override bool MemWriteStatic { get { return this.ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } + public override bool MemWriteStatic { get { return ToMemReadWrite(this.op1_, this.op2_, this.op3_); } } } public abstract class Opcode2Type1 : Opcode2Base @@ -1025,7 +1019,7 @@ public override void Execute() this.RegularUpdate.Set(this.op1_, this.ctx_.MkITE(zf, this.Op2Value, op1) as BitVecExpr); this.RegularUpdate.Set(regA, this.ctx_.MkITE(zf, regA_Expr_Curr, op1) as BitVecExpr); - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(this.Op1Value, this.Op2Value, this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(this.Op1Value, this.Op2Value, this.ctx_); this.RegularUpdate.Set(Flags.CF, cf); this.RegularUpdate.Set(Flags.OF, of); this.RegularUpdate.Set(Flags.AF, af); @@ -1801,7 +1795,7 @@ public Sub(string[] args, (string prevKey, string nextKey, string nextKeyBranch) public override void Execute() { - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(this.Op1Value, this.Op2Value, this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(this.Op1Value, this.Op2Value, this.ctx_); this.RegularUpdate.Set(this.op1_, result); this.RegularUpdate.Set(Flags.CF, cf); this.RegularUpdate.Set(Flags.OF, of); @@ -1824,7 +1818,7 @@ public Sbb(string[] args, (string prevKey, string nextKey, string nextKeyBranch) public override void Execute() { - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(this.Op1Value, this.Op2Value, this.Get(Flags.CF), this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(this.Op1Value, this.Op2Value, this.Get(Flags.CF), this.ctx_); this.RegularUpdate.Set(this.op1_, result); this.RegularUpdate.Set(Flags.CF, cf); this.RegularUpdate.Set(Flags.OF, of); @@ -2564,7 +2558,7 @@ public Dec(string[] args, (string prevKey, string nextKey, string nextKeyBranch) public override void Execute() { - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(this.Op1Value, this.ctx_.MkBV(1, (uint)this.op1_.NBits), this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(this.Op1Value, this.ctx_.MkBV(1, (uint)this.op1_.NBits), this.ctx_); this.RegularUpdate.Set(this.op1_, result); //CF is not updated! this.RegularUpdate.Set(Flags.OF, of); @@ -2610,7 +2604,7 @@ public Cmp(string[] args, (string prevKey, string nextKey, string nextKeyBranch) public override void Execute() { - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(this.Op1Value, this.Op2Value, this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(this.Op1Value, this.Op2Value, this.ctx_); this.RegularUpdate.Set(Flags.CF, cf); this.RegularUpdate.Set(Flags.OF, of); this.RegularUpdate.Set(Flags.AF, af); @@ -3051,7 +3045,7 @@ public static (BitVecExpr shiftCount, BoolExpr tooLarge) GetShiftCount(BitVecExp BitVecNum shiftMask = ctx.MkBV((nBits == 64) ? 0x3F : 0x1F, 8); BoolExpr tooLarge = ctx.MkBVSGE(value, ctx.MkBV((nBits == 64) ? 64 : 32, 8)); BitVecExpr shiftCount = ctx.MkBVAND(value, shiftMask); - return (shiftCount: shiftCount, tooLarge: tooLarge); + return (shiftCount, tooLarge); } public void UpdateFlagsShift(BitVecExpr value, BoolExpr cfIn, BitVecExpr shiftCount, BoolExpr shiftTooLarge, bool left) @@ -4371,7 +4365,7 @@ public override void Execute() if (this.prefix_ == Mnemonic.NONE) { - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(this.GetMem(src, this.nBytes_), this.GetMem(dst, this.nBytes_), this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(this.GetMem(src, this.nBytes_), this.GetMem(dst, this.nBytes_), this.ctx_); this.RegularUpdate.Set(Flags.CF, cf); this.RegularUpdate.Set(Flags.OF, of); @@ -4557,7 +4551,7 @@ public override void Execute() if (this.prefix_ == Mnemonic.NONE) { - (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Substract(accumulator, this.GetMem(dst, this.nBytes_), this.ctx_); + (BitVecExpr result, BoolExpr cf, BoolExpr of, BoolExpr af) = BitOperations.Subtract(accumulator, this.GetMem(dst, this.nBytes_), this.ctx_); this.RegularUpdate.Set(Flags.CF, cf); this.RegularUpdate.Set(Flags.OF, of); diff --git a/VS/CSHARP/asm-sim-lib/ProgramGenerator.cs b/VS/CSHARP/asm-sim-lib/ProgramGenerator.cs index 353cc535..aaf50541 100644 --- a/VS/CSHARP/asm-sim-lib/ProgramGenerator.cs +++ b/VS/CSHARP/asm-sim-lib/ProgramGenerator.cs @@ -45,18 +45,18 @@ public ProgramGenerator() public string RandomProgram(int nInstructions) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); for (int i = 0; i < nInstructions; ++i) { Mnemonic m = this._eligibleMnemonics[this._rand.Next(this._eligibleMnemonics.Count)]; Rn reg1 = this.RandomReg(); Rn reg2 = this.RandomReg(); - sb.AppendLine(this.MakeCodeLine(m, reg1, reg2)); + sb.AppendLine(MakeCodeLine(m, reg1, reg2)); } return sb.ToString().TrimEnd(); } - public string ShuffleProgram(string program) { + public static string ShuffleProgram(string program) { return program; } @@ -74,12 +74,12 @@ public Rn RandomReg() } } - private string ToString(Flags flag, State state) + private static string ToString(Flags flag, State state) { char c = ToolsZ3.ToStringBin(state.GetTv(flag)); return c+""; } - private string ToString(Rn name, State state) + private static string ToString(Rn name, State state) { Tv[] array = state.GetTvArray(name); var tup = ToolsZ3.HasOneValue(array); @@ -91,7 +91,7 @@ private string ToString(Rn name, State state) } } - private string MakeCodeLine(Mnemonic mnemonic, Rn reg1, Rn reg2) + private static string MakeCodeLine(Mnemonic mnemonic, Rn reg1, Rn reg2) { switch (mnemonic) { diff --git a/VS/CSHARP/asm-sim-lib/ProgramSyntesizer.cs b/VS/CSHARP/asm-sim-lib/ProgramSyntesizer.cs index 2c70411c..14bec04d 100644 --- a/VS/CSHARP/asm-sim-lib/ProgramSyntesizer.cs +++ b/VS/CSHARP/asm-sim-lib/ProgramSyntesizer.cs @@ -47,7 +47,7 @@ public ProgramSyntesizer(int nLines, IList registers) this._registers = registers; - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "true" }, // enable generation of unsat cores { "model", "true" }, // enable model generation @@ -144,7 +144,7 @@ public void Run() #endregion - Console.WriteLine(this.ToString(this._solver)); + Console.WriteLine(ToString(this._solver)); if (this._solver.Check() == Status.SATISFIABLE) { this.GetAllModels(this._solver, ctx); @@ -246,12 +246,12 @@ private static BoolExpr ZeroFlag(Rn reg, int lineNumber, Context ctx) return ctx.MkEq(GetFlag(Flags.ZF, ln1, ctx), ctx.MkEq(GetReg(reg, ln1, ctx), ZERO)); } - private BoolExpr OverFlowFlag(Rn reg, int lineNumber, Context ctx) + private static BoolExpr OverFlowFlag(Rn reg, int lineNumber, Context ctx) { return SetFlag(Flags.OF, Tv.UNKNOWN, lineNumber, ctx); } - private BoolExpr SignFlag(Rn reg, int lineNumber, Context ctx) + private static BoolExpr SignFlag(Rn reg, int lineNumber, Context ctx) { return SetFlag(Flags.OF, Tv.UNKNOWN, lineNumber, ctx); } @@ -498,7 +498,7 @@ private void AddInstruction_Add(Rn reg1, Rn reg2, int lineNumber) BoolExpr newRegState = MakeRuleRegResult(reg1, this._registers, x, lineNumber, ctx); BoolExpr newFlagState = ctx.MkAnd( ZeroFlag(reg1, lineNumber, ctx), - this.OverFlowFlag(reg1, lineNumber, ctx) + OverFlowFlag(reg1, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newRegState)); this._solver.Assert(ctx.MkImplies(instruction_Switch, newFlagState)); @@ -510,7 +510,7 @@ private void AddInstruction_Add(Rn reg1, Rn reg2, int lineNumber) ctx.MkEq(GetRegKnown(Rn.RCX, ln1, ctx), (reg1 == Rn.RCX) ? GetRegKnown(reg2, ln0, ctx) : GetRegKnown(Rn.RCX, ln0, ctx)), ctx.MkEq(GetRegKnown(Rn.RDX, ln1, ctx), (reg1 == Rn.RDX) ? GetRegKnown(reg2, ln0, ctx) : GetRegKnown(Rn.RDX, ln0, ctx)), ZeroFlag(reg1, lineNumber, ctx), - this.OverFlowFlag(reg1, lineNumber, ctx) + OverFlowFlag(reg1, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newState)); // this._solver.Assert(ctx.MkImplies(instruction_Switch, IsKnownTest(reg1, ln0, ctx))); @@ -533,7 +533,7 @@ private void AddInstruction_Sub(Rn reg1, Rn reg2, int lineNumber) BoolExpr newRegState = MakeRuleRegResult(reg1, this._registers, x, lineNumber, ctx); BoolExpr newFlagState = ctx.MkAnd( ZeroFlag(reg1, lineNumber, ctx), - this.OverFlowFlag(reg1, lineNumber, ctx) + OverFlowFlag(reg1, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newRegState)); this._solver.Assert(ctx.MkImplies(instruction_Switch, newFlagState)); @@ -545,7 +545,7 @@ private void AddInstruction_Sub(Rn reg1, Rn reg2, int lineNumber) ctx.MkEq(GetRegKnown(Rn.RCX, ln1, ctx), (reg1 == Rn.RCX) ? GetRegKnown(reg2, ln0, ctx) : GetRegKnown(Rn.RCX, ln0, ctx)), ctx.MkEq(GetRegKnown(Rn.RDX, ln1, ctx), (reg1 == Rn.RDX) ? GetRegKnown(reg2, ln0, ctx) : GetRegKnown(Rn.RDX, ln0, ctx)), ZeroFlag(reg1, lineNumber, ctx), - this.OverFlowFlag(reg1, lineNumber, ctx) + OverFlowFlag(reg1, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newState)); //this._solver.Assert(ctx.MkImplies(instruction_Switch, IsKnownTest(reg1, ln0, ctx))); @@ -599,8 +599,8 @@ private void AddInstruction_Xor(Rn reg1, Rn reg2, int lineNumber) SetFlag(Flags.AF, Tv.UNDEFINED, lineNumber, ctx), ZeroFlag(reg1, lineNumber, ctx), - this.SignFlag(reg1, lineNumber, ctx), - this.OverFlowFlag(reg1, lineNumber, ctx) + SignFlag(reg1, lineNumber, ctx), + OverFlowFlag(reg1, lineNumber, ctx) ); // this._solver.Assert(ctx.MkImplies(instruction_Switch, newFlagState)); this._solver.Assert(ctx.MkImplies(instruction_Switch, newRegState)); @@ -612,7 +612,7 @@ private void AddInstruction_Xor(Rn reg1, Rn reg2, int lineNumber) ctx.MkEq(GetRegKnown(Rn.RCX, ln1, ctx), (reg1 == Rn.RCX) ? GetRegKnown(reg2, ln0, ctx) : GetRegKnown(Rn.RCX, ln0, ctx)), ctx.MkEq(GetRegKnown(Rn.RDX, ln1, ctx), (reg1 == Rn.RDX) ? GetRegKnown(reg2, ln0, ctx) : GetRegKnown(Rn.RDX, ln0, ctx)), ZeroFlag(reg1, lineNumber, ctx), - this.OverFlowFlag(reg1, lineNumber, ctx) + OverFlowFlag(reg1, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newState)); //this._solver.Assert(ctx.MkImplies(instruction_Switch, IsKnownTest(reg1, ln0, ctx))); @@ -656,7 +656,7 @@ private void AddInstruction_Inc(Rn reg, int lineNumber) BoolExpr newRegState = MakeRuleRegResult(reg, this._registers, x, lineNumber, ctx); BoolExpr newFlagState = ctx.MkAnd( ZeroFlag(reg, lineNumber, ctx), - this.OverFlowFlag(reg, lineNumber, ctx) + OverFlowFlag(reg, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newRegState)); //this._solver.Assert(ctx.MkImplies(instruction_Switch, newFlagState)); @@ -669,7 +669,7 @@ private void AddInstruction_Inc(Rn reg, int lineNumber) ctx.MkEq(GetRegKnown(Rn.RDX, ln1, ctx), GetRegKnown(Rn.RDX, ln0, ctx)), ZeroFlag(reg, lineNumber, ctx), - this.OverFlowFlag(reg, lineNumber, ctx) + OverFlowFlag(reg, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newState)); //this._solver.Assert(ctx.MkImplies(instruction_Switch, IsKnownTest(reg, ln1, ctx))); @@ -695,7 +695,7 @@ private void AddInstruction_Dec(Rn reg, int lineNumber) BoolExpr newFlagState = ctx.MkAnd( ZeroFlag(reg, lineNumber, ctx), - this.OverFlowFlag(reg, lineNumber, ctx) + OverFlowFlag(reg, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newFlagState)); this._solver.Assert(ctx.MkImplies(instruction_Switch, newRegState)); @@ -708,7 +708,7 @@ private void AddInstruction_Dec(Rn reg, int lineNumber) ctx.MkEq(GetRegKnown(Rn.RDX, ln1, ctx), GetRegKnown(Rn.RDX, ln0, ctx)), ZeroFlag(reg, lineNumber, ctx), - this.OverFlowFlag(reg, lineNumber, ctx) + OverFlowFlag(reg, lineNumber, ctx) ); this._solver.Assert(ctx.MkImplies(instruction_Switch, newState)); //this._solver.Assert(ctx.MkImplies(instruction_Switch, IsKnownTest(reg, ln1, ctx))); @@ -750,7 +750,7 @@ private bool IsGrounded(BitVecExpr value, Solver solver, Context ctx) throw new NotImplementedException(); } - private bool Contains(FuncDecl f, IEnumerable e) + private static bool Contains(FuncDecl f, IEnumerable e) { foreach (FuncDecl f2 in e) { @@ -804,7 +804,7 @@ private static BitVecExpr GetRegKnown(Rn reg, int lineNumber, Context ctx) { FuncDecl constantFuncDecl = this._constants[constant].FuncDecl; string constantValue; - if (this.Contains(constantFuncDecl, model.ConstDecls)) + if (Contains(constantFuncDecl, model.ConstDecls)) { constantValue = model.ConstInterp(this._constants[constant].FuncDecl).ToString(); } @@ -823,8 +823,8 @@ private static BitVecExpr GetRegKnown(Rn reg, int lineNumber, Context ctx) } } - StringBuilder sb = new StringBuilder(); - StringBuilder sb2 = new StringBuilder(); + StringBuilder sb = new(); + StringBuilder sb2 = new(); foreach (string s in program) sb.AppendLine(s); foreach (string s in program2) sb2.AppendLine(s); return (sb.ToString(), sb2.ToString()); @@ -838,22 +838,22 @@ private string ToString(Model model) if (true) { - program.Add(funcDecl.Name + " = " + this.ToString(value)); + program.Add(funcDecl.Name + " = " + ToString(value)); } else { if (value.IsBool && value.IsTrue) { - program.Add(funcDecl.Name + " = " + this.ToString(value)); + program.Add(funcDecl.Name + " = " + ToString(value)); } else { - program.Add(funcDecl.Name + " = " + this.ToString(value)); + program.Add(funcDecl.Name + " = " + ToString(value)); } } } - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); sb.AppendLine("\nModel:"); foreach (string s in program) { @@ -878,7 +878,7 @@ private string ToString_Constants(Model model) program.Add(regValue.FuncDecl.Name + " = " + ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(regValue, 64, this._solver, this._ctx))); } } - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); sb.AppendLine("Constants:"); foreach (string s in program) { @@ -887,7 +887,7 @@ private string ToString_Constants(Model model) return sb.ToString(); } - private string ToString(Expr expr) + private static string ToString(Expr expr) { try { @@ -908,9 +908,9 @@ private string ToString(Expr expr) } - private string ToString(Solver solver) + private static string ToString(Solver solver) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); sb.AppendLine("solver:"); foreach (BoolExpr e in solver.Assertions) { @@ -920,7 +920,7 @@ private string ToString(Solver solver) } private string Solver2Asm(Solver solver, Context ctx) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); sb.AppendLine("\nAsm:"); for (int lineNumber = 1; lineNumber <= this._nLines; ++lineNumber) { diff --git a/VS/CSHARP/asm-sim-lib/Runner.cs b/VS/CSHARP/asm-sim-lib/Runner.cs index 137260a9..39beba2e 100644 --- a/VS/CSHARP/asm-sim-lib/Runner.cs +++ b/VS/CSHARP/asm-sim-lib/Runner.cs @@ -37,7 +37,7 @@ public static DynamicFlow Construct_DynamicFlow_Backward(StaticFlow sFlow, Tools public static DynamicFlow Construct_DynamicFlow_Backward(StaticFlow sFlow, int startLine, int nSteps, Tools tools) { - DynamicFlow dFlow = new DynamicFlow(tools); + DynamicFlow dFlow = new(tools); dFlow.Reset(sFlow, false); return dFlow; } @@ -50,7 +50,7 @@ public static DynamicFlow Construct_DynamicFlow_Forward(StaticFlow sFlow, Tools public static DynamicFlow Construct_DynamicFlow_Forward(StaticFlow sFlow, int startLine, int nSteps, Tools tools) { - DynamicFlow dFlow = new DynamicFlow(tools); + DynamicFlow dFlow = new(tools); dFlow.Reset(sFlow, true); return dFlow; } @@ -81,7 +81,7 @@ public static State SimpleStep_Forward(string line, State state) return null; } opcodeBase.Execute(); - State stateOut = new State(state); + State stateOut = new(state); stateOut.Update_Forward(opcodeBase.Updates.regular); stateOut.Frozen = true; @@ -128,7 +128,7 @@ public static State SimpleStep_Backward(string line, State state) } opcodeBase.Execute(); - State stateOut = new State(state); + State stateOut = new(state); stateOut.Update_Backward(opcodeBase.Updates.regular, prevKey); opcodeBase.Updates.regular?.Dispose(); @@ -198,21 +198,22 @@ public static (State? regular, State? branch) Step_Forward(string line, State st } } - public static (StateUpdate regular, StateUpdate branch) Execute( + public static (StateUpdate? regular, StateUpdate? branch) Execute( StaticFlow sFlow, int lineNumber, (string prevKey, string nextKey, string nextKeyBranch) keys, Tools tools) { Contract.Requires(sFlow != null); + Contract.Assume(sFlow != null); try { - (Mnemonic mnemonic, string[] args) content = sFlow.Get_Line(lineNumber); - using OpcodeBase opcodeBase = InstantiateOpcode(content.mnemonic, content.args, keys, tools); + (Mnemonic mnemonic, string[] args) = sFlow.Get_Line(lineNumber); + using OpcodeBase opcodeBase = InstantiateOpcode(mnemonic, args, keys, tools); if ((opcodeBase == null) || opcodeBase.IsHalted) { - StateUpdate resetState = new StateUpdate(keys.prevKey, keys.nextKey, tools) + StateUpdate resetState = new(keys.prevKey, keys.nextKey, tools) { Reset = true, }; @@ -228,7 +229,7 @@ public static (State? regular, State? branch) Step_Forward(string line, State st } } - public static OpcodeBase InstantiateOpcode( + public static OpcodeBase? InstantiateOpcode( Mnemonic mnemonic, string[] args, (string prevKey, string nextKey, string nextKeyBranch) keys, diff --git a/VS/CSHARP/asm-sim-lib/State.cs b/VS/CSHARP/asm-sim-lib/State.cs index 6c7fdfe8..2edf7500 100644 --- a/VS/CSHARP/asm-sim-lib/State.cs +++ b/VS/CSHARP/asm-sim-lib/State.cs @@ -64,7 +64,7 @@ public class State : IDisposable private readonly IDictionary cached_Reg_Values_; private readonly IDictionary cached_Flag_Values_; - private readonly object ctxLock_ = new object(); + private readonly object ctxLock_ = new(); private BranchInfoStore branchInfoStore_; @@ -168,7 +168,7 @@ public State(State state1, State state2, bool merge) } else { - this.DiffConstructor(state1, state2); + DiffConstructor(state1, state2); } } @@ -266,21 +266,19 @@ private void MergeConstructor(State state1, State state2) string head1 = state1.HeadKey; string head2 = state2.HeadKey; - using (StateUpdate stateUpdateForward = new StateUpdate("!ERROR_1", this.HeadKey, this.Tools)) + using StateUpdate stateUpdateForward = new("!ERROR_1", this.HeadKey, this.Tools); + BoolExpr dummyBranchCondttion = ctx.MkBoolConst("DymmyBC" + this.HeadKey); + foreach (Rn reg in this.Tools.StateConfig.GetRegOn()) { - BoolExpr dummyBranchCondttion = ctx.MkBoolConst("DymmyBC" + this.HeadKey); - foreach (Rn reg in this.Tools.StateConfig.GetRegOn()) - { - stateUpdateForward.Set(reg, ctx.MkITE(dummyBranchCondttion, Tools.Create_Key(reg, head1, ctx), Tools.Create_Key(reg, head2, ctx)) as BitVecExpr); - } - foreach (Flags flag in this.Tools.StateConfig.GetFlagOn()) - { - stateUpdateForward.Set(flag, ctx.MkITE(dummyBranchCondttion, Tools.Create_Key(flag, head1, ctx), Tools.Create_Key(flag, head2, ctx)) as BoolExpr); - } - stateUpdateForward.Set_Mem(ctx.MkITE(dummyBranchCondttion, Tools.Create_Mem_Key(head1, ctx), Tools.Create_Mem_Key(head2, ctx)) as ArrayExpr); - - this.Update_Forward(stateUpdateForward); + stateUpdateForward.Set(reg, ctx.MkITE(dummyBranchCondttion, Tools.Create_Key(reg, head1, ctx), Tools.Create_Key(reg, head2, ctx)) as BitVecExpr); } + foreach (Flags flag in this.Tools.StateConfig.GetFlagOn()) + { + stateUpdateForward.Set(flag, ctx.MkITE(dummyBranchCondttion, Tools.Create_Key(flag, head1, ctx), Tools.Create_Key(flag, head2, ctx)) as BoolExpr); + } + stateUpdateForward.Set_Mem(ctx.MkITE(dummyBranchCondttion, Tools.Create_Mem_Key(head1, ctx), Tools.Create_Mem_Key(head2, ctx)) as ArrayExpr); + + this.Update_Forward(stateUpdateForward); } if (state1.TailKey == state2.TailKey) { @@ -295,7 +293,7 @@ private void MergeConstructor(State state1, State state2) } } - private void DiffConstructor(State state1, State state2) + private static void DiffConstructor(State state1, State state2) { //TODO } @@ -313,7 +311,11 @@ public void Assert(BoolExpr expr, bool undef, bool translate) if (translate) { - BoolExpr t = expr.Translate(this.ctx_) as BoolExpr; + BoolExpr? t = expr.Translate(this.ctx_) as BoolExpr; + if (t == null) + { + return; + } if (undef) { this.Solver_U.Assert(t); @@ -481,19 +483,17 @@ public bool Is_Redundant(Flags flagName, string key1, string key2) popNeeded = true; } - using (Expr e1 = Tools.Create_Key(flagName, key1, this.ctx_)) - using (Expr e2 = Tools.Create_Key(flagName, key2, this.ctx_)) - using (BoolExpr e = this.ctx_.MkEq(e1, e2)) - { - Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this.ctx_); + using Expr e1 = Tools.Create_Key(flagName, key1, this.ctx_); + using Expr e2 = Tools.Create_Key(flagName, key2, this.ctx_); + using BoolExpr e = this.ctx_.MkEq(e1, e2); + Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this.ctx_); - if (popNeeded) - { - this.Solver.Pop(); - this.Solver_U.Pop(); - } - return result == Tv.ONE; + if (popNeeded) + { + this.Solver.Pop(); + this.Solver_U.Pop(); } + return result == Tv.ONE; } } @@ -512,19 +512,17 @@ public bool Is_Redundant(Rn regName, string key1, string key2) popNeeded = true; } - using (Expr e1 = Tools.Create_Key(regName, key1, this.ctx_)) - using (Expr e2 = Tools.Create_Key(regName, key2, this.ctx_)) - using (BoolExpr e = this.ctx_.MkEq(e1, e2)) - { - Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this.ctx_); + using Expr e1 = Tools.Create_Key(regName, key1, this.ctx_); + using Expr e2 = Tools.Create_Key(regName, key2, this.ctx_); + using BoolExpr e = this.ctx_.MkEq(e1, e2); + Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this.ctx_); - if (popNeeded) - { - this.Solver.Pop(); - this.Solver_U.Pop(); - } - return result == Tv.ONE; + if (popNeeded) + { + this.Solver.Pop(); + this.Solver_U.Pop(); } + return result == Tv.ONE; } } @@ -543,18 +541,16 @@ public Tv Is_Redundant_Mem(string key1, string key2) popNeeded = true; } - using (Expr e1 = Tools.Create_Mem_Key(key1, this.ctx_)) - using (Expr e2 = Tools.Create_Mem_Key(key2, this.ctx_)) - using (BoolExpr e = this.ctx_.MkEq(e1, e2)) + using Expr e1 = Tools.Create_Mem_Key(key1, this.ctx_); + using Expr e2 = Tools.Create_Mem_Key(key2, this.ctx_); + using BoolExpr e = this.ctx_.MkEq(e1, e2); + Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this.ctx_, true); + if (popNeeded) { - Tv result = ToolsZ3.GetTv(e, e, this.Solver, this.Solver_U, this.ctx_, true); - if (popNeeded) - { - this.Solver.Pop(); - this.Solver_U.Pop(); - } - return result; + this.Solver.Pop(); + this.Solver_U.Pop(); } + return result; } } @@ -587,21 +583,19 @@ public Tv GetTv(Flags flagName) popNeeded = true; } - using (BoolExpr flagExpr = this.Create(flagName)) - { - Tv result = ToolsZ3.GetTv(flagExpr, flagExpr, this.Solver, this.Solver_U, this.ctx_); + using BoolExpr flagExpr = this.Create(flagName); + Tv result = ToolsZ3.GetTv(flagExpr, flagExpr, this.Solver, this.Solver_U, this.ctx_); - if (popNeeded) - { - this.Solver.Pop(); - this.Solver_U.Pop(); - } - if (this.Frozen) - { - this.cached_Flag_Values_[flagName] = result; - } - return result; + if (popNeeded) + { + this.Solver.Pop(); + this.Solver_U.Pop(); + } + if (this.Frozen) + { + this.cached_Flag_Values_[flagName] = result; } + return result; } } @@ -637,31 +631,29 @@ public Tv[] GetTvArray(Rn regName) popNeeded = true; } - using (BitVecExpr regExpr = this.Create(regName)) - { - Tv[] result = ToolsZ3.GetTvArray(regExpr, RegisterTools.NBits(regName), this.Solver, this.Solver_U, this.ctx_); + using BitVecExpr regExpr = this.Create(regName); + Tv[] result = ToolsZ3.GetTvArray(regExpr, RegisterTools.NBits(regName), this.Solver, this.Solver_U, this.ctx_); - if (popNeeded) - { - this.Solver.Pop(); - this.Solver_U.Pop(); - } + if (popNeeded) + { + this.Solver.Pop(); + this.Solver_U.Pop(); + } - if (this.Frozen) + if (this.Frozen) + { + if (ADD_COMPUTED_VALUES && (RegisterTools.NBits(regName) == 64)) { - if (ADD_COMPUTED_VALUES && (RegisterTools.NBits(regName) == 64)) + ulong? value2 = ToolsZ3.ToUlong(result); + if (value2 != null) { - ulong? value2 = ToolsZ3.ToUlong(result); - if (value2 != null) - { - this.Solver.Assert(this.Ctx.MkEq(regExpr, this.Ctx.MkBV(value2.Value, 64))); - this.solver_Dirty = true; - } + this.Solver.Assert(this.Ctx.MkEq(regExpr, this.Ctx.MkBV(value2.Value, 64))); + this.solver_Dirty = true; } - this.cached_Reg_Values_[regName] = result; } - return result; + this.cached_Reg_Values_[regName] = result; } + return result; } catch (Exception e) { @@ -689,17 +681,15 @@ public Tv[] GetTvArrayMem(BitVecExpr address, int nBytes, bool addBranchInfo = t popNeeded = true; } - using (BitVecExpr valueExpr = this.Create_Mem(address, nBytes)) - { - Tv[] result = ToolsZ3.GetTvArray(valueExpr, nBytes << 3, this.Solver, this.Solver_U, this.ctx_); + using BitVecExpr valueExpr = this.Create_Mem(address, nBytes); + Tv[] result = ToolsZ3.GetTvArray(valueExpr, nBytes << 3, this.Solver, this.Solver_U, this.ctx_); - if (popNeeded) - { - this.Solver.Pop(); - this.Solver_U.Pop(); - } - return result; + if (popNeeded) + { + this.Solver.Pop(); + this.Solver_U.Pop(); } + return result; } public BitVecExpr Create(Rn regName) @@ -822,7 +812,7 @@ public override string ToString() public string ToString(string identStr) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); sb.AppendLine(this.ToStringConstraints(identStr)); @@ -843,7 +833,7 @@ public string ToString(string identStr) public string ToStringFlags(string identStr) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); foreach (Flags flag in new Flags[] { Flags.CF, Flags.ZF, Flags.PF, Flags.OF, Flags.SF, Flags.AF, Flags.DF }) { char c = ' '; @@ -859,7 +849,7 @@ public string ToStringFlags(string identStr) public string ToStringRegs(string identStr) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); foreach (Rn reg in this.Tools.StateConfig.GetRegOn()) { Tv[] regContent = this.GetTvArray(reg); @@ -875,7 +865,7 @@ public string ToStringRegs(string identStr) public string ToStringSIMD(string identStr) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); // foreach (Rn reg in this.Tools.StateConfig.GetRegOn()) { Rn reg = Rn.XMM1; @@ -892,7 +882,7 @@ public string ToStringSIMD(string identStr) public string ToStringConstraints(string identStr) { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); if (this.Solver.NumAssertions > 0) { sb.AppendLine(identStr + "Current Value constraints:"); @@ -916,27 +906,21 @@ public string ToStringConstraints(string identStr) #region Misc public void Remove_History() { - ISet keep = new HashSet(); + HashSet keep = new(); foreach (Flags v in this.tools_.StateConfig.GetFlagOn()) { - using (BoolExpr expr = this.Create(v)) - { - keep.Add(expr.ToString()); - } + using BoolExpr expr = this.Create(v); + keep.Add(expr.ToString()); } foreach (Rn v in this.tools_.StateConfig.GetRegOn()) { - using (BitVecExpr expr = this.Create(v)) - { - keep.Add(expr.ToString()); - } + using BitVecExpr expr = this.Create(v); + keep.Add(expr.ToString()); } if (this.tools_.StateConfig.Mem) { - using (ArrayExpr expr = Tools.Create_Mem_Key(this.HeadKey, this.ctx_)) - { - keep.Add(expr.ToString()); - } + using ArrayExpr expr = Tools.Create_Mem_Key(this.HeadKey, this.ctx_); + keep.Add(expr.ToString()); } this.Compress(keep); } @@ -946,9 +930,9 @@ public void Compress(string keep) this.Compress(new HashSet() { keep }); } - public void Compress(ISet keep) + public void Compress(HashSet keep) { - ISet used = new HashSet(keep); + HashSet used = new(keep); BoolExpr[] s = this.Solver.Assertions; int nAssertions = s.Length; bool[] added = new bool[nAssertions]; @@ -989,8 +973,8 @@ public void Compress(ISet keep) public void UpdateConstName(string postfix) { - this.HeadKey = this.HeadKey + postfix; - this.TailKey = this.TailKey + postfix; + this.HeadKey += postfix; + this.TailKey += postfix; lock (this.ctxLock_) { { @@ -1041,11 +1025,9 @@ public Tv IsConsistent public Tv EqualValues(Rn reg1, Rn reg2) { - using (BitVecExpr expr1 = this.Create(reg1)) - using (BitVecExpr expr2 = this.Create(reg2)) - { - return this.EqualValues(expr1, expr2); - } + using BitVecExpr expr1 = this.Create(reg1); + using BitVecExpr expr2 = this.Create(reg2); + return this.EqualValues(expr1, expr2); } public Tv EqualValues(Expr value1, Expr value2) diff --git a/VS/CSHARP/asm-sim-lib/StateUpdate.cs b/VS/CSHARP/asm-sim-lib/StateUpdate.cs index 642f32f0..0e073387 100644 --- a/VS/CSHARP/asm-sim-lib/StateUpdate.cs +++ b/VS/CSHARP/asm-sim-lib/StateUpdate.cs @@ -9,24 +9,27 @@ // copies of the Software, and to permit persons to whom the Software is // furnished to do so, subject to the following conditions: -namespace AsmSim -{ - // The above copyright notice and this permission notice shall be included in all - // copies or substantial portions of the Software. +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. - // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - // OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - // SOFTWARE. +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. +namespace AsmSim +{ using System; using System.Collections.Generic; + using System.Diagnostics.CodeAnalysis; using System.Diagnostics.Contracts; using System.Text; using AsmTools; + + using Microsoft.CodeAnalysis.CSharp.Syntax; using Microsoft.Z3; public class StateUpdate : IDisposable @@ -36,8 +39,8 @@ public class StateUpdate : IDisposable private readonly Context ctx_; private string nextKey_; private readonly string prevKey_Regular_; - private readonly string prevKey_Branch_; - private readonly BoolExpr branch_Condition_; + private readonly string? prevKey_Branch_; + private readonly BoolExpr? branch_Condition_; public bool Empty { get; private set; } @@ -46,7 +49,7 @@ public class StateUpdate : IDisposable private BranchInfo branchInfo_; - private readonly object ctxLock_ = new object(); + private readonly object ctxLock_ = new(); #endregion @@ -126,6 +129,7 @@ public class StateUpdate : IDisposable public StateUpdate(string prevKey, string nextKey, Tools tools) { Contract.Requires(tools != null); + Contract.Assume(tools != null); this.branch_Condition_ = null; this.prevKey_Regular_ = prevKey; @@ -143,6 +147,8 @@ public StateUpdate(BoolExpr branchCondition, string prevKey_Regular, string prev { Contract.Requires(tools != null); Contract.Requires(branchCondition != null); + Contract.Assume(tools != null); + Contract.Assume(branchCondition != null); this.ctx_ = new Context(tools.ContextSettings); // housekeeping in Dispose(); this.branch_Condition_ = branchCondition.Translate(this.ctx_) as BoolExpr; @@ -158,6 +164,7 @@ public StateUpdate(BoolExpr branchCondition, string prevKey_Regular, string prev public void Update(State state) { Contract.Requires(state != null); + Contract.Assume(state != null); lock (this.ctxLock_) { @@ -358,10 +365,17 @@ public string NextKey set { + if (value == null) + { + return; + } + if (this.nextKey_ == null) { this.nextKey_ = value; } + + else if (this.nextKey_ != value) { Context ctx = this.ctx_; @@ -625,7 +639,6 @@ public void Set(Rn reg, Tv value) case Tv.UNDEFINED: case Tv.ONE: throw new Exception("Not implemented yet"); - break; default: break; } } @@ -639,12 +652,16 @@ public void Set(Rn reg, BitVecExpr value, BitVecExpr undef) { Contract.Requires(value != null); Contract.Requires(undef != null); + Contract.Assume(value != null); + this.Empty = false; lock (this.ctxLock_) { Context ctx = this.ctx_; + Contract.Assume(ctx != null); + value = value.Translate(ctx) as BitVecExpr; undef = undef.Translate(ctx) as BitVecExpr; @@ -715,8 +732,8 @@ public void Set(Rn reg, BitVecExpr value, BitVecExpr undef) BitVecExpr prevKey = ctx.MkBVConst(Tools.Reg_Name(reg, this.prevKey_Regular_), max); (uint high, uint low) = Tools.SIMD_Extract_Range(reg); - BitVecExpr top = null; - BitVecExpr bottom = null; + BitVecExpr? top = null; + BitVecExpr? bottom = null; if (high < (max - 1)) { top = ctx.MkExtract(max - 1, high + 1, prevKey); @@ -727,11 +744,11 @@ public void Set(Rn reg, BitVecExpr value, BitVecExpr undef) bottom = ctx.MkExtract(low - 1, 0, prevKey); } - Console.WriteLine(top.SortSize + "+" + value.SortSize + "+" + bottom.SortSize + "=" + prevKey.SortSize); + Console.WriteLine(top!.SortSize + "+" + value!.SortSize + "+" + bottom!.SortSize + "=" + prevKey.SortSize); - BitVecExpr newValue = (top == null) ? value : ctx.MkConcat(top, value) as BitVecExpr; + BitVecExpr newValue = (top == null) ? value : ctx.MkConcat(top, value); newValue = (bottom == null) ? newValue : ctx.MkConcat(newValue, bottom); - BitVecExpr newUndef = (top == null) ? value : ctx.MkConcat(top, value) as BitVecExpr; + BitVecExpr newUndef = (top == null) ? value : ctx.MkConcat(top, value); newUndef = (bottom == null) ? newUndef : ctx.MkConcat(newUndef, bottom); BitVecExpr nextKey = ctx.MkBVConst(Tools.Reg_Name(reg, this.NextKey), 512 * 32); @@ -976,12 +993,12 @@ public void Set_Mem(BitVecExpr address, BitVecExpr value, BitVecExpr undef) } } - public void Set_Mem(ArrayExpr memContent) + public void Set_Mem([DisallowNull] ArrayExpr memContent) { - Contract.Requires(memContent != null); + - this.Empty = false; + this.Empty = false; if (this.mem_Full_ != null) { Console.WriteLine("WARNING: StateUpdate:SetMem: multiple memory updates are not allowed"); @@ -1006,6 +1023,7 @@ public void Set(Operand operand, BitVecExpr value) public void Set(Operand operand, BitVecExpr value, BitVecExpr undef) { Contract.Requires(operand != null); + Contract.Assume(operand != null); if (operand.IsReg) { @@ -1029,7 +1047,7 @@ public void Set(Operand operand, BitVecExpr value, BitVecExpr undef) public string ToString2() { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); foreach (Flags flag in this.tools_.StateConfig.GetFlagOn()) { BoolExpr b = this.Get_Raw_Private(flag, true); @@ -1055,7 +1073,7 @@ public string ToString2() public override string ToString() { - StringBuilder sb = new StringBuilder("StateUpdate: PrevKey=" + this.prevKey_Regular_ + "; NextKey=" + this.NextKey + " "); + StringBuilder sb = new("StateUpdate: PrevKey=" + this.prevKey_Regular_ + "; NextKey=" + this.NextKey + " "); if (this.Empty) { sb.AppendLine("Empty UpdateState"); diff --git a/VS/CSHARP/asm-sim-lib/StaticFlow.cs b/VS/CSHARP/asm-sim-lib/StaticFlow.cs index 349bd7a5..9e87434c 100644 --- a/VS/CSHARP/asm-sim-lib/StaticFlow.cs +++ b/VS/CSHARP/asm-sim-lib/StaticFlow.cs @@ -73,27 +73,25 @@ public StateConfig Create_StateConfig() for (int lineNumber = lineNumberBegin; lineNumber <= lineNumberEnd; lineNumber++) { (Mnemonic mnemonic, string[] args) content = this.Get_Line(lineNumber); - using (Mnemonics.OpcodeBase opcodeBase = Runner.InstantiateOpcode(content.mnemonic, content.args, dummyKeys, this.tools_)) + using Mnemonics.OpcodeBase opcodeBase = Runner.InstantiateOpcode(content.mnemonic, content.args, dummyKeys, this.tools_); + if (opcodeBase != null) { - if (opcodeBase != null) + flags |= opcodeBase.FlagsReadStatic | opcodeBase.FlagsWriteStatic; + foreach (Rn r in opcodeBase.RegsReadStatic) { - flags |= opcodeBase.FlagsReadStatic | opcodeBase.FlagsWriteStatic; - foreach (Rn r in opcodeBase.RegsReadStatic) - { - regs.Add(RegisterTools.Get64BitsRegister(r)); - } - - foreach (Rn r in opcodeBase.RegsWriteStatic) - { - regs.Add(RegisterTools.Get64BitsRegister(r)); - } + regs.Add(RegisterTools.Get64BitsRegister(r)); + } - mem |= opcodeBase.MemWriteStatic || opcodeBase.MemReadStatic; + foreach (Rn r in opcodeBase.RegsWriteStatic) + { + regs.Add(RegisterTools.Get64BitsRegister(r)); } + + mem |= opcodeBase.MemWriteStatic || opcodeBase.MemReadStatic; } } - StateConfig config = new StateConfig(); + StateConfig config = new(); config.Set_All_Off(); config.Set_Flags_On(flags); foreach (Rn reg in regs) @@ -123,13 +121,13 @@ public string Get_Key(int lineNumber) { string key1 = this.Get_Key(lineNumber.lineNumber1); string key2 = this.Get_Key(lineNumber.lineNumber2); - return (key1: key1, key2: key2); + return (key1, key2); } else { string key1 = Tools.CreateKey(this.tools_.Rand); string key2 = key1 + "B"; - return (key1: key1, key2: key2); + return (key1, key2); } } @@ -162,11 +160,11 @@ public bool HasLine(int lineNumber) if (lineNumber >= this.Current.Count) { Console.WriteLine("WARING: CFlow:geLine: lineNumber " + lineNumber + " does not exist"); - return (Mnemonic.NONE, null); + return (Mnemonic.NONE, Array.Empty()); } - (string label, Mnemonic mnemonic, string[] args) v = this.Current[lineNumber]; + (string label, Mnemonic mnemonic, string[] args) = this.Current[lineNumber]; - return (v.mnemonic, v.args); + return (mnemonic, args); } public string Get_Line_Str(int lineNumber) @@ -221,7 +219,7 @@ public IEnumerable<(int lineNumber, bool isBranch)> Get_Prev_LineNumber(int line regular = v.Target; } } - return (regular: regular, branch: branch); + return (regular, branch); } /// A LoopBranchPoint is a BranchPoint that choices between leaving the loop or staying in the loop. @@ -325,7 +323,7 @@ public bool Update(string programStr, bool removeEmptyLines = true) this.use_Parsed_Code_A_ = !this.use_Parsed_Code_A_; #region Parse to find all labels - IDictionary labels = this.GetLabels(programStr); + IDictionary labels = GetLabels(programStr); // replace all labels by annotated label foreach (KeyValuePair entry in labels) @@ -354,10 +352,10 @@ public bool Update(string programStr, bool removeEmptyLines = true) for (int lineNumber = 0; lineNumber < lines.Length; ++lineNumber) { (KeywordID[] _, string label, Mnemonic mnemonic, string[] args, string remark) line = AsmSourceTools.ParseLine(lines[lineNumber], -1, -1); - this.EvalArgs(ref line.args); + EvalArgs(ref line.args); current.Add((line.label, line.mnemonic, line.args)); - (int jumpTo1, int jumpTo2) = this.Static_Jump(line.mnemonic, line.args, lineNumber); + (int jumpTo1, int jumpTo2) = Static_Jump(line.mnemonic, line.args, lineNumber); if (jumpTo1 != -1) { this.Add_Edge(lineNumber, jumpTo1, false); @@ -409,7 +407,7 @@ public bool Update(string programStr, bool removeEmptyLines = true) #endregion } - private void EvalArgs(ref string[] args) + private static void EvalArgs(ref string[] args) { for (int i = 0; i < args.Length; ++i) { @@ -443,7 +441,7 @@ private void Compress() int next = outEdge.Target; //Remove this empty line - List> inEdges = new List>(this.graph_.InEdges(lineNumber)); + List> inEdges = new(this.graph_.InEdges(lineNumber)); foreach (TaggedEdge e in inEdges) { this.graph_.AddEdge(new TaggedEdge(e.Source, next, e.Tag)); @@ -487,7 +485,7 @@ public static string ToString((string label, Mnemonic mnemonic, string[] args) t public override string ToString() { - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); for (int i = 0; i < this.Current.Count; ++i) { @@ -549,7 +547,7 @@ private void Add_Edge(int jumpFrom, int jumpTo, bool isBranch) this.graph_.AddEdge(new TaggedEdge(jumpFrom, jumpTo, isBranch)); } - private (int regularLineNumber, int branchLineNumber) Static_Jump(Mnemonic mnemonic, string[] args, int lineNumber) + private static (int regularLineNumber, int branchLineNumber) Static_Jump(Mnemonic mnemonic, string[] args, int lineNumber) { int jumpTo1 = -1; int jumpTo2 = -1; @@ -625,7 +623,7 @@ private void Add_Edge(int jumpFrom, int jumpTo, bool isBranch) } /// Get all labels with the line number on which it is defined - private IDictionary GetLabels(string text) + private static IDictionary GetLabels(string text) { Contract.Requires(text != null); diff --git a/VS/CSHARP/asm-sim-lib/Tools.cs b/VS/CSHARP/asm-sim-lib/Tools.cs index 08772cb6..994d97a9 100644 --- a/VS/CSHARP/asm-sim-lib/Tools.cs +++ b/VS/CSHARP/asm-sim-lib/Tools.cs @@ -393,18 +393,16 @@ public static BitVecExpr Create_Value_From_Mem(BitVecExpr address, int nBytes, s Contract.Requires(ctx != null); Contract.Requires(nBytes > 0, "Number of bytes has to larger than zero. nBytes=" + nBytes); - using (ArrayExpr mem = Create_Mem_Key(key, ctx)) - { - BitVecExpr result = ctx.MkSelect(mem, address) as BitVecExpr; + using ArrayExpr mem = Create_Mem_Key(key, ctx); + BitVecExpr result = ctx.MkSelect(mem, address) as BitVecExpr; - for (uint i = 1; i < nBytes; ++i) - { - BitVecExpr result2 = ctx.MkSelect(mem, ctx.MkBVAdd(address, ctx.MkBV(i, 64))) as BitVecExpr; - result = ctx.MkConcat(result2, result); - } - Debug.Assert(result.SortSize == (nBytes * 8)); - return result; + for (uint i = 1; i < nBytes; ++i) + { + BitVecExpr result2 = ctx.MkSelect(mem, ctx.MkBVAdd(address, ctx.MkBV(i, 64))) as BitVecExpr; + result = ctx.MkConcat(result2, result); } + Debug.Assert(result.SortSize == (nBytes * 8)); + return result; } public static ArrayExpr Set_Value_To_Mem(BitVecExpr value, BitVecExpr address, string key, Context ctx) @@ -444,7 +442,7 @@ public static State Collapse(IEnumerable previousStates) { Console.WriteLine("INFO: Tools:Collapse: state1:\n" + result); Console.WriteLine("INFO: Tools:Collapse: state2:\n" + prev); - State result2 = new State(result, prev, true); + State result2 = new(result, prev, true); if (counter > 2) { //TODO HJ 26 okt 2019 investigate dispose diff --git a/VS/CSHARP/asm-sim-lib/ToolsFlags.cs b/VS/CSHARP/asm-sim-lib/ToolsFlags.cs index 9b0521bc..9853b989 100644 --- a/VS/CSHARP/asm-sim-lib/ToolsFlags.cs +++ b/VS/CSHARP/asm-sim-lib/ToolsFlags.cs @@ -109,13 +109,11 @@ private static BoolExpr Create_OF(BitVecExpr a, BitVecExpr b, BitVecExpr result, Contract.Requires(a.SortSize == result.SortSize, "number of bits of a and result should be equal"); Contract.Requires(nBits <= a.SortSize); - using (BitVecExpr signA = Create_SF_BV(a, nBits, ctx)) - using (BitVecExpr signB = Create_SF_BV(b, nBits, ctx)) - using (BitVecExpr signC = Create_SF_BV(result, nBits, ctx)) - using (BitVecExpr oNE = ctx.MkBV(1, 1)) - { - return ctx.MkAnd(ctx.MkEq(signA, signB), ctx.MkEq(ctx.MkBVXOR(signA, signC), oNE)); - } + using BitVecExpr signA = Create_SF_BV(a, nBits, ctx); + using BitVecExpr signB = Create_SF_BV(b, nBits, ctx); + using BitVecExpr signC = Create_SF_BV(result, nBits, ctx); + using BitVecExpr oNE = ctx.MkBV(1, 1); + return ctx.MkAnd(ctx.MkEq(signA, signB), ctx.MkEq(ctx.MkBVXOR(signA, signC), oNE)); } #endregion diff --git a/VS/CSHARP/asm-sim-lib/ToolsZ3.cs b/VS/CSHARP/asm-sim-lib/ToolsZ3.cs index 06cd5686..2a291889 100644 --- a/VS/CSHARP/asm-sim-lib/ToolsZ3.cs +++ b/VS/CSHARP/asm-sim-lib/ToolsZ3.cs @@ -32,7 +32,7 @@ namespace AsmSim public static class ToolsZ3 { - private static readonly object Object_ = new object(); + private static readonly object Object_ = new(); #region Public Methods @@ -121,7 +121,7 @@ public static (BitVecExpr value, BitVecExpr undef) MakeVecExpr(Tv[] tv5, Context Contract.Requires(tv5 != null); Contract.Requires(tv5.Length > 0); - Random random = new Random(); + Random random = new(); BitVecExpr value = null; BitVecExpr undef = null; @@ -154,7 +154,7 @@ public static (BitVecExpr value, BitVecExpr undef) MakeVecExpr(Tv[] tv5, Context value = (value == null) ? next_value : ctx.MkConcat(next_value, value); undef = (undef == null) ? next_undef : ctx.MkConcat(next_undef, undef); } - return (value: value, undef: undef); + return (value, undef); } private static (bool valid, ulong value) IsSimpleAssignment_UNUSED(string name, BoolExpr e) @@ -314,33 +314,23 @@ public static void Consolidate(bool undef, Solver solver, Solver solver_U, Conte //Tactic ta6b = ctx.MkTactic("sat-preprocess"); // does not work: some constrains are lost //Tactic ta7 = ctx.MkTactic("smt"); // does not work: all constraitns are lost - using (Tactic tactic = ctx.AndThen(ta2, ctx.AndThen(ta1, ta5))) + using Tactic tactic = ctx.AndThen(ta2, ctx.AndThen(ta1, ta5)); // using (Tactic tactic = ctx.AndThen(ta2, ta1)) + if (!undef) { - if (!undef) - { - using (Goal goal1 = ctx.MkGoal()) - { - goal1.Assert(solver.Assertions); - using (ApplyResult ar = tactic.Apply(goal1)) - { - solver.Reset(); - solver.Assert(ar.Subgoals[0].Formulas); - } - } - } - else - { - using (Goal goal1 = ctx.MkGoal()) - { - goal1.Assert(solver_U.Assertions); - using (ApplyResult ar = tactic.Apply(goal1)) - { - solver_U.Reset(); - solver_U.Assert(ar.Subgoals[0].Formulas); - } - } - } + using Goal goal1 = ctx.MkGoal(); + goal1.Assert(solver.Assertions); + using ApplyResult ar = tactic.Apply(goal1); + solver.Reset(); + solver.Assert(ar.Subgoals[0].Formulas); + } + else + { + using Goal goal1 = ctx.MkGoal(); + goal1.Assert(solver_U.Assertions); + using ApplyResult ar = tactic.Apply(goal1); + solver_U.Reset(); + solver_U.Assert(ar.Subgoals[0].Formulas); } } } @@ -352,20 +342,16 @@ public static bool Equals(BitVecExpr valueExpr, BitVecExpr undef, Tv[] valueTv, Contract.Requires(ctx != null); Contract.Requires(valueTv != null); - using (BitVecNum bv1_1bit = ctx.MkBV(1, 1)) + using BitVecNum bv1_1bit = ctx.MkBV(1, 1); + for (uint bit = 0; bit < nBits; ++bit) { - for (uint bit = 0; bit < nBits; ++bit) + using BoolExpr b = GetBit(valueExpr, bit, bv1_1bit, ctx); + using BoolExpr b_undef = GetBit(undef, bit, bv1_1bit, ctx); + // this can be done faster + Tv tv = GetTv(b, b_undef, solver, solver_U, ctx); + if (tv != valueTv[bit]) { - using (BoolExpr b = GetBit(valueExpr, bit, bv1_1bit, ctx)) - using (BoolExpr b_undef = GetBit(undef, bit, bv1_1bit, ctx)) - { - // this can be done faster - Tv tv = GetTv(b, b_undef, solver, solver_U, ctx); - if (tv != valueTv[bit]) - { - return false; - } - } + return false; } } return true; @@ -400,7 +386,7 @@ private static void CollectFlags_UNUSED(Expr e, ref Flags flags) } } - /// add the contants from Expression e to the provided set + /// add the constants from Expression e to the provided set private static void CollectConstants_UNUSED(Expr e, ref ISet set) { if (e.IsConst) @@ -433,7 +419,7 @@ public static string ToString(Solver solver, string identStr) { Contract.Requires(solver != null); - StringBuilder sb = new StringBuilder(); + StringBuilder sb = new(); for (int i = 0; i < (int)solver.NumAssertions; ++i) { BoolExpr e = solver.Assertions[i]; @@ -446,7 +432,7 @@ public static string ToString(Solver solver, string identStr) public static string ToStringBin(Tv[] a) { - StringBuilder sb = new StringBuilder("0b"); + StringBuilder sb = new("0b"); if (a == null) { sb.Append("null"); @@ -753,19 +739,17 @@ public static char BitToCharOct(Tv b0, Tv b1, Tv b2) { for (uint bit = 0; bit < nBits; ++bit) { - using (BoolExpr b = GetBit(value, bit, oNE, ctx)) + using BoolExpr b = GetBit(value, bit, oNE, ctx); + switch (GetTv(b, solver, ctx)) { - switch (GetTv(b, solver, ctx)) - { - case Tv.ONE: - results[bit] = Tv.ONE; - break; - case Tv.ZERO: - results[bit] = Tv.ZERO; - break; - default: - return null; - } + case Tv.ONE: + results[bit] = Tv.ONE; + break; + case Tv.ZERO: + results[bit] = Tv.ZERO; + break; + default: + return null; } } } @@ -858,11 +842,9 @@ public static Tv[] GetTvArray(BitVecExpr value, BitVecExpr undef, int nBits, Sol { for (uint bit = 0; bit < nBits; ++bit) { - using (BoolExpr b = GetBit(value, bit, bv1_1bit, ctx)) - using (BoolExpr b_undef = GetBit(undef, bit, bv1_1bit, ctx)) - { - results[bit] = GetTv(b, b_undef, solver, solver_U, ctx); - } + using BoolExpr b = GetBit(value, bit, bv1_1bit, ctx); + using BoolExpr b_undef = GetBit(undef, bit, bv1_1bit, ctx); + results[bit] = GetTv(b, b_undef, solver, solver_U, ctx); } } return results; @@ -882,10 +864,8 @@ public static Tv[] GetTvArray(BitVecExpr value, int nBits, Solver solver, Contex { for (uint bit = 0; bit < nBits; ++bit) { - using (BoolExpr b = GetBit(value, bit, bv1_1bit, ctx)) - { - results[bit] = GetTv(b, solver, ctx); - } + using BoolExpr b = GetBit(value, bit, bv1_1bit, ctx); + results[bit] = GetTv(b, solver, ctx); } } return results; @@ -930,16 +910,14 @@ private static Tv GetTv_Method1(BoolExpr value, BoolExpr undef, Solver solver, S bool tvFalse; { - using (BoolExpr t = ctx.MkNot(value)) + using BoolExpr t = ctx.MkNot(value); + Status status = solver.Check(t); + if (status == Status.UNKNOWN) { - Status status = solver.Check(t); - 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; + //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 @@ -969,16 +947,14 @@ private static Tv GetTv_Method1(BoolExpr value, BoolExpr undef, Solver solver, S bool tvFalseU; { - using (BoolExpr t = ctx.MkNot(undef)) + using BoolExpr t = ctx.MkNot(undef); + Status status = solver_U.Check(t); + if (status == Status.UNKNOWN) { - Status status = solver_U.Check(t); - 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; } + tvFalseU = status == Status.SATISFIABLE; } // if (!tvFalseU) return Tv5.UNKNOWN; @@ -1002,40 +978,36 @@ private static Tv GetTv_Method2(BoolExpr value, BoolExpr undef, Solver solver, S { bool tvTrue; { - using (Solver s = State.MakeSolver(ctx)) + using Solver s = State.MakeSolver(ctx); + s.Assert(solver.Assertions); + s.Assert(value); + Status status = s.Check(); + if (status == Status.UNKNOWN) { - s.Assert(solver.Assertions); - s.Assert(value); - Status status = s.Check(); - if (status == Status.UNKNOWN) - { - //Console.WriteLine("ToolsZ3:getTv5: A: value=" + value + " yields UNKNOWN solver status. Reason: " + solver.ReasonUnknown); - return Tv.UNDETERMINED; - } - tvTrue = status == Status.SATISFIABLE; + //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; { - using (Solver s = State.MakeSolver(ctx)) + using Solver s = State.MakeSolver(ctx); + s.Assert(solver.Assertions); + using (BoolExpr t = ctx.MkNot(value)) { - s.Assert(solver.Assertions); - using (BoolExpr t = ctx.MkNot(value)) - { - s.Assert(t); - } + s.Assert(t); + } - 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; + 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 @@ -1065,39 +1037,35 @@ private static Tv GetTv_Method2(BoolExpr value, BoolExpr undef, Solver solver, S bool tvFalseU; { - using (Solver s = State.MakeSolver(ctx)) + using Solver s = State.MakeSolver(ctx); + s.Assert(solver_U.Assertions); + using (BoolExpr t = ctx.MkNot(undef)) { - s.Assert(solver_U.Assertions); - using (BoolExpr t = ctx.MkNot(undef)) - { - s.Assert(t); - } + s.Assert(t); + } - Status status = s.Check(); - 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; + Status status = s.Check(); + 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; } // if (!tvFalseU) return Tv5.UNKNOWN; bool tvTrueU; { - using (Solver s = State.MakeSolver(ctx)) + using Solver s = State.MakeSolver(ctx); + s.Assert(solver_U.Assertions); + s.Assert(value); + Status status = s.Check(); + if (status == Status.UNKNOWN) { - s.Assert(solver_U.Assertions); - s.Assert(value); - Status status = s.Check(); - 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; } + tvTrueU = status == Status.SATISFIABLE; } return (tvTrueU && tvFalseU) ? Tv.UNDEFINED : Tv.UNKNOWN; } @@ -1293,6 +1261,7 @@ private static void GetConstants(Expr expr, ref IList boolResults, ref I public static IEnumerable Get_Constants(Expr expr) { Contract.Requires(expr != null); + Contract.Assume(expr != null); if (expr.IsConst) { diff --git a/VS/CSHARP/asm-sim-lib/asm-sim-lib.csproj b/VS/CSHARP/asm-sim-lib/asm-sim-lib.csproj index 57c6fab9..088b8ec6 100644 --- a/VS/CSHARP/asm-sim-lib/asm-sim-lib.csproj +++ b/VS/CSHARP/asm-sim-lib/asm-sim-lib.csproj @@ -3,14 +3,18 @@ net7.0-windows asm_sim_lib2 - enable + x64 + enable enable - x64 + true + True + latest + False - + diff --git a/VS/CSHARP/asm-sim-main/DotVisualizer.cs b/VS/CSHARP/asm-sim-main/DotVisualizer.cs index 065471e2..26d4daa7 100644 --- a/VS/CSHARP/asm-sim-main/DotVisualizer.cs +++ b/VS/CSHARP/asm-sim-main/DotVisualizer.cs @@ -36,7 +36,7 @@ public static void SaveToDot(StaticFlow sFlow, DynamicFlow dFlow, string filenam Contract.Requires(sFlow != null); Contract.Requires(dFlow != null); - AdjacencyGraph> displayGraph = new AdjacencyGraph>(); + AdjacencyGraph> displayGraph = new(); foreach (string vertex in dFlow.Graph.Vertices) { @@ -57,7 +57,7 @@ public static void SaveToDot(StaticFlow sFlow, DynamicFlow dFlow, string filenam string dir = @"C:\Temp\AsmSim") { string fullFileName = Path.Combine(dir, fileName); - GraphvizAlgorithm> viz = new GraphvizAlgorithm>(graph); + GraphvizAlgorithm> viz = new(graph); viz.FormatVertex += VizFormatVertex; viz.FormatEdge += MyEdgeFormatter; @@ -66,7 +66,7 @@ public static void SaveToDot(StaticFlow sFlow, DynamicFlow dFlow, string filenam private static void MyEdgeFormatter(object sender, FormatEdgeEventArgs> e) { - GraphvizEdgeLabel label = new GraphvizEdgeLabel + GraphvizEdgeLabel label = new() { Value = e.Edge.Tag, }; diff --git a/VS/CSHARP/asm-sim-main/ProgramZ3.cs b/VS/CSHARP/asm-sim-main/ProgramZ3.cs index a5cacfd9..fb3df57c 100644 --- a/VS/CSHARP/asm-sim-main/ProgramZ3.cs +++ b/VS/CSHARP/asm-sim-main/ProgramZ3.cs @@ -32,7 +32,6 @@ namespace AsmSim using Microsoft.Z3; using QuikGraph; - [System.Diagnostics.CodeAnalysis.SuppressMessage("Reliability", "CA2000:Dispose objects before losing scope", Justification = "")] internal class AsmSimMain { private static readonly CultureInfo Culture = CultureInfo.CurrentUICulture; @@ -60,7 +59,7 @@ private static void Main() } // TestDynamicFlow(); // TestSIMD(); - if (false) + if (true) { EmptyMemoryTest(); } @@ -99,7 +98,7 @@ private static Tools CreateTools(int timeOut = 1000) Microsoft.Z3.Global.SetParameter(System.String,System.String) */ - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat_core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation @@ -131,18 +130,18 @@ private static void TestExecutionTree() " jnz label1 " + Environment.NewLine + " mov rbx, 10 "; - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", "1000" }, }; - Tools tools = new Tools(settings) + Tools tools = new(settings) { Quiet = false, }; - StaticFlow sFlow = new StaticFlow(tools); + StaticFlow sFlow = new(tools); sFlow.Update(programStr); Console.WriteLine("sFlow=" + sFlow.ToString()); @@ -154,31 +153,29 @@ private static void TestExecutionTree() private static void TestSIMD() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", "1000" }, }; - Tools tools = new Tools(settings); + Tools tools = new(settings); tools.StateConfig.Set_All_Off(); tools.StateConfig.SIMD = true; tools.ShowUndefConstraints = true; - using (Context ctx = new Context(settings)) - { - string line1 = "xorpd xmm1, xmm1"; - string line2 = "addpd xmm1, xmm1"; + using Context ctx = new(settings); + string line1 = "xorpd xmm1, xmm1"; + string line2 = "addpd xmm1, xmm1"; - { // forward - string rootKey = "!0"; - State state = new State(tools, rootKey, rootKey); + { // forward + string rootKey = "!0"; + State state = new(tools, rootKey, rootKey); - state = Runner.SimpleStep_Forward(line1, state); - Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); - state = Runner.SimpleStep_Forward(line2, state); - Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); - } + state = Runner.SimpleStep_Forward(line1, state); + Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + state = Runner.SimpleStep_Forward(line2, state); + Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); } } @@ -268,14 +265,14 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax return y; } - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", "60000" }, // 60000=1min }; - using (Context ctx = new Context(settings)) + using (Context ctx = new(settings)) { // Solver solver = ctx.MkSolver(); Solver solver = ctx.MkSolver(ctx.MkTactic("qfbv")); @@ -519,7 +516,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax return y; } - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation @@ -538,7 +535,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax //5: (= RSP!6DE3EBEB4605B058(bvadd #x0000000000000008 RSP!3D50632C10EAA838)) //6: (= MEM!6DE3EBEB4605B058 MEM!3D50632C10EAA838) - using (Context ctx = new Context(settings)) + using (Context ctx = new(settings)) { // Solver solver = ctx.MkSolver(); Solver solver = ctx.MkSolver(ctx.MkTactic("qfbv")); @@ -727,7 +724,7 @@ BitVecExpr retrieve_mem_method_LOCAL(Context ctx, ArrayExpr mem1, BitVecExpr rax private static void TestGraph() { - BidirectionalGraph> graph = new BidirectionalGraph>(false); + BidirectionalGraph> graph = new(false); int rootVertex = 1; graph.AddVertex(1); @@ -772,7 +769,7 @@ string ToString(long vertex, int depth) /// private static void TestTactic() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation @@ -780,37 +777,35 @@ private static void TestTactic() { "timeout", "20000" }, }; - using (Context ctx = new Context(settings)) + using Context ctx = new(settings); + IntExpr x = ctx.MkIntConst("x"); + BoolExpr y = ctx.MkOr(ctx.MkGt(x, ctx.MkInt(6)), ctx.MkGt(x, ctx.MkInt(12))); + Console.WriteLine("y = " + y.ToString()); + Console.WriteLine("z0 = " + y.Simplify().ToString()); + + Tactic ctx_solver_simplify = ctx.MkTactic("ctx-solver-simplify"); + Tactic propagate_values = ctx.MkTactic("propagate-values"); + Tactic split_clause = ctx.MkTactic("split-clause"); + Tactic propagate_ineqs = ctx.MkTactic("propagate-ineqs"); + Tactic skip = ctx.MkTactic("skip"); + + Tactic tactic = ctx.AndThen(ctx_solver_simplify, ctx.AndThen(propagate_values, ctx.AndThen(ctx.Repeat(ctx.OrElse(split_clause, skip), 10), propagate_ineqs))); + Goal goal = ctx.MkGoal(); + goal.Assert(y); + ApplyResult apply_result = tactic.Apply(goal); + + foreach (Goal subgoal in apply_result.Subgoals) { - IntExpr x = ctx.MkIntConst("x"); - BoolExpr y = ctx.MkOr(ctx.MkGt(x, ctx.MkInt(6)), ctx.MkGt(x, ctx.MkInt(12))); - Console.WriteLine("y = " + y.ToString()); - Console.WriteLine("z0 = " + y.Simplify().ToString()); - - Tactic ctx_solver_simplify = ctx.MkTactic("ctx-solver-simplify"); - Tactic propagate_values = ctx.MkTactic("propagate-values"); - Tactic split_clause = ctx.MkTactic("split-clause"); - Tactic propagate_ineqs = ctx.MkTactic("propagate-ineqs"); - Tactic skip = ctx.MkTactic("skip"); - - Tactic tactic = ctx.AndThen(ctx_solver_simplify, ctx.AndThen(propagate_values, ctx.AndThen(ctx.Repeat(ctx.OrElse(split_clause, skip), 10), propagate_ineqs))); - Goal goal = ctx.MkGoal(); - goal.Assert(y); - ApplyResult apply_result = tactic.Apply(goal); - - foreach (Goal subgoal in apply_result.Subgoals) + foreach (BoolExpr e in subgoal.Formulas) { - foreach (BoolExpr e in subgoal.Formulas) - { - Console.WriteLine("z1 = " + e.ToString()); - } + Console.WriteLine("z1 = " + e.ToString()); } } } private static void TestMem2() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation @@ -818,108 +813,104 @@ private static void TestMem2() { "timeout", "20000" }, }; - using (Context ctx = new Context(settings)) - { - Tactic tactic = ctx.MkTactic("qfbv"); - Solver solver = ctx.MkSolver(tactic); - Params p = ctx.MkParams(); - p.Add("mbqi", true); // use Model-based Quantifier Instantiation - solver.Parameters = p; + using Context ctx = new(settings); + Tactic tactic = ctx.MkTactic("qfbv"); + Solver solver = ctx.MkSolver(tactic); + Params p = ctx.MkParams(); + p.Add("mbqi", true); // use Model-based Quantifier Instantiation + solver.Parameters = p; - Sort domain = ctx.MkBitVecSort(64); - Sort range = ctx.MkBitVecSort(8); + Sort domain = ctx.MkBitVecSort(64); + Sort range = ctx.MkBitVecSort(8); - ArrayExpr mem0 = ctx.MkArrayConst("MEM!0", domain, range); - ArrayExpr mem1 = ctx.MkArrayConst("MEM!1", domain, range); - BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); - BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64); + ArrayExpr mem0 = ctx.MkArrayConst("MEM!0", domain, range); + ArrayExpr mem1 = ctx.MkArrayConst("MEM!1", domain, range); + BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); + BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64); - Expr address1 = ctx.MkBV(10, 64); - Expr address2 = ctx.MkBV(7, 64); - Expr value1 = ctx.MkBV(0x1, 8); - Expr value2 = ctx.MkBV(0x2, 8); + Expr address1 = ctx.MkBV(10, 64); + Expr address2 = ctx.MkBV(7, 64); + Expr value1 = ctx.MkBV(0x1, 8); + Expr value2 = ctx.MkBV(0x2, 8); - if (false) - { - solver.Assert(ctx.MkEq(mem1, ctx.MkStore(ctx.MkStore(mem0, address2, value2), address1, value1))); - solver.Assert(ctx.MkEq(rax1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address1) as BitVecExpr))); - solver.Assert(ctx.MkEq(rbx1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address2) as BitVecExpr))); - } - else - { - BitVecExpr address = ctx.MkBVConst("address", 64); - // solver.Assert(ctx.MkForall(new Expr[] { address, mem0, mem1, rax1, rbx1 }, ctx.MkImplies(ctx.MkAnd(ctx.MkBVULE(ctx.MkBV(10, 64), address), ctx.MkBVULE(address, ctx.MkBV(5, 64))), ctx.MkEq(mem1, ctx.MkStore(mem0, address, value2))))); - solver.Assert(ctx.MkForall(new Expr[] { address, mem0, mem1, rax1, rbx1 }, ctx.MkImplies(ctx.MkOr(ctx.MkEq(ctx.MkBV(10, 64), address), ctx.MkEq(address, ctx.MkBV(5, 64))), ctx.MkEq(mem1, ctx.MkStore(mem0, address, value2))))); - solver.Assert(ctx.MkEq(rax1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address1) as BitVecExpr))); - solver.Assert(ctx.MkEq(rbx1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address2) as BitVecExpr))); - } - Console.WriteLine("solver " + solver); - Console.WriteLine("rax=" + ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rax1, 64, solver, ctx))); - Console.WriteLine("rbx=" + ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rbx1, 64, solver, ctx))); + if (false) + { + solver.Assert(ctx.MkEq(mem1, ctx.MkStore(ctx.MkStore(mem0, address2, value2), address1, value1))); + solver.Assert(ctx.MkEq(rax1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address1) as BitVecExpr))); + solver.Assert(ctx.MkEq(rbx1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address2) as BitVecExpr))); + } + else + { + BitVecExpr address = ctx.MkBVConst("address", 64); + // solver.Assert(ctx.MkForall(new Expr[] { address, mem0, mem1, rax1, rbx1 }, ctx.MkImplies(ctx.MkAnd(ctx.MkBVULE(ctx.MkBV(10, 64), address), ctx.MkBVULE(address, ctx.MkBV(5, 64))), ctx.MkEq(mem1, ctx.MkStore(mem0, address, value2))))); + solver.Assert(ctx.MkForall(new Expr[] { address, mem0, mem1, rax1, rbx1 }, ctx.MkImplies(ctx.MkOr(ctx.MkEq(ctx.MkBV(10, 64), address), ctx.MkEq(address, ctx.MkBV(5, 64))), ctx.MkEq(mem1, ctx.MkStore(mem0, address, value2))))); + solver.Assert(ctx.MkEq(rax1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address1) as BitVecExpr))); + solver.Assert(ctx.MkEq(rbx1, ctx.MkZeroExt(64 - 8, ctx.MkSelect(mem1, address2) as BitVecExpr))); } + Console.WriteLine("solver " + solver); + Console.WriteLine("rax=" + ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rax1, 64, solver, ctx))); + Console.WriteLine("rbx=" + ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rbx1, 64, solver, ctx))); } private static void Test_Rep() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", "1000" }, }; - Tools tools = new Tools(settings); + Tools tools = new(settings); tools.StateConfig.Set_All_Off(); - using (Context ctx = new Context(settings)) + using Context ctx = new(settings); + if (true) { - if (true) - { - tools.StateConfig.Set_All_Off(); - tools.StateConfig.DF = true; - tools.StateConfig.RCX = true; - tools.StateConfig.RSI = true; - tools.StateConfig.RDI = true; - tools.StateConfig.Mem = true; - - string line1 = "std"; // std = set direction flag - string line2 = "mov rdi, 100"; - string line3 = "mov rsi, 200"; - string line4 = "mov rcx, 3"; - string line5 = "rep movs"; - - { // forward - string rootKey = "!INIT"; - State state = new State(tools, rootKey, rootKey); - - state = Runner.SimpleStep_Forward(line1, state); - state = Runner.SimpleStep_Forward(line2, state); - state = Runner.SimpleStep_Forward(line3, state); - state = Runner.SimpleStep_Forward(line4, state); - - Console.WriteLine("After \"" + line4 + "\", we know:\n" + state); - state = Runner.SimpleStep_Forward(line5, state); - Console.WriteLine("After \"" + line5 + "\", we know:\n" + state); - } + tools.StateConfig.Set_All_Off(); + tools.StateConfig.DF = true; + tools.StateConfig.RCX = true; + tools.StateConfig.RSI = true; + tools.StateConfig.RDI = true; + tools.StateConfig.Mem = true; + + string line1 = "std"; // std = set direction flag + string line2 = "mov rdi, 100"; + string line3 = "mov rsi, 200"; + string line4 = "mov rcx, 3"; + string line5 = "rep movs"; + + { // forward + string rootKey = "!INIT"; + State state = new(tools, rootKey, rootKey); + + state = Runner.SimpleStep_Forward(line1, state); + state = Runner.SimpleStep_Forward(line2, state); + state = Runner.SimpleStep_Forward(line3, state); + state = Runner.SimpleStep_Forward(line4, state); + + Console.WriteLine("After \"" + line4 + "\", we know:\n" + state); + state = Runner.SimpleStep_Forward(line5, state); + Console.WriteLine("After \"" + line5 + "\", we know:\n" + state); } } } private static void Test_Usage() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", "1000" }, }; - Tools tools = new Tools(settings); + Tools tools = new(settings); (string, string, string) keys = ("dummy1", "dummy2", "dummy3"); Mnemonics.OpcodeBase opcode = Runner.InstantiateOpcode(Mnemonic.MOV, new string[] { "rbx", "ptr qword [rax + rcx]" }, keys, tools); - SortedSet read = new SortedSet(opcode.RegsReadStatic); - SortedSet write = new SortedSet(opcode.RegsWriteStatic); + SortedSet read = new(opcode.RegsReadStatic); + SortedSet write = new(opcode.RegsWriteStatic); Console.WriteLine("read = " + string.Join(",", read)); Console.WriteLine("write = " + string.Join(",", write)); @@ -927,288 +918,286 @@ private static void Test_Usage() private static void TestMnemonic() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation { "timeout", "1000" }, }; - Tools tools = new Tools(settings); + Tools tools = new(settings); tools.StateConfig.Set_All_Off(); - using (Context ctx = new Context(settings)) + using Context ctx = new(settings); + if (false) { - if (false) - { - tools.StateConfig.Set_All_Off(); - // tools.StateConfig.Set_All_Flags_On(); - tools.StateConfig.RAX = true; + tools.StateConfig.Set_All_Off(); + // tools.StateConfig.Set_All_Flags_On(); + tools.StateConfig.RAX = true; - string line1 = "mov rax, 1"; - string line2 = "shl rax, 65"; // special behaviour: shift left too large; 65 mod 64 = 1 + string line1 = "mov rax, 1"; + string line2 = "shl rax, 65"; // special behaviour: shift left too large; 65 mod 64 = 1 - { // forward - string rootKey = "!INIT"; - State state = new State(tools, rootKey, rootKey); + { // forward + string rootKey = "!INIT"; + State state = new(tools, rootKey, rootKey); - Console.WriteLine("Before \"" + line1 + "\", we know:\n" + state); - state = Runner.SimpleStep_Forward(line1, state); - Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); - state = Runner.SimpleStep_Forward(line2, state); - Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); + Console.WriteLine("Before \"" + line1 + "\", we know:\n" + state); + state = Runner.SimpleStep_Forward(line1, state); + Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + state = Runner.SimpleStep_Forward(line2, state); + Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); - Console.WriteLine("IsConsistent=" + state.IsConsistent); - } + Console.WriteLine("IsConsistent=" + state.IsConsistent); } - if (false) - { - bool logToDisplay = true; + } + if (false) + { + bool logToDisplay = true; - tools.StateConfig.Set_All_Off(); - tools.StateConfig.Set_All_Flags_On(); - tools.StateConfig.RAX = true; - tools.StateConfig.RBX = true; - tools.ShowUndefConstraints = true; + tools.StateConfig.Set_All_Off(); + tools.StateConfig.Set_All_Flags_On(); + tools.StateConfig.RAX = true; + tools.StateConfig.RBX = true; + tools.ShowUndefConstraints = true; - Random rand = new Random((int)DateTime.Now.Ticks); + Random rand = new((int)DateTime.Now.Ticks); - for (int i = 0; i < 1; ++i) - { - ulong value_rax = ToolsZ3.GetRandomUlong(rand); - ulong value_rbx = ToolsZ3.GetRandomUlong(rand); - ulong value_result = value_rax ^ value_rbx; - - string line1 = "mov rax, " + value_rax; - string line2 = "mov rbx, " + value_rbx; - string line3 = "xor rax, rbx"; - - State state = new State(tools, "!0", "!0"); - if (logToDisplay) - { - Console.WriteLine("Before line 3 with \"" + line3 + "\", we know:\n" + state); - } - - state = Runner.SimpleStep_Backward(line3, state); - if (logToDisplay) - { - Console.WriteLine("After line 3 with \"" + line3 + "\", we know:\n" + state); - } - - state = Runner.SimpleStep_Backward(line2, state); - if (logToDisplay) - { - Console.WriteLine("After line 2 with \"" + line2 + "\", we know:\n" + state); - } - - state = Runner.SimpleStep_Backward(line1, state); - if (logToDisplay) - { - Console.WriteLine("After line 1 with \"" + line1 + "\", we know:\n" + state); - } - } - } - if (false) + for (int i = 0; i < 1; ++i) { -#pragma warning disable CS0162 // Unreachable code detected - tools.StateConfig.RAX = true; - tools.StateConfig.RBX = true; - tools.StateConfig.RCX = true; - tools.StateConfig.CF = true; + ulong value_rax = ToolsZ3.GetRandomUlong(rand); + ulong value_rbx = ToolsZ3.GetRandomUlong(rand); + ulong value_result = value_rax ^ value_rbx; - string line1 = "mov rax, rbx"; - string line2 = "xor rax, rbx"; - string line3 = "rcl rax, cl"; + string line1 = "mov rax, " + value_rax; + string line2 = "mov rbx, " + value_rbx; + string line3 = "xor rax, rbx"; - string rootKey = "!0"; - State state = new State(tools, rootKey, rootKey); - - state = Runner.SimpleStep_Forward(line1, state); - state = Runner.SimpleStep_Forward(line2, state); - state = Runner.SimpleStep_Forward(line3, state); - Console.WriteLine("After \"" + line3 + "\", we know:\n" + state); - } - if (false) - { - tools.StateConfig.RAX = true; - tools.StateConfig.RBX = true; - - string line1 = "mov rax, 10"; - string line2 = "mov rbx, 20"; - string line3 = "add rax, rbx"; - - string rootKey = "!0"; - State state = new State(tools, rootKey, rootKey); + State state = new(tools, "!0", "!0"); + if (logToDisplay) + { + Console.WriteLine("Before line 3 with \"" + line3 + "\", we know:\n" + state); + } - Console.WriteLine("Before \"" + line3 + "\", we know:\n" + state); state = Runner.SimpleStep_Backward(line3, state); - Console.WriteLine("After \"" + line3 + "\", we know:\n" + state); + if (logToDisplay) + { + Console.WriteLine("After line 3 with \"" + line3 + "\", we know:\n" + state); + } + state = Runner.SimpleStep_Backward(line2, state); - Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); + if (logToDisplay) + { + Console.WriteLine("After line 2 with \"" + line2 + "\", we know:\n" + state); + } + state = Runner.SimpleStep_Backward(line1, state); - Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + if (logToDisplay) + { + Console.WriteLine("After line 1 with \"" + line1 + "\", we know:\n" + state); + } } - if (false) - { - ulong a = 0b0000_1000; - ulong b = 0b0000_0100; + } + if (false) + { +#pragma warning disable CS0162 // Unreachable code detected + tools.StateConfig.RAX = true; + tools.StateConfig.RBX = true; + tools.StateConfig.RCX = true; + tools.StateConfig.CF = true; - string tailKey = Tools.CreateKey(tools.Rand); - string headKey = Tools.CreateKey(tools.Rand); - State state = new State(tools, tailKey, headKey); + string line1 = "mov rax, rbx"; + string line2 = "xor rax, rbx"; + string line3 = "rcl rax, cl"; - string line1 = "add al, bl"; + string rootKey = "!0"; + State state = new(tools, rootKey, rootKey); - string nextKey = Tools.CreateKey(state.Tools.Rand); - StateUpdate updateState = new StateUpdate(state.TailKey, nextKey, state.Tools); - updateState.Set(Rn.AL, a); - updateState.Set(Rn.BL, b); + state = Runner.SimpleStep_Forward(line1, state); + state = Runner.SimpleStep_Forward(line2, state); + state = Runner.SimpleStep_Forward(line3, state); + Console.WriteLine("After \"" + line3 + "\", we know:\n" + state); + } + if (false) + { + tools.StateConfig.RAX = true; + tools.StateConfig.RBX = true; + + string line1 = "mov rax, 10"; + string line2 = "mov rbx, 20"; + string line3 = "add rax, rbx"; + + string rootKey = "!0"; + State state = new(tools, rootKey, rootKey); + + Console.WriteLine("Before \"" + line3 + "\", we know:\n" + state); + state = Runner.SimpleStep_Backward(line3, state); + Console.WriteLine("After \"" + line3 + "\", we know:\n" + state); + state = Runner.SimpleStep_Backward(line2, state); + Console.WriteLine("After \"" + line2 + "\", we know:\n" + state); + state = Runner.SimpleStep_Backward(line1, state); + Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + } + if (false) + { + ulong a = 0b0000_1000; + ulong b = 0b0000_0100; - state.Update_Forward(updateState); - // if (logToDisplay) Console.WriteLine("Before \"" + line1 + "\", we know:\n" + state); + string tailKey = Tools.CreateKey(tools.Rand); + string headKey = Tools.CreateKey(tools.Rand); + State state = new(tools, tailKey, headKey); - state = Runner.SimpleStep_Forward(line1, state); - Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + string line1 = "add al, bl"; - Console.WriteLine(ToolsZ3.ToStringBin(state.GetTvArray(Rn.AL))); - } - if (false) - { - tools.StateConfig.Set_All_Off(); - tools.StateConfig.RAX = true; - tools.StateConfig.RBX = true; - tools.StateConfig.ZF = true; - - string programStr = - // " xor rax, rax " + Environment.NewLine + - " jz label1 " + Environment.NewLine + - " mov rax, 1 " + Environment.NewLine + - " jmp label2 " + Environment.NewLine + - "label1: " + Environment.NewLine + - " mov rax, 2 " + Environment.NewLine + - "label2: " + Environment.NewLine + - " mov rbx, 0 "; - - StaticFlow sFlow1 = new StaticFlow(tools); - sFlow1.Update(programStr); - Console.WriteLine(sFlow1); + string nextKey = Tools.CreateKey(state.Tools.Rand); + StateUpdate updateState = new(state.TailKey, nextKey, state.Tools); + updateState.Set(Rn.AL, a); + updateState.Set(Rn.BL, b); - tools.Quiet = false; - DynamicFlow tree1 = new DynamicFlow(tools); - tree1.Reset(sFlow1, false); - Console.WriteLine(tree1.Create_EndState); - } - if (false) - { - tools.StateConfig.Set_All_Off(); - tools.StateConfig.RAX = true; - tools.StateConfig.RBX = true; - tools.StateConfig.ZF = true; - tools.StateConfig.Mem = true; + state.Update_Forward(updateState); + // if (logToDisplay) Console.WriteLine("Before \"" + line1 + "\", we know:\n" + state); - string programStr0 = + state = Runner.SimpleStep_Forward(line1, state); + Console.WriteLine("After \"" + line1 + "\", we know:\n" + state); + + Console.WriteLine(ToolsZ3.ToStringBin(state.GetTvArray(Rn.AL))); + } + if (false) + { + tools.StateConfig.Set_All_Off(); + tools.StateConfig.RAX = true; + tools.StateConfig.RBX = true; + tools.StateConfig.ZF = true; + + string programStr = + // " xor rax, rax " + Environment.NewLine + " jz label1 " + Environment.NewLine + - " mov byte ptr[rax], 10 " + Environment.NewLine + + " mov rax, 1 " + Environment.NewLine + " jmp label2 " + Environment.NewLine + "label1: " + Environment.NewLine + - " mov byte ptr[rax], 20 " + Environment.NewLine + + " mov rax, 2 " + Environment.NewLine + "label2: " + Environment.NewLine + - " mov bl, byte ptr[rax] "; - - StaticFlow sFlow = new StaticFlow(tools); - sFlow.Update(programStr0); - Console.WriteLine(sFlow); + " mov rbx, 0 "; - if (false) - { - tools.Quiet = false; - DynamicFlow tree0 = Runner.Construct_DynamicFlow_Forward(sFlow, tools); + StaticFlow sFlow1 = new(tools); + sFlow1.Update(programStr); + Console.WriteLine(sFlow1); - int lineNumber_JZ = 0; - State state_FirstLine = tree0.Create_States_Before(lineNumber_JZ, 0); - BranchInfo branchInfo = new BranchInfo(state_FirstLine.Create(Flags.ZF), true); + tools.Quiet = false; + DynamicFlow tree1 = new(tools); + tree1.Reset(sFlow1, false); + Console.WriteLine(tree1.Create_EndState); + } + if (false) + { + tools.StateConfig.Set_All_Off(); + tools.StateConfig.RAX = true; + tools.StateConfig.RBX = true; + tools.StateConfig.ZF = true; + tools.StateConfig.Mem = true; - State state0 = tree0.Create_EndState; - state0.BranchInfoStore.Add(branchInfo, true); - Console.WriteLine("State0:" + state0); - } -#pragma warning restore CS0162 // Unreachable code detected - if (true) - { - tools.Quiet = false; - DynamicFlow tree1 = Runner.Construct_DynamicFlow_Backward(sFlow, tools); + string programStr0 = + " jz label1 " + Environment.NewLine + + " mov byte ptr[rax], 10 " + Environment.NewLine + + " jmp label2 " + Environment.NewLine + + "label1: " + Environment.NewLine + + " mov byte ptr[rax], 20 " + Environment.NewLine + + "label2: " + Environment.NewLine + + " mov bl, byte ptr[rax] "; - int lineNumber_JZ = 0; - State state_FirstLine = tree1.Create_States_Before(lineNumber_JZ, 0); - BranchInfo branchInfo = new BranchInfo(state_FirstLine.Create(Flags.ZF), false); + StaticFlow sFlow = new(tools); + sFlow.Update(programStr0); + Console.WriteLine(sFlow); - State state1 = tree1.Create_EndState; - state1.BranchInfoStore.Add(branchInfo, true); - Console.WriteLine("State1:" + state1); - } - } if (false) { - string programStr1 = - "mov rax, 0" + Environment.NewLine + - "mov ptr qword[rax], 2"; - - string programStr2 = - "mov rbx, 1" + Environment.NewLine + - "mov ptr qword[rbx], 3"; + tools.Quiet = false; + DynamicFlow tree0 = Runner.Construct_DynamicFlow_Forward(sFlow, tools); - StaticFlow sFlow1 = new StaticFlow(tools); - sFlow1.Update(programStr1); - StaticFlow sFlow2 = new StaticFlow(tools); - sFlow2.Update(programStr2); + int lineNumber_JZ = 0; + State state_FirstLine = tree0.Create_States_Before(lineNumber_JZ, 0); + BranchInfo branchInfo = new(state_FirstLine.Create(Flags.ZF), true); - tools.Quiet = true; - tools.StateConfig.Set_All_Off(); - tools.StateConfig.RAX = true; - tools.StateConfig.RBX = true; - tools.StateConfig.Mem = true; + State state0 = tree0.Create_EndState; + state0.BranchInfoStore.Add(branchInfo, true); + Console.WriteLine("State0:" + state0); + } +#pragma warning restore CS0162 // Unreachable code detected + if (true) + { + tools.Quiet = false; + DynamicFlow tree1 = Runner.Construct_DynamicFlow_Backward(sFlow, tools); - DynamicFlow tree1 = Runner.Construct_DynamicFlow_Forward(sFlow1, tools); - DynamicFlow tree2 = Runner.Construct_DynamicFlow_Forward(sFlow2, tools); + int lineNumber_JZ = 0; + State state_FirstLine = tree1.Create_States_Before(lineNumber_JZ, 0); + BranchInfo branchInfo = new(state_FirstLine.Create(Flags.ZF), false); - // Console.WriteLine(tree1.ToString(flow1)); State state1 = tree1.Create_EndState; - State state2 = tree2.Create_EndState; - - Console.WriteLine("state1:" + state1); - Console.WriteLine("state2:" + state2); - State mergedState = new State(state1, state2, true); - Console.WriteLine("mergedState:" + mergedState); + state1.BranchInfoStore.Add(branchInfo, true); + Console.WriteLine("State1:" + state1); } - if (false) - { - string programStr1 = - "mov rax, 0" + Environment.NewLine + - "mov rbx, 0"; + } + if (false) + { + string programStr1 = + "mov rax, 0" + Environment.NewLine + + "mov ptr qword[rax], 2"; - string programStr2 = - "mov rax, 1" + Environment.NewLine + - "mov rbx, 1"; + string programStr2 = + "mov rbx, 1" + Environment.NewLine + + "mov ptr qword[rbx], 3"; - StaticFlow sFlow1 = new StaticFlow(tools); - sFlow1.Update(programStr1); - StaticFlow sFlow2 = new StaticFlow(tools); - sFlow2.Update(programStr2); + StaticFlow sFlow1 = new(tools); + sFlow1.Update(programStr1); + StaticFlow sFlow2 = new(tools); + sFlow2.Update(programStr2); - tools.Quiet = true; + tools.Quiet = true; + tools.StateConfig.Set_All_Off(); + tools.StateConfig.RAX = true; + tools.StateConfig.RBX = true; + tools.StateConfig.Mem = true; + + DynamicFlow tree1 = Runner.Construct_DynamicFlow_Forward(sFlow1, tools); + DynamicFlow tree2 = Runner.Construct_DynamicFlow_Forward(sFlow2, tools); + + // Console.WriteLine(tree1.ToString(flow1)); + State state1 = tree1.Create_EndState; + State state2 = tree2.Create_EndState; + + Console.WriteLine("state1:" + state1); + Console.WriteLine("state2:" + state2); + State mergedState = new(state1, state2, true); + Console.WriteLine("mergedState:" + mergedState); + } + if (false) + { + string programStr1 = + "mov rax, 0" + Environment.NewLine + + "mov rbx, 0"; - DynamicFlow tree1 = Runner.Construct_DynamicFlow_Forward(sFlow1, tools); - DynamicFlow tree2 = Runner.Construct_DynamicFlow_Forward(sFlow2, tools); + string programStr2 = + "mov rax, 1" + Environment.NewLine + + "mov rbx, 1"; - // Console.WriteLine(tree1.ToString(flow1)); + StaticFlow sFlow1 = new(tools); + sFlow1.Update(programStr1); + StaticFlow sFlow2 = new(tools); + sFlow2.Update(programStr2); - State state1 = tree1.Create_Leafs.ElementAt(0); - State state2 = tree2.Create_Leafs.ElementAt(0); + tools.Quiet = true; - Console.WriteLine("state1:" + state1); - Console.WriteLine("state2:" + state2); - State mergedState = new State(state1, state2, true); - Console.WriteLine("mergedState:" + mergedState); - } + DynamicFlow tree1 = Runner.Construct_DynamicFlow_Forward(sFlow1, tools); + DynamicFlow tree2 = Runner.Construct_DynamicFlow_Forward(sFlow2, tools); + + // Console.WriteLine(tree1.ToString(flow1)); + + State state1 = tree1.Create_Leafs.ElementAt(0); + State state2 = tree2.Create_Leafs.ElementAt(0); + + Console.WriteLine("state1:" + state1); + Console.WriteLine("state2:" + state2); + State mergedState = new(state1, state2, true); + Console.WriteLine("mergedState:" + mergedState); } } @@ -1296,7 +1285,7 @@ private static void TestDynamicFlow() " movbe dword ptr [rbx], eax " + Environment.NewLine + " mov eax, dword ptr [rbx] "; - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation @@ -1304,12 +1293,12 @@ private static void TestDynamicFlow() { "timeout", "1000" }, }; - Tools tools = new Tools(settings) + Tools tools = new(settings) { ShowUndefConstraints = false, }; - StaticFlow sFlow = new StaticFlow(tools); + StaticFlow sFlow = new(tools); sFlow.Update(programStr8); Console.WriteLine(sFlow.ToString()); tools.StateConfig = sFlow.Create_StateConfig(); @@ -1347,54 +1336,52 @@ private static void TestDynamicFlow() private static void EmptyMemoryTest() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation { "proof", "false" }, // enable proof generation }; - using (Context ctx = new Context(settings)) - { - Tactic tactic = ctx.MkTactic("qfbv"); - Solver solver = ctx.MkSolver(tactic); + using Context ctx = new(settings); + Tactic tactic = ctx.MkTactic("qfbv"); + Solver solver = ctx.MkSolver(tactic); - if (false) - { - ArrayExpr mem0 = ctx.MkArrayConst("memory", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); - Expr address1 = ctx.MkBV(10, 64); - Expr address2 = ctx.MkBV(12, 64); - Expr value = ctx.MkBV(0xFF, 8); + if (false) + { + ArrayExpr mem0 = ctx.MkArrayConst("memory", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); + Expr address1 = ctx.MkBV(10, 64); + Expr address2 = ctx.MkBV(12, 64); + Expr value = ctx.MkBV(0xFF, 8); - ArrayExpr mem1 = ctx.MkStore(mem0, address1, value); - Console.WriteLine("Stored value " + value); + ArrayExpr mem1 = ctx.MkStore(mem0, address1, value); + Console.WriteLine("Stored value " + value); - Expr retrievedValue1 = ctx.MkSelect(mem1, address1); - Console.WriteLine("Retrieved value 1 " + retrievedValue1); - Console.WriteLine("Retrieved value 1 Simplified " + retrievedValue1.Simplify()); + Expr retrievedValue1 = ctx.MkSelect(mem1, address1); + Console.WriteLine("Retrieved value 1 " + retrievedValue1); + Console.WriteLine("Retrieved value 1 Simplified " + retrievedValue1.Simplify()); - Expr retrievedValue2 = ctx.MkSelect(mem1, address2); - Console.WriteLine("Retrieved value 2 " + retrievedValue2); - Console.WriteLine("Retrieved value 2 Simplified " + retrievedValue2.Simplify()); - } - if (true) - { - ArrayExpr mem0 = ctx.MkConstArray(ctx.MkBitVecSort(64), ctx.MkBV(0, 8)); - Expr address1 = ctx.MkBV(10, 64); - Expr address2 = ctx.MkBV(12, 64); - Expr value = ctx.MkBV(0xFF, 8); + Expr retrievedValue2 = ctx.MkSelect(mem1, address2); + Console.WriteLine("Retrieved value 2 " + retrievedValue2); + Console.WriteLine("Retrieved value 2 Simplified " + retrievedValue2.Simplify()); + } + if (true) + { + ArrayExpr mem0 = ctx.MkConstArray(ctx.MkBitVecSort(64), ctx.MkBV(0, 8)); + Expr address1 = ctx.MkBV(10, 64); + Expr address2 = ctx.MkBV(12, 64); + Expr value = ctx.MkBV(0xFF, 8); - ArrayExpr mem1 = ctx.MkStore(mem0, address1, value); - Console.WriteLine("Stored value " + value); + ArrayExpr mem1 = ctx.MkStore(mem0, address1, value); + Console.WriteLine("Stored value " + value); - Expr retrievedValue1 = ctx.MkSelect(mem1, address1); - // Console.WriteLine("Retrieved value 1 " + retrievedValue1); - Console.WriteLine("Retrieved value 1 Simplified " + retrievedValue1.Simplify()); + Expr retrievedValue1 = ctx.MkSelect(mem1, address1); + // Console.WriteLine("Retrieved value 1 " + retrievedValue1); + Console.WriteLine("Retrieved value 1 Simplified " + retrievedValue1.Simplify()); - Expr retrievedValue2 = ctx.MkSelect(mem1, address2); - // Console.WriteLine("Retrieved value 2 " + retrievedValue2); - Console.WriteLine("Retrieved value 2 Simplified " + retrievedValue2.Simplify()); - } + Expr retrievedValue2 = ctx.MkSelect(mem1, address2); + // Console.WriteLine("Retrieved value 2 " + retrievedValue2); + Console.WriteLine("Retrieved value 2 Simplified " + retrievedValue2.Simplify()); } } @@ -1402,297 +1389,291 @@ private static void ProgramSynthesis1() { if (false) { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "true" }, // enable model generation { "proof", "false" }, // enable proof generation }; - using (Context ctx = new Context(settings)) - { - Solver solver = ctx.MkSolver(); + using Context ctx = new(settings); + Solver solver = ctx.MkSolver(); - BoolExpr b1 = ctx.MkBoolConst("b1"); - BoolExpr b2 = ctx.MkBoolConst("b2"); - IntExpr i1 = ctx.MkIntConst("i1"); - IntExpr i2 = ctx.MkIntConst("i2"); + BoolExpr b1 = ctx.MkBoolConst("b1"); + BoolExpr b2 = ctx.MkBoolConst("b2"); + IntExpr i1 = ctx.MkIntConst("i1"); + IntExpr i2 = ctx.MkIntConst("i2"); - if (false) - { - solver.Assert(ctx.MkOr(ctx.MkNot(b1), ctx.MkLt(ctx.MkInt(0), i1), ctx.MkAnd(b2, ctx.MkEq(i1, i2)))); - Console.WriteLine(solver); - } - else - { - FuncDecl myFunc = ctx.MkFuncDecl("MyFunc", ctx.MkIntSort(), ctx.MkBoolSort()); + if (false) + { + solver.Assert(ctx.MkOr(ctx.MkNot(b1), ctx.MkLt(ctx.MkInt(0), i1), ctx.MkAnd(b2, ctx.MkEq(i1, i2)))); + Console.WriteLine(solver); + } + else + { + FuncDecl myFunc = ctx.MkFuncDecl("MyFunc", ctx.MkIntSort(), ctx.MkBoolSort()); - BoolExpr newState = ctx.MkOr(ctx.MkNot(b1), ctx.MkLt(ctx.MkInt(0), i1), ctx.MkAnd(b2, ctx.MkEq(i1, i2))); - solver.Assert(ctx.MkQuantifier(true, new Expr[] { i1 }, ctx.MkEq(myFunc.Apply(i1), ctx.MkOr(ctx.MkNot(b1), ctx.MkLt(ctx.MkInt(0), i1), ctx.MkAnd(b2, ctx.MkEq(i1, i2)))))); + BoolExpr newState = ctx.MkOr(ctx.MkNot(b1), ctx.MkLt(ctx.MkInt(0), i1), ctx.MkAnd(b2, ctx.MkEq(i1, i2))); + solver.Assert(ctx.MkQuantifier(true, new Expr[] { i1 }, ctx.MkEq(myFunc.Apply(i1), ctx.MkOr(ctx.MkNot(b1), ctx.MkLt(ctx.MkInt(0), i1), ctx.MkAnd(b2, ctx.MkEq(i1, i2)))))); - solver.Assert(b1); + solver.Assert(b1); - Console.WriteLine(solver); - Status status = solver.Check(); - Console.WriteLine("Status = " + status); - if (status == Status.SATISFIABLE) - { - Console.WriteLine(solver.Model); - } + Console.WriteLine(solver); + Status status = solver.Check(); + Console.WriteLine("Status = " + status); + if (status == Status.SATISFIABLE) + { + Console.WriteLine(solver.Model); } } } else if (true) { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "true" }, // enable generation of unsat cores { "model", "true" }, // enable model generation { "proof", "false" }, // enable proof generation }; - using (Context ctx = new Context(settings)) - { - Solver solver = ctx.MkSolver(); + using Context ctx = new(settings); + Solver solver = ctx.MkSolver(); - IList switchList = new List(); + IList switchList = new List(); - BitVecExpr rax_0 = ctx.MkBVConst("RAX!0", 8); // register values - BitVecExpr rax_1 = ctx.MkBVConst("RAX!1", 8); + BitVecExpr rax_0 = ctx.MkBVConst("RAX!0", 8); // register values + BitVecExpr rax_1 = ctx.MkBVConst("RAX!1", 8); - BoolExpr switch_XOR_RAX_RAX = ctx.MkBoolConst("switch_XOR_RAX_RAX"); // switch on/off instruction 1 - BoolExpr switch_INC_RAX = ctx.MkBoolConst("switch_INC_RAX"); // switch on/off instruction 2 + BoolExpr switch_XOR_RAX_RAX = ctx.MkBoolConst("switch_XOR_RAX_RAX"); // switch on/off instruction 1 + BoolExpr switch_INC_RAX = ctx.MkBoolConst("switch_INC_RAX"); // switch on/off instruction 2 - // solver.Assert(switch_XOR_RAX_RAX); // this instruction should not be allowed - solver.Assert(switch_INC_RAX); // this instruction has to be allowed + // solver.Assert(switch_XOR_RAX_RAX); // this instruction should not be allowed + solver.Assert(switch_INC_RAX); // this instruction has to be allowed - solver.Assert(ctx.MkImplies(switch_XOR_RAX_RAX, ctx.MkEq(rax_1, ctx.MkBV(0, 8)))); - solver.Assert(ctx.MkImplies(switch_INC_RAX, ctx.MkEq(rax_1, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8))))); + solver.Assert(ctx.MkImplies(switch_XOR_RAX_RAX, ctx.MkEq(rax_1, ctx.MkBV(0, 8)))); + solver.Assert(ctx.MkImplies(switch_INC_RAX, ctx.MkEq(rax_1, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8))))); - // atleast and atmost one instruction must be executed - solver.Assert(ctx.MkAtMost(new BoolExpr[] { switch_XOR_RAX_RAX, switch_INC_RAX }, 1)); - solver.Assert(ctx.MkOr(new BoolExpr[] { switch_XOR_RAX_RAX, switch_INC_RAX })); + // atleast and atmost one instruction must be executed + solver.Assert(ctx.MkAtMost(new BoolExpr[] { switch_XOR_RAX_RAX, switch_INC_RAX }, 1)); + solver.Assert(ctx.MkOr(new BoolExpr[] { switch_XOR_RAX_RAX, switch_INC_RAX })); - // after executing we want rax to be 0 - if (false) - { - solver.Assert(ctx.MkEq(rax_1, ctx.MkBV(0b0000_0000, 8))); - } - else - { - BitVecExpr reg_0 = ctx.MkBVConst("reg0", 8); - BitVecExpr reg_1 = ctx.MkBVConst("reg1", 8); - - solver.Assert(ctx.MkNot(ctx.MkQuantifier(true, new Expr[] { reg_0, reg_1 }, - ctx.MkIff( - ctx.MkAnd( - ctx.MkEq(ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8)), reg_0), - ctx.MkEq(rax_1, reg_1) - ), - ctx.MkEq(reg_0, reg_1)) - ) - )); - // solver.Assert(ctx.MkNot(ctx.MkEq(rax_0, ctx.MkBV(0, 64)))); - /* - solver.Assert(ctx.MkNot(ctx.MkQuantifier(false, new Expr[] { reg1 }, - ctx.MkAnd(ctx.MkEq(reg1, rax_1), ctx.MkNot(ctx.MkEq(reg1, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8))))) - ))); - */ - /* - solver.Assert(ctx.MkQuantifier(true, new Expr[] { reg1 }, ctx.MkAnd( - ctx.MkIff(ctx.MkEq(reg1, rax_1), ctx.MkEq(reg1, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8)))), - ctx.MkIff(ctx.MkEq(reg2, rax_1), ctx.MkEq(reg2, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8)))), - ctx.MkNot(ctx.MkEq(reg1, reg2)) - ))); - */ - } + // after executing we want rax to be 0 + if (false) + { + solver.Assert(ctx.MkEq(rax_1, ctx.MkBV(0b0000_0000, 8))); + } + else + { + BitVecExpr reg_0 = ctx.MkBVConst("reg0", 8); + BitVecExpr reg_1 = ctx.MkBVConst("reg1", 8); + + solver.Assert(ctx.MkNot(ctx.MkQuantifier(true, new Expr[] { reg_0, reg_1 }, + ctx.MkIff( + ctx.MkAnd( + ctx.MkEq(ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8)), reg_0), + ctx.MkEq(rax_1, reg_1) + ), + ctx.MkEq(reg_0, reg_1)) + ) + )); + // solver.Assert(ctx.MkNot(ctx.MkEq(rax_0, ctx.MkBV(0, 64)))); + /* + solver.Assert(ctx.MkNot(ctx.MkQuantifier(false, new Expr[] { reg1 }, + ctx.MkAnd(ctx.MkEq(reg1, rax_1), ctx.MkNot(ctx.MkEq(reg1, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8))))) + ))); + */ + /* + solver.Assert(ctx.MkQuantifier(true, new Expr[] { reg1 }, ctx.MkAnd( + ctx.MkIff(ctx.MkEq(reg1, rax_1), ctx.MkEq(reg1, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8)))), + ctx.MkIff(ctx.MkEq(reg2, rax_1), ctx.MkEq(reg2, ctx.MkBVAdd(rax_0, ctx.MkBV(1, 8)))), + ctx.MkNot(ctx.MkEq(reg1, reg2)) + ))); + */ + } - foreach (BoolExpr b in solver.Assertions) - { - Console.WriteLine("Solver A: " + b); - } + foreach (BoolExpr b in solver.Assertions) + { + Console.WriteLine("Solver A: " + b); + } - Console.WriteLine("-------------"); + Console.WriteLine("-------------"); - Status status = solver.Check(); - Console.WriteLine("Status = " + status); - if (status == Status.SATISFIABLE) + Status status = solver.Check(); + Console.WriteLine("Status = " + status); + if (status == Status.SATISFIABLE) + { + foreach (FuncDecl funcDecl in solver.Model.ConstDecls) { - foreach (FuncDecl funcDecl in solver.Model.ConstDecls) - { - Console.WriteLine("Model A: " + funcDecl.Name + "=" + solver.Model.ConstInterp(funcDecl)); - } + Console.WriteLine("Model A: " + funcDecl.Name + "=" + solver.Model.ConstInterp(funcDecl)); } - else + } + else + { + foreach (BoolExpr b in solver.UnsatCore) { - foreach (BoolExpr b in solver.UnsatCore) - { - Console.WriteLine("Uncore: " + b); - } + Console.WriteLine("Uncore: " + b); } } } else if (false) { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "true" }, // enable generation of unsat cores { "model", "true" }, // enable model generation { "proof", "false" }, // enable proof generation }; - using (Context ctx = new Context(settings)) - { - Solver solver = ctx.MkSolver(); - - BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); - BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); - BitVecExpr rbx0 = ctx.MkBVConst("RBX!0", 64); - BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64); - - BoolExpr rax0_input = ctx.MkBoolConst("RAX!0!input"); - BoolExpr rax1_input = ctx.MkBoolConst("RAX!1!input"); - BoolExpr rbx0_input = ctx.MkBoolConst("RBX!0!input"); - BoolExpr rbx1_input = ctx.MkBoolConst("RBX!1!input"); - - BoolExpr rax0_goal = ctx.MkBoolConst("RAX!0!goal"); - BoolExpr rax1_goal = ctx.MkBoolConst("RAX!1!goal"); - BoolExpr rbx0_goal = ctx.MkBoolConst("RBX!0!goal"); - BoolExpr rbx1_goal = ctx.MkBoolConst("RBX!1!goal"); - - // switches - BoolExpr switch_L1_INC_RAX = ctx.MkBoolConst("switch_L1_INC_RAX"); - BoolExpr switch_L1_INC_RBX = ctx.MkBoolConst("switch_L1_INC_RBX"); - - BoolExpr switch_L1_XOR_RAX_RAX = ctx.MkBoolConst("switch_L1_XOR_RAX_RAX"); - BoolExpr switch_L1_XOR_RBX_RBX = ctx.MkBoolConst("switch_L1_XOR_RBX_RBX"); - - solver.Assert(ctx.MkAtMost(new BoolExpr[] { switch_L1_INC_RAX, switch_L1_INC_RBX, switch_L1_XOR_RAX_RAX, switch_L1_XOR_RBX_RBX }, 1)); - solver.Assert(ctx.MkOr(new BoolExpr[] { switch_L1_INC_RAX, switch_L1_INC_RBX, switch_L1_XOR_RAX_RAX, switch_L1_XOR_RBX_RBX })); - - BitVecExpr zERO = ctx.MkBV(0, 64); - BitVecExpr oNE = ctx.MkBV(1, 64); - - // INC RAX - solver.Assert(ctx.MkImplies( - ctx.MkAnd(switch_L1_INC_RAX), - ctx.MkAnd(ctx.MkEq(rax1, ctx.MkBVAdd(rax0, oNE)), - rax0_goal, // make the prerequisite a goal - rax1_goal, // make application of this rule goal directed - rax0_input, // rax0 is based on (variable) input but is not a constant - rax1_input)) // rax1 is based on (variable) input but is not a constant - ); - - // INC RBX - solver.Assert(ctx.MkImplies( - ctx.MkAnd(switch_L1_INC_RBX), - ctx.MkAnd(ctx.MkEq(rax1, ctx.MkBVAdd(rbx0, oNE)), - rbx0_goal, // make the prerequisite a goal - rbx1_goal, // make application of this rule goal directed - rbx0_input, // rax0 is based on (variable) input but is not a constant - rbx1_input)) // rax1 is based on (variable) input but is not a constant - ); - - // XOR RAX, RAX - solver.Assert(ctx.MkImplies( - ctx.MkAnd(switch_L1_XOR_RAX_RAX), - ctx.MkAnd(ctx.MkEq(rax1, zERO), - // rax0_goal is irelevant - rax1_goal, // make application of this rule goal directed - ctx.MkNot(rax0_input), // TODO: could this create inconsistencies with other instructions that updated rax!0 - ctx.MkNot(rax1_input))) // rax1 is not based on (variable) input but is a constant - ); - - // XOR RBX, RBX - solver.Assert(ctx.MkImplies( - ctx.MkAnd(switch_L1_XOR_RBX_RBX), - ctx.MkAnd(ctx.MkEq(rbx1, zERO), - // rbx0_goal is irelevant - rbx1_goal, // make application of this rule goal directed - ctx.MkNot(rbx0_input), // TODO: could this create inconsistencies with other instructions that updated rax!0 - ctx.MkNot(rbx1_input))) // rax1 is not based on (variable) input but is a constant - ); - - { // check INC RAX - solver.Push(); - solver.Assert(ctx.MkEq(rax1, ctx.MkBVAdd(rax0, ctx.MkBV(1, 64)))); - solver.Assert(rax0_input, rax1_goal); - - if (solver.Check(switch_L1_INC_RAX) == Status.UNSATISFIABLE) - { - Console.WriteLine("A: INC RAX: switch_INC SHOULD HAVE BEEN ALLOWED"); - } + using Context ctx = new(settings); + Solver solver = ctx.MkSolver(); - if (solver.Check(switch_L1_XOR_RAX_RAX) == Status.SATISFIABLE) - { - Console.WriteLine("A: XOR RAX, RAX: switch_XOR SHOULD NOT HAVE BEEN ALLOWED"); - } + BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); + BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); + BitVecExpr rbx0 = ctx.MkBVConst("RBX!0", 64); + BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64); - solver.Pop(); + BoolExpr rax0_input = ctx.MkBoolConst("RAX!0!input"); + BoolExpr rax1_input = ctx.MkBoolConst("RAX!1!input"); + BoolExpr rbx0_input = ctx.MkBoolConst("RBX!0!input"); + BoolExpr rbx1_input = ctx.MkBoolConst("RBX!1!input"); + + BoolExpr rax0_goal = ctx.MkBoolConst("RAX!0!goal"); + BoolExpr rax1_goal = ctx.MkBoolConst("RAX!1!goal"); + BoolExpr rbx0_goal = ctx.MkBoolConst("RBX!0!goal"); + BoolExpr rbx1_goal = ctx.MkBoolConst("RBX!1!goal"); + + // switches + BoolExpr switch_L1_INC_RAX = ctx.MkBoolConst("switch_L1_INC_RAX"); + BoolExpr switch_L1_INC_RBX = ctx.MkBoolConst("switch_L1_INC_RBX"); + + BoolExpr switch_L1_XOR_RAX_RAX = ctx.MkBoolConst("switch_L1_XOR_RAX_RAX"); + BoolExpr switch_L1_XOR_RBX_RBX = ctx.MkBoolConst("switch_L1_XOR_RBX_RBX"); + + solver.Assert(ctx.MkAtMost(new BoolExpr[] { switch_L1_INC_RAX, switch_L1_INC_RBX, switch_L1_XOR_RAX_RAX, switch_L1_XOR_RBX_RBX }, 1)); + solver.Assert(ctx.MkOr(new BoolExpr[] { switch_L1_INC_RAX, switch_L1_INC_RBX, switch_L1_XOR_RAX_RAX, switch_L1_XOR_RBX_RBX })); + + BitVecExpr zERO = ctx.MkBV(0, 64); + BitVecExpr oNE = ctx.MkBV(1, 64); + + // INC RAX + solver.Assert(ctx.MkImplies( + ctx.MkAnd(switch_L1_INC_RAX), + ctx.MkAnd(ctx.MkEq(rax1, ctx.MkBVAdd(rax0, oNE)), + rax0_goal, // make the prerequisite a goal + rax1_goal, // make application of this rule goal directed + rax0_input, // rax0 is based on (variable) input but is not a constant + rax1_input)) // rax1 is based on (variable) input but is not a constant + ); + + // INC RBX + solver.Assert(ctx.MkImplies( + ctx.MkAnd(switch_L1_INC_RBX), + ctx.MkAnd(ctx.MkEq(rax1, ctx.MkBVAdd(rbx0, oNE)), + rbx0_goal, // make the prerequisite a goal + rbx1_goal, // make application of this rule goal directed + rbx0_input, // rax0 is based on (variable) input but is not a constant + rbx1_input)) // rax1 is based on (variable) input but is not a constant + ); + + // XOR RAX, RAX + solver.Assert(ctx.MkImplies( + ctx.MkAnd(switch_L1_XOR_RAX_RAX), + ctx.MkAnd(ctx.MkEq(rax1, zERO), + // rax0_goal is irelevant + rax1_goal, // make application of this rule goal directed + ctx.MkNot(rax0_input), // TODO: could this create inconsistencies with other instructions that updated rax!0 + ctx.MkNot(rax1_input))) // rax1 is not based on (variable) input but is a constant + ); + + // XOR RBX, RBX + solver.Assert(ctx.MkImplies( + ctx.MkAnd(switch_L1_XOR_RBX_RBX), + ctx.MkAnd(ctx.MkEq(rbx1, zERO), + // rbx0_goal is irelevant + rbx1_goal, // make application of this rule goal directed + ctx.MkNot(rbx0_input), // TODO: could this create inconsistencies with other instructions that updated rax!0 + ctx.MkNot(rbx1_input))) // rax1 is not based on (variable) input but is a constant + ); + + { // check INC RAX + solver.Push(); + solver.Assert(ctx.MkEq(rax1, ctx.MkBVAdd(rax0, ctx.MkBV(1, 64)))); + solver.Assert(rax0_input, rax1_goal); + + if (solver.Check(switch_L1_INC_RAX) == Status.UNSATISFIABLE) + { + Console.WriteLine("A: INC RAX: switch_INC SHOULD HAVE BEEN ALLOWED"); } - { // check XOR RAX, RAX - solver.Push(); - solver.Assert(ctx.MkEq(rax1, ctx.MkBV(0, 64))); - solver.Assert(ctx.MkNot(rax0_input)); - if (solver.Check(switch_L1_INC_RAX) == Status.SATISFIABLE) - { - Console.WriteLine("B: INC RAX: switch_INC SHOULD NOT HAVE BEEN ALLOWED"); - } + if (solver.Check(switch_L1_XOR_RAX_RAX) == Status.SATISFIABLE) + { + Console.WriteLine("A: XOR RAX, RAX: switch_XOR SHOULD NOT HAVE BEEN ALLOWED"); + } - if (solver.Check(switch_L1_XOR_RAX_RAX) == Status.UNSATISFIABLE) - { - Console.WriteLine("B: XOR RAX, RAX: switch_XOR SHOULD HAVE BEEN ALLOWED"); - } + solver.Pop(); + } + { // check XOR RAX, RAX + solver.Push(); + solver.Assert(ctx.MkEq(rax1, ctx.MkBV(0, 64))); + solver.Assert(ctx.MkNot(rax0_input)); - solver.Pop(); + if (solver.Check(switch_L1_INC_RAX) == Status.SATISFIABLE) + { + Console.WriteLine("B: INC RAX: switch_INC SHOULD NOT HAVE BEEN ALLOWED"); } - Console.WriteLine(string.Empty); - foreach (BoolExpr b in solver.Assertions) + if (solver.Check(switch_L1_XOR_RAX_RAX) == Status.UNSATISFIABLE) { - Console.WriteLine("Solver = " + b); + Console.WriteLine("B: XOR RAX, RAX: switch_XOR SHOULD HAVE BEEN ALLOWED"); } - Console.WriteLine(string.Empty); + solver.Pop(); + } - Status status = solver.Check(); - Console.WriteLine("Status = " + status + "\n"); - if (status == Status.SATISFIABLE) + Console.WriteLine(string.Empty); + foreach (BoolExpr b in solver.Assertions) + { + Console.WriteLine("Solver = " + b); + } + + Console.WriteLine(string.Empty); + + Status status = solver.Check(); + Console.WriteLine("Status = " + status + "\n"); + if (status == Status.SATISFIABLE) + { + foreach (FuncDecl f in solver.Model.ConstDecls) { - foreach (FuncDecl f in solver.Model.ConstDecls) - { - Console.WriteLine("Model: " + f.Name + " = " + solver.Model.ConstInterp(f)); - } + Console.WriteLine("Model: " + f.Name + " = " + solver.Model.ConstInterp(f)); } - else + } + else + { + foreach (BoolExpr b in solver.UnsatCore) { - foreach (BoolExpr b in solver.UnsatCore) - { - Console.WriteLine("Unsat: " + b); - } + Console.WriteLine("Unsat: " + b); } - Console.WriteLine(string.Empty); + } + Console.WriteLine(string.Empty); - /* + /* - (declare-const RAX!0 (_ BitVec 8)) - (declare-const RAX!1 (_ BitVec 8)) +(declare-const RAX!0 (_ BitVec 8)) +(declare-const RAX!1 (_ BitVec 8)) - (declare-const switch_inc bool) - (declare-const switch_xor_xor bool) +(declare-const switch_inc bool) +(declare-const switch_xor_xor bool) - (assert ((_ at-most 1) switch_inc switch_xor_xor)) - (assert (or switch_inc switch_xor_xor)) +(assert ((_ at-most 1) switch_inc switch_xor_xor)) +(assert (or switch_inc switch_xor_xor)) - (assert (=> switch_inc (= RAX!1 (bvadd RAX!0 #x01)))) - (assert (=> switch_xor_xor (= RAX!1 #x00))) +(assert (=> switch_inc (= RAX!1 (bvadd RAX!0 #x01)))) +(assert (=> switch_xor_xor (= RAX!1 #x00))) - ;(assert (= RAX!1 (bvadd RAX!0 #x01))) - (assert (forall ((RAX1 (_ BitVec 8))) (= RAX!1 (bvadd RAX!0 #x01)))) - (assert (not switch_inc)) +;(assert (= RAX!1 (bvadd RAX!0 #x01))) +(assert (forall ((RAX1 (_ BitVec 8))) (= RAX!1 (bvadd RAX!0 #x01)))) +(assert (not switch_inc)) - (check-sat) - (get-model) - */ - } +(check-sat) +(get-model) + */ } else { @@ -1709,186 +1690,182 @@ private static BoolExpr IsKnownTest(BitVecExpr reg, Context ctx) private static void TestFunctions() { - using (Context ctx = new Context()) + using Context ctx = new(); { - { - Solver solver1 = ctx.MkSolver(); - BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); - BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); + Solver solver1 = ctx.MkSolver(); + BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); + BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); - BitVecExpr var = ctx.MkBVConst("var", 64); - FuncDecl incFunc64 = ctx.MkFuncDecl("INC_64", ctx.MkBitVecSort(64), ctx.MkBitVecSort(64)); - solver1.Assert(ctx.MkQuantifier(true, new Expr[] { var }, ctx.MkEq(incFunc64.Apply(var), ctx.MkBVAdd(var, ctx.MkBV(1, 64))))); + BitVecExpr var = ctx.MkBVConst("var", 64); + FuncDecl incFunc64 = ctx.MkFuncDecl("INC_64", ctx.MkBitVecSort(64), ctx.MkBitVecSort(64)); + solver1.Assert(ctx.MkQuantifier(true, new Expr[] { var }, ctx.MkEq(incFunc64.Apply(var), ctx.MkBVAdd(var, ctx.MkBV(1, 64))))); - solver1.Assert(ctx.MkEq(rax0, ctx.MkBV(0, 64))); - solver1.Assert(ctx.MkEq(rax1, incFunc64.Apply(rax0))); + solver1.Assert(ctx.MkEq(rax0, ctx.MkBV(0, 64))); + solver1.Assert(ctx.MkEq(rax1, incFunc64.Apply(rax0))); - Console.WriteLine(solver1); - Console.WriteLine(ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rax1, 64, solver1, ctx))); - } - { - Solver solver2 = ctx.MkSolver(); - BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); - BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); + Console.WriteLine(solver1); + Console.WriteLine(ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rax1, 64, solver1, ctx))); + } + { + Solver solver2 = ctx.MkSolver(); + BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); + BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); - solver2.Assert(ctx.MkEq(rax0, ctx.MkBV(0, 64))); - solver2.Assert(ctx.MkEq(rax1, ctx.MkBVAdd(rax0, ctx.MkBV(1, 64)))); + solver2.Assert(ctx.MkEq(rax0, ctx.MkBV(0, 64))); + solver2.Assert(ctx.MkEq(rax1, ctx.MkBVAdd(rax0, ctx.MkBV(1, 64)))); - Console.WriteLine(solver2); - Console.WriteLine(ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rax1, 64, solver2, ctx))); - } + Console.WriteLine(solver2); + Console.WriteLine(ToolsZ3.ToStringBin(ToolsZ3.GetTvArray(rax1, 64, solver2, ctx))); } } private static void TacticTest() { - using (Context ctx = new Context()) + using Context ctx = new(); + if (false) { - if (false) + #region Doc + /* + tacticName ackermannize_bv: A tactic for performing full Ackermannization on bv instances. + tacticName subpaving: tactic for testing subpaving module. + tacticName horn: apply tactic for horn clauses. + tacticName horn-simplify: simplify horn clauses. + tacticName nlsat: (try to) solve goal using a nonlinear arithmetic solver. + tacticName qfnra-nlsat: builtin strategy for solving QF_NRA problems using only nlsat. + tacticName nlqsat: apply a NL-QSAT solver. + tacticName qe-light: apply light-weight quantifier elimination. + tacticName qe-sat: check satisfiability of quantified formulas using quantifier elimination. + tacticName qe: apply quantifier elimination. + tacticName qsat: apply a QSAT solver. + tacticName qe2: apply a QSAT based quantifier elimination. + tacticName qe_rec: apply a QSAT based quantifier elimination recursively. + tacticName vsubst: checks satsifiability of quantifier-free non-linear constraints using virtual substitution. + tacticName sat: (try to) solve goal using a SAT solver. + tacticName sat-preprocess: Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution). + tacticName ctx-solver-simplify: apply solver-based contextual simplification rules. + tacticName smt: apply a SAT based SMT solver. + tacticName unit-subsume-simplify: unit subsumption simplification. + tacticName aig: simplify Boolean structure using AIGs. + tacticName add-bounds: add bounds to unbounded variables (under approximation). + tacticName card2bv: convert pseudo-boolean constraints to bit-vectors. + tacticName degree-shift: try to reduce degree of polynomials (remark: :mul2power simplification is automatically applied). + tacticName diff-neq: specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numeral, and all constants are bounded. + tacticName elim01: eliminate 0-1 integer variables, replace them by Booleans. + tacticName eq2bv: convert integer variables used as finite domain elements to bit-vectors. + tacticName factor: polynomial factorization. + tacticName fix-dl-var: if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0. + tacticName fm: eliminate variables using fourier-motzkin elimination. + tacticName lia2card: introduce cardinality constraints from 0-1 integer. + tacticName lia2pb: convert bounded integer variables into a sequence of 0-1 variables. + tacticName nla2bv: convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models. + tacticName normalize-bounds: replace a variable x with lower bound k <= x with x' = x - k. + tacticName pb2bv: convert pseudo-boolean constraints to bit-vectors. + tacticName propagate-ineqs: propagate ineqs/bounds, remove subsumed inequalities. + tacticName purify-arith: eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects. + tacticName recover-01: recover 0-1 variables hidden as Boolean variables. + tacticName bit-blast: reduce bit-vector expressions into SAT. + tacticName bv1-blast: reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported). + tacticName bv_bound_chk: attempts to detect inconsistencies of bounds on bv expressions. + tacticName propagate-bv-bounds: propagate bit-vector bounds by simplifying implied or contradictory bounds. + tacticName reduce-bv-size: try to reduce bit-vector sizes using inequalities. + tacticName bvarray2uf: Rewrite bit-vector arrays into bit-vector (uninterpreted) functions. + tacticName dt2bv: eliminate finite domain data-types. Replace by bit-vectors. + tacticName elim-small-bv: eliminate small, quantified bit-vectors by expansion. + tacticName max-bv-sharing: use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers. + tacticName blast-term-ite: blast term if-then-else by hoisting them. + tacticName cofactor-term-ite: eliminate term if-the-else using cofactors. + tacticName collect-statistics: Collects various statistics. + tacticName ctx-simplify: apply contextual simplification rules. + tacticName der: destructive equality resolution. + tacticName distribute-forall: distribute forall over conjunctions. + tacticName elim-term-ite: eliminate term if-then-else by adding fresh auxiliary declarations. + tacticName elim-uncnstr: eliminate application containing unconstrained variables. + tacticName snf: put goal in skolem normal form. + tacticName nnf: put goal in negation normal form. + tacticName occf: put goal in one constraint per clause normal form (notes: fails if proof generation is enabled; only clauses are considered). + tacticName pb-preprocess: pre-process pseudo-Boolean constraints a la Davis Putnam. + tacticName propagate-values: propagate constants. + tacticName reduce-args: reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value. + tacticName simplify: apply simplification rules. + tacticName elim-and: convert (and a b) into (not (or (not a) (not b))). + tacticName solve-eqs: eliminate variables by solving equations. + tacticName split-clause: split a clause in many subgoals. + tacticName symmetry-reduce: apply symmetry reduction. + tacticName tseitin-cnf: convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). + tacticName tseitin-cnf-core: convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). This tactic does not apply required simplifications to the input goal like the tseitin-cnf tactic. + tacticName fpa2bv: convert floating point numbers to bit-vectors. + tacticName qffp: (try to) solve goal using the tactic for QF_FP. + tacticName qffpbv: (try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors). + tacticName nl-purify: Decompose goal into pure NL-sat formula and formula over other theories. + tacticName default: default strategy used when no logic is specified. + tacticName qfbv-sls: (try to) solve using stochastic local search for QF_BV. + tacticName nra: builtin strategy for solving NRA problems. + tacticName qfaufbv: builtin strategy for solving QF_AUFBV problems. + tacticName qfauflia: builtin strategy for solving QF_AUFLIA problems. + tacticName qfbv: builtin strategy for solving QF_BV problems. + tacticName qfidl: builtin strategy for solving QF_IDL problems. + tacticName qflia: builtin strategy for solving QF_LIA problems. + tacticName qflra: builtin strategy for solving QF_LRA problems. + tacticName qfnia: builtin strategy for solving QF_NIA problems. + tacticName qfnra: builtin strategy for solving QF_NRA problems. + tacticName qfuf: builtin strategy for solving QF_UF problems. + tacticName qfufbv: builtin strategy for solving QF_UFBV problems. + tacticName qfufbv_ackr: A tactic for solving QF_UFBV based on Ackermannization. + tacticName qfufnra: builtin strategy for solving QF_UNFRA problems. + tacticName ufnia: builtin strategy for solving UFNIA problems. + tacticName uflra: builtin strategy for solving UFLRA problems. + tacticName auflia: builtin strategy for solving AUFLIA problems. + tacticName auflira: builtin strategy for solving AUFLIRA problems. + tacticName aufnira: builtin strategy for solving AUFNIRA problems. + tacticName lra: builtin strategy for solving LRA problems. + tacticName lia: builtin strategy for solving LIA problems. + tacticName lira: builtin strategy for solving LIRA problems. + tacticName skip: do nothing tactic. + tacticName fail: always fail tactic. + tacticName fail-if-undecided: fail if goal is undecided. + tacticName macro-finder: Identifies and applies macros. + tacticName quasi-macros: Identifies and applies quasi-macros. + tacticName ufbv-rewriter: Applies UFBV-specific rewriting rules, mainly demodulation. + tacticName bv: builtin strategy for solving BV problems (with quantifiers). + tacticName ufbv: builtin strategy for solving UFBV problems (with quantifiers). + */ + #endregion + foreach (string tacticName in ctx.TacticNames) { - #region Doc - /* - tacticName ackermannize_bv: A tactic for performing full Ackermannization on bv instances. - tacticName subpaving: tactic for testing subpaving module. - tacticName horn: apply tactic for horn clauses. - tacticName horn-simplify: simplify horn clauses. - tacticName nlsat: (try to) solve goal using a nonlinear arithmetic solver. - tacticName qfnra-nlsat: builtin strategy for solving QF_NRA problems using only nlsat. - tacticName nlqsat: apply a NL-QSAT solver. - tacticName qe-light: apply light-weight quantifier elimination. - tacticName qe-sat: check satisfiability of quantified formulas using quantifier elimination. - tacticName qe: apply quantifier elimination. - tacticName qsat: apply a QSAT solver. - tacticName qe2: apply a QSAT based quantifier elimination. - tacticName qe_rec: apply a QSAT based quantifier elimination recursively. - tacticName vsubst: checks satsifiability of quantifier-free non-linear constraints using virtual substitution. - tacticName sat: (try to) solve goal using a SAT solver. - tacticName sat-preprocess: Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution). - tacticName ctx-solver-simplify: apply solver-based contextual simplification rules. - tacticName smt: apply a SAT based SMT solver. - tacticName unit-subsume-simplify: unit subsumption simplification. - tacticName aig: simplify Boolean structure using AIGs. - tacticName add-bounds: add bounds to unbounded variables (under approximation). - tacticName card2bv: convert pseudo-boolean constraints to bit-vectors. - tacticName degree-shift: try to reduce degree of polynomials (remark: :mul2power simplification is automatically applied). - tacticName diff-neq: specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numeral, and all constants are bounded. - tacticName elim01: eliminate 0-1 integer variables, replace them by Booleans. - tacticName eq2bv: convert integer variables used as finite domain elements to bit-vectors. - tacticName factor: polynomial factorization. - tacticName fix-dl-var: if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0. - tacticName fm: eliminate variables using fourier-motzkin elimination. - tacticName lia2card: introduce cardinality constraints from 0-1 integer. - tacticName lia2pb: convert bounded integer variables into a sequence of 0-1 variables. - tacticName nla2bv: convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models. - tacticName normalize-bounds: replace a variable x with lower bound k <= x with x' = x - k. - tacticName pb2bv: convert pseudo-boolean constraints to bit-vectors. - tacticName propagate-ineqs: propagate ineqs/bounds, remove subsumed inequalities. - tacticName purify-arith: eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects. - tacticName recover-01: recover 0-1 variables hidden as Boolean variables. - tacticName bit-blast: reduce bit-vector expressions into SAT. - tacticName bv1-blast: reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported). - tacticName bv_bound_chk: attempts to detect inconsistencies of bounds on bv expressions. - tacticName propagate-bv-bounds: propagate bit-vector bounds by simplifying implied or contradictory bounds. - tacticName reduce-bv-size: try to reduce bit-vector sizes using inequalities. - tacticName bvarray2uf: Rewrite bit-vector arrays into bit-vector (uninterpreted) functions. - tacticName dt2bv: eliminate finite domain data-types. Replace by bit-vectors. - tacticName elim-small-bv: eliminate small, quantified bit-vectors by expansion. - tacticName max-bv-sharing: use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers. - tacticName blast-term-ite: blast term if-then-else by hoisting them. - tacticName cofactor-term-ite: eliminate term if-the-else using cofactors. - tacticName collect-statistics: Collects various statistics. - tacticName ctx-simplify: apply contextual simplification rules. - tacticName der: destructive equality resolution. - tacticName distribute-forall: distribute forall over conjunctions. - tacticName elim-term-ite: eliminate term if-then-else by adding fresh auxiliary declarations. - tacticName elim-uncnstr: eliminate application containing unconstrained variables. - tacticName snf: put goal in skolem normal form. - tacticName nnf: put goal in negation normal form. - tacticName occf: put goal in one constraint per clause normal form (notes: fails if proof generation is enabled; only clauses are considered). - tacticName pb-preprocess: pre-process pseudo-Boolean constraints a la Davis Putnam. - tacticName propagate-values: propagate constants. - tacticName reduce-args: reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value. - tacticName simplify: apply simplification rules. - tacticName elim-and: convert (and a b) into (not (or (not a) (not b))). - tacticName solve-eqs: eliminate variables by solving equations. - tacticName split-clause: split a clause in many subgoals. - tacticName symmetry-reduce: apply symmetry reduction. - tacticName tseitin-cnf: convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). - tacticName tseitin-cnf-core: convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). This tactic does not apply required simplifications to the input goal like the tseitin-cnf tactic. - tacticName fpa2bv: convert floating point numbers to bit-vectors. - tacticName qffp: (try to) solve goal using the tactic for QF_FP. - tacticName qffpbv: (try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors). - tacticName nl-purify: Decompose goal into pure NL-sat formula and formula over other theories. - tacticName default: default strategy used when no logic is specified. - tacticName qfbv-sls: (try to) solve using stochastic local search for QF_BV. - tacticName nra: builtin strategy for solving NRA problems. - tacticName qfaufbv: builtin strategy for solving QF_AUFBV problems. - tacticName qfauflia: builtin strategy for solving QF_AUFLIA problems. - tacticName qfbv: builtin strategy for solving QF_BV problems. - tacticName qfidl: builtin strategy for solving QF_IDL problems. - tacticName qflia: builtin strategy for solving QF_LIA problems. - tacticName qflra: builtin strategy for solving QF_LRA problems. - tacticName qfnia: builtin strategy for solving QF_NIA problems. - tacticName qfnra: builtin strategy for solving QF_NRA problems. - tacticName qfuf: builtin strategy for solving QF_UF problems. - tacticName qfufbv: builtin strategy for solving QF_UFBV problems. - tacticName qfufbv_ackr: A tactic for solving QF_UFBV based on Ackermannization. - tacticName qfufnra: builtin strategy for solving QF_UNFRA problems. - tacticName ufnia: builtin strategy for solving UFNIA problems. - tacticName uflra: builtin strategy for solving UFLRA problems. - tacticName auflia: builtin strategy for solving AUFLIA problems. - tacticName auflira: builtin strategy for solving AUFLIRA problems. - tacticName aufnira: builtin strategy for solving AUFNIRA problems. - tacticName lra: builtin strategy for solving LRA problems. - tacticName lia: builtin strategy for solving LIA problems. - tacticName lira: builtin strategy for solving LIRA problems. - tacticName skip: do nothing tactic. - tacticName fail: always fail tactic. - tacticName fail-if-undecided: fail if goal is undecided. - tacticName macro-finder: Identifies and applies macros. - tacticName quasi-macros: Identifies and applies quasi-macros. - tacticName ufbv-rewriter: Applies UFBV-specific rewriting rules, mainly demodulation. - tacticName bv: builtin strategy for solving BV problems (with quantifiers). - tacticName ufbv: builtin strategy for solving UFBV problems (with quantifiers). - */ - #endregion - foreach (string tacticName in ctx.TacticNames) - { - Console.WriteLine("tacticName " + tacticName + ": " + ctx.TacticDescription(tacticName)); - } + Console.WriteLine("tacticName " + tacticName + ": " + ctx.TacticDescription(tacticName)); } + } - Tactic tactic3 = ctx.MkTactic("propagate-values"); - Solver solver = ctx.MkSolver(tactic3); + Tactic tactic3 = ctx.MkTactic("propagate-values"); + Solver solver = ctx.MkSolver(tactic3); - BitVecExpr rax = ctx.MkBVConst("RAX", 64); - BitVecExpr rbx = ctx.MkBVConst("RBX", 64); - BitVecExpr rcx = ctx.MkBVConst("RCX", 64); - BitVecExpr rdx = ctx.MkBVConst("RDX", 64); + BitVecExpr rax = ctx.MkBVConst("RAX", 64); + BitVecExpr rbx = ctx.MkBVConst("RBX", 64); + BitVecExpr rcx = ctx.MkBVConst("RCX", 64); + BitVecExpr rdx = ctx.MkBVConst("RDX", 64); - BitVecExpr zero_64 = ctx.MkBV(0, 64); + BitVecExpr zero_64 = ctx.MkBV(0, 64); - BoolExpr fact1 = ctx.MkEq(rax, zero_64); - BoolExpr fact2 = ctx.MkEq(rbx, ctx.MkITE(ctx.MkEq(rax, zero_64), rcx, rdx)); + BoolExpr fact1 = ctx.MkEq(rax, zero_64); + BoolExpr fact2 = ctx.MkEq(rbx, ctx.MkITE(ctx.MkEq(rax, zero_64), rcx, rdx)); - if (false) - { - solver.Assert(fact1, fact2); - } - else - { - Goal goal1 = ctx.MkGoal(); - goal1.Assert(fact1, fact2); - ApplyResult ar = tactic3.Apply(goal1); - solver.Assert(ar.Subgoals[0].Formulas); - } - Console.WriteLine(solver.ToString()); + if (false) + { + solver.Assert(fact1, fact2); + } + else + { + Goal goal1 = ctx.MkGoal(); + goal1.Assert(fact1, fact2); + ApplyResult ar = tactic3.Apply(goal1); + solver.Assert(ar.Subgoals[0].Formulas); } + Console.WriteLine(solver.ToString()); } private static void TestMemoryLeak() { - Dictionary settings = new Dictionary + Dictionary settings = new() { { "unsat-core", "false" }, // enable generation of unsat cores { "model", "false" }, // enable model generation @@ -1901,30 +1878,26 @@ private static void TestMemoryLeak() for (int i = 0; i < nContexts; ++i) { - using (Context ctx = new Context(settings)) - using (Solver s = ctx.MkSolver()) + using Context ctx = new(settings); + using Solver s = ctx.MkSolver(); + // ctxArray[i] = ctx; + + using BitVecExpr rax = ctx.MkBVConst("RAX!0", 64); + using BitVecExpr rbx = ctx.MkBVConst("RBX!0", 64); + using BitVecExpr rcx = ctx.MkBVConst("RCX!0", 64); + using (BoolExpr t = ctx.MkEq(rax, rbx)) { - // ctxArray[i] = ctx; + s.Assert(t); + } - using (BitVecExpr rax = ctx.MkBVConst("RAX!0", 64)) - using (BitVecExpr rbx = ctx.MkBVConst("RBX!0", 64)) - using (BitVecExpr rcx = ctx.MkBVConst("RCX!0", 64)) - { - using (BoolExpr t = ctx.MkEq(rax, rbx)) - { - s.Assert(t); - } - - using (BoolExpr t = ctx.MkEq(rbx, rcx)) - { - s.Assert(t); - } - - using (BoolExpr t = ctx.MkEq(rax, rcx)) - { - Console.WriteLine("i=" + i + ":" + ToolsZ3.GetTv(t, s, ctx)); - } - } + using (BoolExpr t = ctx.MkEq(rbx, rcx)) + { + s.Assert(t); + } + + using (BoolExpr t = ctx.MkEq(rax, rcx)) + { + Console.WriteLine("i=" + i + ":" + ToolsZ3.GetTv(t, s, ctx)); } // System.GC.Collect(); }