From d5890371c7ba71af00cced2376009e0fb966a56a Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 7 Sep 2013 00:17:10 -0700 Subject: fixed the problem with codexprs now positive/negative context is detected and appropriate translation is done --- Source/VCExpr/Boogie2VCExpr.cs | 34 +++++++++++++++++++++++++++++++--- Source/VCGeneration/VC.cs | 27 ++++++++++----------------- Source/VCGeneration/Wlp.cs | 27 ++++++++++----------------- 3 files changed, 51 insertions(+), 37 deletions(-) (limited to 'Source') diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index e4101d49..c5c61546 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST { } } - public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/**//*!*/ blockVariables, List bindings, bool isAssumeContext); + public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/**//*!*/ blockVariables, List bindings, bool isPositiveContext); public class Boogie2VCExprTranslator : StandardVisitor, ICloneable { // Stack on which the various Visit-methods put the result of the translation @@ -375,13 +375,42 @@ namespace Microsoft.Boogie.VCExprAST { return node; } + public bool isPositiveContext = true; private VCExpr TranslateNAryExpr(NAryExpr node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); + + bool flipContextForArg0 = false; + if (node.Fun is UnaryOperator) + { + UnaryOperator oper = (UnaryOperator)node.Fun; + if (oper.Op == UnaryOperator.Opcode.Neg) + flipContextForArg0 = true; + } + else if (node.Fun is BinaryOperator) + { + BinaryOperator oper = (BinaryOperator)node.Fun; + if (oper.Op == BinaryOperator.Opcode.Imp) + flipContextForArg0 = true; + else if (oper.Op == BinaryOperator.Opcode.Iff) { + Expr one = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List { node.Args[0], node.Args[1] }); + Expr two = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List { node.Args[1], node.Args[0] }); + NAryExpr cmpd = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.And), new List { one, two }); + TypecheckingContext tc = new TypecheckingContext(null); + cmpd.Typecheck(tc); + return TranslateNAryExpr(cmpd); + } + } + int n = node.Args.Count; List/*!*/ vcs = new List(n); + for (int i = 0; i < n; i++) { + if (i == 0 && flipContextForArg0) + isPositiveContext = !isPositiveContext; vcs.Add(Translate(cce.NonNull(node.Args)[i])); + if (i == 0 && flipContextForArg0) + isPositiveContext = !isPositiveContext; } if (node.Type == null) { @@ -618,12 +647,11 @@ namespace Microsoft.Boogie.VCExprAST { public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) { //Contract.Requires(codeExpr != null); Contract.Ensures(Contract.Result() != null); - Contract.Assume(codeExprConverter != null); Hashtable/**/ blockVariables = new Hashtable/**/(); List bindings = new List(); - VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, false); + VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, isPositiveContext); Push(e); return codeExpr; } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 7cd9f9c2..ca74c1d2 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1345,7 +1345,7 @@ namespace VC { this.ctx = ctx; } - public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List bindings, bool isAssumeContext) + public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List bindings, bool isPositiveContext) { VCGen vcgen = new VCGen(new Program(), null, false, new List()); vcgen.variable2SequenceNumber = new Dictionary(); @@ -1356,12 +1356,8 @@ namespace VC { vcgen.AddBlocksBetween(codeExpr.Blocks); Dictionary gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List(), new ModelViewInfo(codeExpr)); int ac; // computed, but then ignored for this CodeExpr - VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isAssumeContext); + VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isPositiveContext); VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect); - if (isAssumeContext) - { - vce = ctx.ExprGen.Not(vce); - } if (vcgen.CurrentLocalVariables.Count != 0) { Boogie2VCExprTranslator translator = ctx.BoogieExprTranslator; @@ -1378,15 +1374,12 @@ namespace VC { vce = ctx.ExprGen.Implies(ctx.ExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce); } } - if (isAssumeContext) - { - vce = ctx.ExprGen.Exists(boundVars, new List(), vce); - } - else - { - vce = ctx.ExprGen.Forall(boundVars, new List(), vce); - } + vce = ctx.ExprGen.Forall(boundVars, new List(), vce); } + if (isPositiveContext) + { + vce = ctx.ExprGen.Not(vce); + } return vce; } } @@ -2717,7 +2710,7 @@ namespace VC { Dictionary label2absy, ProverContext proverCtxt, out int assertionCount, - bool isAssumeContext = false) + bool isPositiveContext = true) { Contract.Requires(blocks != null); Contract.Requires(proverCtxt != null); @@ -2755,7 +2748,7 @@ namespace VC { else { SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr); } - if (isAssumeContext) + if (isPositiveContext) { SuccCorrect = gen.Not(SuccCorrect); } @@ -2776,7 +2769,7 @@ namespace VC { SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); } - VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr); + VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext); VCExpr vc = Wlp.Block(block, SuccCorrect, context); assertionCount += context.AssertionCount; diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index b1e69c38..bb2a2785 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -24,22 +24,24 @@ namespace VC { [Rep] public readonly ProverContext Ctxt; public readonly VCExpr ControlFlowVariableExpr; public int AssertionCount; // counts the number of assertions for which Wlp has been computed - - public VCContext(Dictionary label2absy, ProverContext ctxt) + public bool isPositiveContext; + + public VCContext(Dictionary label2absy, ProverContext ctxt, bool isPositiveContext = true) { Contract.Requires(ctxt != null); this.Label2absy = label2absy; this.Ctxt = ctxt; + this.isPositiveContext = isPositiveContext; } - - public VCContext(Dictionary label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr) + + public VCContext(Dictionary label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr, bool isPositiveContext = true) { Contract.Requires(ctxt != null); this.Label2absy = label2absy; this.Ctxt = ctxt; this.ControlFlowVariableExpr = controlFlowVariableExpr; + this.isPositiveContext = isPositiveContext; } - } #region A class to compute wlp of a passive command program @@ -95,7 +97,9 @@ namespace VC { Contract.Assert(gen != null); if (cmd is AssertCmd) { AssertCmd ac = (AssertCmd)cmd; + ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); + ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { return gen.Implies(C, N); } else { @@ -159,18 +163,7 @@ namespace VC { } } } - - CodeExpr codeExpr = ac.Expr as CodeExpr; - if (codeExpr != null) - { - Hashtable blockVariables = new Hashtable(); - List bindings = new List(); - return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.codeExprConverter(codeExpr, blockVariables, bindings, true), N); - } - else - { - return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N); - } + return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N); } else { Console.WriteLine(cmd.ToString()); Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command -- cgit v1.2.3