VC gen for security properties

4 files changed, 392 insertions, 7 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index bbdccda9..dbbb6fd0 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -746,6 +746,7 @@ namespace Microsoft.Boogie {
     public bool PrintInlined = false;

     public bool ExtractLoops = false;

     public bool DeterministicExtractLoops = false;

+    public string SecureVcGen = null;

     public int StratifiedInlining = 0;

     public string FixedPointEngine = null;

     public int StratifiedInliningOption = 0;

@@ -1251,7 +1252,10 @@ namespace Microsoft.Boogie {
             }

           }

           return true;

-

+        case "secure":

+          if (ps.ConfirmArgumentCount(1))

+              SecureVcGen = args[ps.i];

+          return true;

         case "stratifiedInline":

           if (ps.ConfirmArgumentCount(1)) {

             switch (args[ps.i]) {

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 7756973d..31a69c6e 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1060,6 +1060,9 @@ namespace Microsoft.Boogie
 

       #endregion

 

+      if (SecureVCGen.outfile != null)

+          SecureVCGen.outfile.Close();

+

       return outcome;

     }

 

@@ -1290,9 +1293,13 @@ namespace Microsoft.Boogie
       {

         vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

       }

+      else if (CommandLineOptions.Clo.SecureVcGen != null)

+      {

+          vcgen = new SecureVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

+      }

       else

       {

-        vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

+          vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

       }

       return vcgen;

     }

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index a62fa25a..868b9ee3 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -74,7 +74,8 @@ namespace Microsoft.Boogie.SMTLib
 

       SetupProcess();

 

-      if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)

+      if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer

+          || CommandLineOptions.Clo.SecureVcGen != null)

       {

           // Prepare for ApiChecker usage

           if (options.LogFilename != null && currentLogFile == null)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 88577e46..6f8d3668 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2094,10 +2094,7 @@ namespace VC {
 

     } // end FCallInliner

 

-    public class EmptyErrorHandler : ProverInterface.ErrorHandler {

-        public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)

-        { }

-    }

+

 

     public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {

       Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

@@ -2538,4 +2535,380 @@ namespace VC {
 

   } // class StratifiedVCGen

 

+  public class EmptyErrorHandler : ProverInterface.ErrorHandler

+  {

+      public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)

+      { }

+  }

+

+  public class InvalidProgramForSecureVc : Exception

+  {

+      public InvalidProgramForSecureVc(string msg) :

+          base(msg) { }

+  }

+

+  public class SecureVCGen : VCGen

+  {

+      // Z3

+      ProverInterface prover;

+      // Handler

+      ErrorReporter handler;

+      // dump file

+      public static TokenTextWriter outfile = null;

+

+

+      public SecureVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+          : base(program, logFilePath, appendLogFile, checkers)

+      {

+          prover = null;

+          handler = null;

+          if (CommandLineOptions.Clo.SecureVcGen != "" && outfile == null)

+          {

+              outfile = new TokenTextWriter(new StreamWriter(CommandLineOptions.Clo.SecureVcGen));

+              CommandLineOptions.Clo.PrintInstrumented = true;

+              var implsToVerify = new HashSet<string>(

+                  program.TopLevelDeclarations.OfType<Implementation>()

+                  .Where(impl => !impl.SkipVerification)

+                  .Select(impl => impl.Name));

+

+              foreach (var decl in program.TopLevelDeclarations)

+              {

+                  if (decl is NamedDeclaration && implsToVerify.Contains((decl as NamedDeclaration).Name))

+                      continue;

+                  decl.Emit(outfile, 0);

+              }

+          }

+      }

+

+      private Block GetExitBlock(Implementation impl)

+      {

+          var exitblocks = impl.Blocks.Where(blk => blk.TransferCmd is ReturnCmd);

+          if (exitblocks.Count() == 1)

+              return exitblocks.First();

+          // create a new exit block

+          var eb = new Block(Token.NoToken, "SVCeb", new List<Cmd>(), new ReturnCmd(Token.NoToken));

+          foreach (var b in exitblocks)

+          {

+              b.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { eb });

+          }

+          impl.Blocks.Add(eb);

+          return eb;

+      }

+

+      //static int LocalVarCounter = 0;

+      private LocalVariable GetNewLocal(Variable v, string suffix)

+      {

+          return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken,

+              string.Format("svc_{0}_{1}", v.Name, suffix), v.TypedIdent.Type));

+      }

+

+      private void GenVc(Implementation impl, VerifierCallback collector)

+      {

+          if (impl.Proc.Requires.Any())

+              throw new InvalidProgramForSecureVc("SecureVc: Requires not supported");

+          if(impl.LocVars.Any(v => isVisible(v)))

+              throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed");

+

+          // Gather spec, remove existing ensures

+          var secureAsserts = new List<AssertCmd>();

+          var logicalAsserts = new List<AssertCmd>();

+          

+          foreach (var ens in impl.Proc.Ensures)

+          {

+              if(ens.Free)

+                  throw new InvalidProgramForSecureVc("SecureVc: Free Ensures not supported");

+              var dd = new Duplicator();

+              secureAsserts.Add(new AssertCmd(ens.tok, Expr.Not(ens.Condition)));

+              logicalAsserts.Add(dd.VisitAssertCmd(new AssertCmd(ens.tok, ens.Condition)) as AssertCmd);

+          }

+          impl.Proc.Ensures.Clear();

+

+          // Make a copy of the impl

+          var dup = new Duplicator();

+          var implDup = dup.VisitImplementation(impl);

+

+          // Get exit block

+          var eb = GetExitBlock(impl);

+

+          // Create two blocks: one for secureAsserts, one for logical asserts

+          var ebSecure = new Block(Token.NoToken, "svc_secure_asserts", new List<Cmd>(), new ReturnCmd(Token.NoToken));

+          var ebLogical = new Block(Token.NoToken, "svc_logical_asserts", new List<Cmd>(), new ReturnCmd(Token.NoToken));

+

+          eb.TransferCmd = new GotoCmd(eb.TransferCmd.tok, new List<Block> { ebSecure, ebLogical });

+          impl.Blocks.Add(ebSecure);

+          impl.Blocks.Add(ebLogical);

+

+          // Rename spec, while create copies of the hidden variables

+          var substOld = new Dictionary<Variable, Expr>();

+          var substVarSpec = new Dictionary<Variable, Expr>();

+          var substVarPath = new Dictionary<Variable, Expr>();

+          foreach (var g in program.GlobalVariables)

+          {

+              if (!isHidden(g)) continue;

+              var lv = GetNewLocal(g, "In");

+              impl.LocVars.Add(lv);

+              substOld.Add(g, Expr.Ident(lv));

+          }

+

+          for(int i = 0; i < impl.InParams.Count; i++)

+          {

+              var v = impl.Proc.InParams[i];

+              if (!isHidden(v))

+              {

+                  substVarSpec.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i]));

+                  continue;

+              }

+

+              var lv = GetNewLocal(v, "In");

+              impl.LocVars.Add(lv);

+              substVarSpec.Add(v, Expr.Ident(lv));

+              substVarPath.Add(impl.InParams[i], Expr.Ident(lv));

+          }

+

+          for (int i = 0; i < impl.OutParams.Count; i++)

+          {

+              var v = impl.Proc.OutParams[i];

+              if (!isHidden(v))

+              {

+                  substVarSpec.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i]));

+                  continue;

+              }

+

+              var lv = GetNewLocal(v, "Out");

+              impl.LocVars.Add(lv);

+              substVarSpec.Add(v, Expr.Ident(lv));

+              substVarPath.Add(impl.OutParams[i], Expr.Ident(lv));

+          }

+

+          foreach (var g in program.GlobalVariables)

+          {

+              if (!isHidden(g)) continue;

+              if (!impl.Proc.Modifies.Any(ie => ie.Name == g.Name)) continue;

+

+              var lv = GetNewLocal(g, "Out");

+              impl.LocVars.Add(lv);

+              substVarSpec.Add(g, Expr.Ident(lv));

+              substVarPath.Add(g, Expr.Ident(lv));

+          }

+

+          secureAsserts = secureAsserts.ConvertAll(ac => 

+              Substituter.ApplyReplacingOldExprs(

+                 Substituter.SubstitutionFromHashtable(substVarSpec),

+                 Substituter.SubstitutionFromHashtable(substOld),

+                 ac) as AssertCmd);

+

+          var substVarProcToImpl = new Dictionary<Variable, Expr>();

+          for (int i = 0; i < impl.InParams.Count; i++)

+              substVarProcToImpl.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i]));

+

+          for (int i = 0; i < impl.OutParams.Count; i++)

+              substVarProcToImpl.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i]));

+

+          logicalAsserts = logicalAsserts.ConvertAll(ac =>

+              Substituter.Apply(Substituter.SubstitutionFromHashtable(substVarProcToImpl), ac)

+              as AssertCmd);

+

+          // Paths

+          foreach (var path in GetAllPaths(implDup))

+          {

+              var wp = ComputeWP(implDup, path);

+

+              // replace hidden variables to match those used in the spec

+              wp = Substituter.ApplyReplacingOldExprs(

+                  Substituter.SubstitutionFromHashtable(substVarPath),

+                  Substituter.SubstitutionFromHashtable(substOld),

+                  wp);

+

+              ebSecure.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(wp)));

+          }

+

+          ebSecure.Cmds.AddRange(secureAsserts);

+          ebLogical.Cmds.AddRange(logicalAsserts);

+

+          if (outfile != null)

+          {

+              impl.Proc.Emit(outfile, 0);

+              impl.Emit(outfile, 0);

+          }

+

+          ModelViewInfo mvInfo;

+          ConvertCFG2DAG(impl);

+          var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

+

+          var gen = prover.VCExprGen;

+          var exprGen = prover.Context.ExprGen;

+          var translator = prover.Context.BoogieExprTranslator;

+

+          var label2absy = new Dictionary<int, Absy>();

+          VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, prover.Context);

+          translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);

+          var implVc = gen.Not(GenerateVCAux(impl, null, label2absy, prover.Context));

+

+          handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, prover.Context, program);

+

+          prover.Assert(implVc, true);

+      }

+

+      Expr ComputeWP(Implementation impl, List<Cmd> path)

+      {

+          Expr expr = Expr.True;

+

+          // create constants for out varibles

+          var subst = new Dictionary<Variable, Expr>();

+          foreach (var g in impl.Proc.Modifies)

+          {

+              var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,

+                  "svc_out_const_" + g.Name, g.Decl.TypedIdent.Type));

+              subst.Add(c, g);

+              expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), g));

+          }

+

+          foreach (var v in impl.OutParams)

+          {

+              var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,

+                  "svc_out_const_" + v.Name, v.TypedIdent.Type));

+              subst.Add(c, Expr.Ident(v));

+              expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), Expr.Ident(v)));

+          }        

+

+          // we need this technicality

+          var subst1 = new Dictionary<Variable, Expr>();

+          foreach (var g in program.GlobalVariables)

+          {

+              subst1.Add(g, new OldExpr(Token.NoToken, Expr.Ident(g)));

+          }

+

+          // Implicitly close with havoc of all the locals and OutParams

+          path.Insert(0, new HavocCmd(Token.NoToken, new List<IdentifierExpr>(

+              impl.LocVars.Select(v => Expr.Ident(v)).Concat(

+              impl.OutParams.Select(v => Expr.Ident(v))))));

+

+          for (int i = path.Count - 1; i >= 0; i--)

+          {

+              var cmd = path[i];

+              if (cmd is AssumeCmd)

+              {

+                  expr = Expr.And(expr, (cmd as AssumeCmd).Expr);

+              }

+              else if (cmd is AssignCmd)

+              {

+                  var h = new Dictionary<Variable, Expr>();

+                  var acmd = cmd as AssignCmd;

+                  for (int j = 0; j < acmd.Lhss.Count; j++)

+                  {

+                      h.Add(acmd.Lhss[j].DeepAssignedVariable, acmd.Rhss[j]);

+                  }

+                  var s = Substituter.SubstitutionFromHashtable(h);

+                  expr = Substituter.Apply(s, expr);

+              }

+              else if (cmd is HavocCmd)

+              {

+                  var h = new Dictionary<Variable, Expr>();

+                  var formals = new List<Variable>();

+

+                  var vc = new VariableCollector();

+                  vc.VisitExpr(expr);

+

+                  foreach (var ie in (cmd as HavocCmd).Vars)

+                  {

+                      if (!vc.usedVars.Contains(ie.Decl)) continue;

+                      var f = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,

+                          ie.Decl.Name + "_formal", ie.Decl.TypedIdent.Type));

+                      h.Add(ie.Decl, Expr.Ident(f));

+                      formals.Add(f);

+                  }

+                  if (!formals.Any())

+                      continue;

+                  var s = Substituter.SubstitutionFromHashtable(h);

+                  expr = Substituter.Apply(s, expr);

+                  expr = new ExistsExpr(Token.NoToken, formals, expr);

+              }

+              else

+              {

+                  throw new InvalidProgramForSecureVc(string.Format("Unhandled cmd: {0}", cmd));

+              }

+          }

+

+          // Implicitly close with havoc of all the locals and OutParams

+

+

+

+          expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst1), expr);

+          expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), 

+              Substituter.SubstitutionFromHashtable(new Dictionary<Variable,Expr>()), expr);

+          expr.Typecheck(new TypecheckingContext(null));

+          return expr;

+      }

+

+      // Generate all paths in the impl

+      IEnumerable<List<Cmd>> GetAllPaths(Implementation impl)

+      {

+          var stk = new Stack<Tuple<Block, int>>();

+          stk.Push(Tuple.Create(impl.Blocks[0], 0));

+

+          while (stk.Any())

+          {

+              var tup = stk.Peek();

+              if (tup.Item1.TransferCmd is ReturnCmd)

+              {

+                  var ret = new List<Cmd>();

+                  var ls = stk.ToList();

+                  ls.Iter(t => ret.AddRange(t.Item1.Cmds));

+                  yield return ret;

+

+                  stk.Pop();

+                  continue;

+              }

+

+              stk.Pop();

+

+              var gc = tup.Item1.TransferCmd as GotoCmd;

+              if (gc.labelTargets.Count <= tup.Item2)

+                  continue;

+

+              stk.Push(Tuple.Create(tup.Item1, tup.Item2 + 1));

+              stk.Push(Tuple.Create(gc.labelTargets[tup.Item2], 0));

+          }

+          yield break;

+      }

+

+      bool isHidden(Variable v)

+      {

+          return QKeyValue.FindBoolAttribute(v.Attributes, "hidden");

+      }

+

+      bool isVisible(Variable v)

+      {

+          return !isHidden(v);

+      }

+

+      public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback)

+      {

+          Debug.Assert(this.program == program);

+

+          // Record current time

+          var startTime = DateTime.UtcNow;

+

+          CommandLineOptions.Clo.ProverCCLimit = 1;

+          prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);

+

+          // Flush any axioms that came with the program before we start SI on this implementation

+          prover.AssertAxioms();

+

+          GenVc(impl, callback);

+

+          prover.Check();

+          var outcome = prover.CheckOutcomeCore(handler);

+          //var outcome = ProverInterface.Outcome.Valid;

+          

+          prover.Close();

+

+

+

+          //Console.WriteLine("Answer = {0}", outcome);

+

+          return ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);

+      }

+  }

+

 } // namespace VC