diff options
| author |  qadeer <unknown> | 2014-02-28 14:40:40 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-28 14:40:40 -0800 |
| commit | c77f823f177067df9810896fca015fc77a16d5ab (patch) | |
| tree | e5f0a7a2a3734ae36731c49e8e65db055eb8995b /Source | |
| parent | ec8ae543ef620954673f3731bec3a31ab69887df (diff) | |
Added /trustNonInterference option
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 45 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 2 |
2 files changed, 26 insertions, 21 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 786df939..6c78f80d 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -268,35 +268,38 @@ namespace Microsoft.Boogie private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
{
- List<Expr> exprSeq = new List<Expr>();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
- }
- foreach (IdentifierExpr ie in globalMods)
+ if (!CommandLineOptions.Clo.TrustNonInterference)
{
- exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
- }
- if (yieldProc == null)
- {
- List<Variable> inputs = new List<Variable>();
+ List<Expr> exprSeq = new List<Expr>();
foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- var domain = linearTypeChecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
- inputs.Add(f);
+ exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
}
foreach (IdentifierExpr ie in globalMods)
{
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
- inputs.Add(f);
+ exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
+ }
+ if (yieldProc == null)
+ {
+ List<Variable> inputs = new List<Variable>();
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ var domain = linearTypeChecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ inputs.Add(f);
+ }
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
+ inputs.Add(f);
+ }
+ yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
+ yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
}
- yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
+ yieldCallCmd.Proc = yieldProc;
+ newCmds.Add(yieldCallCmd);
}
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
- yieldCallCmd.Proc = yieldProc;
- newCmds.Add(yieldCallCmd);
if (pc != null)
{
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 70729f68..e6f467c8 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -489,6 +489,7 @@ namespace Microsoft.Boogie { public string OwickiGriesDesugaredOutputFile = null;
public bool TrustAtomicityTypes = false;
+ public bool TrustNonInterference = false;
public int TrustPhasesUpto = -1;
public int TrustPhasesDownto = int.MaxValue;
@@ -1392,6 +1393,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||
ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||
ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||
+ ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||
ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false)
) {
// one of the boolean flags matched
|