Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update boogie version #31

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Update boogie version #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
5b6371e
update boogie proj versions
typerSniper Dec 16, 2024
9339b82
update wrapper to call verify impl
typerSniper Dec 16, 2024
845331e
dependency/ errors
typerSniper Dec 16, 2024
89373b8
rootause/ folder
typerSniper Dec 16, 2024
94e6a16
symdiff/source
typerSniper Dec 16, 2024
09edee0
utils/*
typerSniper Dec 16, 2024
d2bfcc9
blovkOutliner commit review
typerSniper Dec 16, 2024
f1ed5d9
loop extractor please review
typerSniper Dec 16, 2024
0e4f32d
symdiff/sources/
typerSniper Dec 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions Sources/BoogieWrapper/BoogieWrapper.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,13 +36,13 @@
<OutputPath>../bin/</OutputPath>
</PropertyGroup>
<ItemGroup>
<PackageReference Include="Boogie.BaseTypes" Version="3.1.3" />
<PackageReference Include="Boogie.CodeContractsExtender" Version="3.1.3" />
<PackageReference Include="Boogie.Core" Version="3.1.3" />
<PackageReference Include="Boogie.Model" Version="3.1.3" />
<PackageReference Include="Boogie.Provers.SMTLib" Version="3.1.3" />
<PackageReference Include="Boogie.VCExpr" Version="3.1.3" />
<PackageReference Include="Boogie.VCGeneration" Version="3.1.3" />
<PackageReference Include="Boogie.BaseTypes" Version="3.4.3" />
<PackageReference Include="Boogie.CodeContractsExtender" Version="3.4.3" />
<PackageReference Include="Boogie.Core" Version="3.4.3" />
<PackageReference Include="Boogie.Model" Version="3.4.3" />
<PackageReference Include="Boogie.Provers.SMTLib" Version="3.4.3" />
<PackageReference Include="Boogie.VCExpr" Version="3.4.3" />
<PackageReference Include="Boogie.VCGeneration" Version="3.4.3" />
</ItemGroup>
<ItemGroup>
<Compile Update="Properties\Resources.Designer.cs">
Expand Down
18 changes: 7 additions & 11 deletions Sources/BoogieWrapper/source/Wrapper.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,16 +61,12 @@ static int Main(string[] args)
}

var newProg = prog;

VC.ConditionGeneration vcgen = BoogieVerify.InitializeVC(newProg);
SDiffCounterexamples SErrors;
List<Model> errModelList;
var Result = BoogieVerify.VerifyImplementation(newProg, fileName, funcName, out SErrors);
var newDict = SDiff.Boogie.Process.BuildProgramDictionary(newProg.TopLevelDeclarations.ToList());

//RS: Uncomment this
var newEq = (Implementation)newDict.Get(funcName + "$IMPL");
SDiffCounterexamples SErrors;
List<Model> errModelList;

var Result = BoogieVerify.VerifyImplementation(vcgen, newEq, newProg, out SErrors);

switch (Result)
{
Expand Down Expand Up @@ -117,7 +113,7 @@ static int Main(string[] args)
}
if (Options.DoSymEx)
{

if (Options.PreciseDifferentialInline)
{
IEnumerable <Declaration> consts = prog.TopLevelDeclarations.Where(x => x is Constant);
Expand All @@ -132,14 +128,14 @@ static int Main(string[] args)
}
}
}

return (SErrors == null ? 0 : SErrors.Count);

}
private static void GetImplementations(Dictionary<string, Declaration> newDict, string funcName, out Implementation n1, out Implementation n2,string n1name, string n2name)
{
n1 = (Implementation)newDict.Get(n1name + "$IMPL");
n2 = (Implementation)newDict.Get(n1name + "$IMPL");
n2 = (Implementation)newDict.Get(n1name + "$IMPL");
}

public class BvdInstrument : FixedVisitor
Expand All @@ -151,7 +147,7 @@ public override Block VisitBlock(Block b)
foreach (Cmd c in b.Cmds)
{
cmds.Add(c);
if ((c is CallCmd) || (c is AssignCmd) || (c is HavocCmd) ||
if ((c is CallCmd) || (c is AssignCmd) || (c is HavocCmd) ||
(c is AssumeCmd && ((AssumeCmd)c).Attributes == null) ||
(c is AssertCmd && ((AssertCmd)c).Attributes == null))
{ //some asserts/assumes have string attributes
Expand Down
14 changes: 7 additions & 7 deletions Sources/Dependency/Dependency.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,13 +49,13 @@
</ItemGroup>
<ItemGroup>
<PackageReference Include="Microsoft.CSharp" Version="4.7.0" />
<PackageReference Include="Boogie.Core" Version="3.1.3" />
<PackageReference Include="Boogie.Houdini" Version="3.1.3" />
<PackageReference Include="Boogie.Graph" Version="3.1.3" />
<PackageReference Include="Boogie.Model" Version="3.1.3" />
<PackageReference Include="Boogie.Provers.SMTLib" Version="3.1.3" />
<PackageReference Include="Boogie.VCExpr" Version="3.1.3" />
<PackageReference Include="Boogie.VCGeneration" Version="3.1.3" />
<PackageReference Include="Boogie.Core" Version="3.4.3" />
<PackageReference Include="Boogie.Houdini" Version="3.4.3" />
<PackageReference Include="Boogie.Graph" Version="3.4.3" />
<PackageReference Include="Boogie.Model" Version="3.4.3" />
<PackageReference Include="Boogie.Provers.SMTLib" Version="3.4.3" />
<PackageReference Include="Boogie.VCExpr" Version="3.4.3" />
<PackageReference Include="Boogie.VCGeneration" Version="3.4.3" />
</ItemGroup>
<ItemGroup>
<Compile Remove="source\TaintVisitor.cs" />
Expand Down
26 changes: 13 additions & 13 deletions Sources/Dependency/source/DependencyVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
using SymDiffUtils;

namespace Dependency
{
{
public class RefineDependencyWL
{
private string filename;
Expand Down Expand Up @@ -355,7 +355,7 @@ public override GotoCmd VisitGotoCmd(GotoCmd node)
Block currBlock = worklist.cmdBlocks[node];
Dependencies dependencies = worklist.GatherPredecessorsState(node, currBlock);

var succs = node.labelTargets;
var succs = node.LabelTargets;
if (succs.Count > 1)
{ // here we create branchCondVars
if (!branchCondVars.ContainsKey(currBlock))
Expand All @@ -380,7 +380,7 @@ public override Cmd VisitAssignCmd(AssignCmd node)
{
//TODO: M := M[p := v]; -> p is LHS!
//if (node.Rhss[i].Type.IsMap)

//MAJOR BUG FIX M[N[y] + z] := T[4];
var lhs = node.Lhss[i].DeepAssignedVariable;
var rhsVars = Utils.VariableUtils.ExtractVars(node.Rhss[i]);
Expand Down Expand Up @@ -408,7 +408,7 @@ public override Cmd VisitAssignCmd(AssignCmd node)
dependencies[lhs].RemoveWhere(v => v != Utils.VariableUtils.BottomUpTaintVar && v != Utils.VariableUtils.TopDownTaintVar);

if (changedProcs.Contains(nodeToImpl[node].Proc) || changedBlocks.Contains(currBlock)) // native taint
{
{
if (Analysis.DacMerged == null || IsImpactedSummary(nodeToImpl[node].Proc, lhs))
{
dependencies[lhs].Add(Utils.VariableUtils.BottomUpTaintVar);
Expand Down Expand Up @@ -442,7 +442,7 @@ public void InferDominatorDependency(Block currBlock, VarSet dependsSet)
}
}

private Dictionary<Procedure, Dictionary<string, int>> paramNameToIndex = new Dictionary<Procedure, Dictionary<string, int>>();
private Dictionary<Procedure, Dictionary<string, int>> paramNameToIndex = new Dictionary<Procedure, Dictionary<string, int>>();
private VarSet InferCalleeOutputDependancy(CallCmd cmd, Variable output, Dependencies state, List<VarSet> inputExpressionsDependency)
{
if (Analysis.DacMerged != null && !IsImpactedOutput(cmd.Proc, output))
Expand Down Expand Up @@ -527,7 +527,7 @@ public override Cmd VisitCallCmd(CallCmd node)
{
topDownTaint[input] = new VarSet();
if(Analysis.DacMerged == null || IsImpactedInput(callee, input))
{
{
topDownTaint[input].Add(Utils.VariableUtils.TopDownTaintVar);
}
}
Expand All @@ -552,7 +552,7 @@ public override Cmd VisitCallCmd(CallCmd node)
var input = calleeImpl.InParams[i];
topDownTaint[input] = new VarSet();
if (Analysis.DacMerged == null || IsImpactedInput(calleeImpl.Proc, input))
{
{
topDownTaint[input].Add(Utils.VariableUtils.TopDownTaintVar);
}
}
Expand All @@ -564,10 +564,10 @@ public override Cmd VisitCallCmd(CallCmd node)
{
if (calleeImpl != null && // not a stub
Utils.VariableUtils.IsTainted(dependencies[g]))
{ // top down taint from global
{ // top down taint from global
topDownTaint[g] = new VarSet();
if (Analysis.DacMerged == null || IsImpactedInput(calleeImpl.Proc, g))
{
{
topDownTaint[g].Add(Utils.VariableUtils.TopDownTaintVar);
}
}
Expand Down Expand Up @@ -652,9 +652,9 @@ public override ReturnCmd VisitReturnCmd(ReturnCmd node)
dep.Value.Remove(Utils.VariableUtils.TopDownTaintVar);
procExitTDTaint[proc][dep.Key] = new VarSet();
if (Analysis.DacMerged == null || (IsImpactedInput(proc, dep.Key) && IsImpactedOutput(proc, dep.Key)))
{
{
procExitTDTaint[proc][dep.Key].Add(Utils.VariableUtils.TopDownTaintVar);

}
});
// Remove taint based on DAC
Expand Down Expand Up @@ -732,8 +732,8 @@ public override Procedure VisitProcedure(Procedure node)
{
AddTaintedInputs(node);
AddTaintedOutputs(node);
}
}

return base.VisitProcedure(node);
}

Expand Down
8 changes: 4 additions & 4 deletions Sources/Dependency/source/TaintVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ public BottomUpTaintVisitor(string filename, Program program, Dictionary<Procedu
else foreach (var procChange in changesPerProc)
{
// add in the block pertaining to the changed line
impl.Blocks.Where(b => b.Cmds.Count > 0 &&
b.Cmds[0] is AssertCmd &&
impl.Blocks.Where(b => b.Cmds.Count > 0 &&
b.Cmds[0] is AssertCmd &&
Utils.AttributeUtils.GetSourceLine(b.Cmds[0] as AssertCmd) == procChange.Item3)
.Iter(b => changedBlocks.Add(b));
}
Expand Down Expand Up @@ -95,7 +95,7 @@ private bool InferDominatorTaint(Block block)
foreach (var dominator in dominatedBy[block])
if (branchCondVars.ContainsKey(dominator))
{
// assignment under a branch is tainted if any the variables in the
// assignment under a branch is tainted if any the variables in the
// branch conditional are tainted, *at the point of branching*
var domTaint = worklist.stateSpace[dominator.TransferCmd];
if (branchCondVars[dominator].Intersect(domTaint).Count() > 0)
Expand Down Expand Up @@ -225,7 +225,7 @@ public override GotoCmd VisitGotoCmd(GotoCmd node)
Block currBlock = worklist.cmdBlocks[node];
var taintSet = worklist.GatherPredecessorsState(node, currBlock);

var succs = node.labelTargets;
var succs = node.LabelTargets;
if (succs.Count > 1)
{ // here we create branchCondVars
if (!branchCondVars.ContainsKey(currBlock))
Expand Down
Loading