Fixes #18

Author: vidsinghal

include/PulseGenerator.h

@@ -7,6 +7,7 @@
 #include "clang/AST/DeclBase.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/RecursiveASTVisitor.h"
+#include "clang/AST/Stmt.h"
 #include "clang/AST/Type.h"
 #include "clang/Analysis/Analyses/ExprMutationAnalyzer.h"
 #include "clang/Basic/SourceManager.h"
@@ -31,7 +32,9 @@ class PulseVisitor : public clang::RecursiveASTVisitor<PulseVisitor> {
   bool VisitTypedefDecl(clang::TypedefDecl *TypeDefDec);
 
   PulseStmt *pulseFromCompoundStmt(clang::Stmt *S, clang::ExprMutationAnalyzer *A, PulseModul *Module);
-  PulseStmt *pulseFromStmt(clang::Stmt *S, clang::ExprMutationAnalyzer *A, clang::Stmt *Parent, PulseModul *Module);
+  PulseStmt *pulseFromStmt(clang::Stmt *S, clang::ExprMutationAnalyzer *A,
+                           clang::Stmt *Parent, PulseModul *Module,
+                           clang::CompoundStmt *CS);
   FStarType *getPulseTyFromCTy(clang::QualType CType);
   Term *getTermFromCExpr(clang::Expr *E, clang::ExprMutationAnalyzer *A, llvm::SmallVector<PulseStmt*> &ExprsBef,
                            clang::Stmt *Parent, clang::QualType ParentType, PulseModul *Module, bool isWrite = false);

src/PulseGenerator.cpp

@@ -76,6 +76,73 @@ std::map<Decl *, QualType> PulseVisitor::inferArrayTypes(FunctionDecl *FD) {
   return DeclToPulseSymbol;
 }
 
+bool checkIsSameStructInstance(Expr *A, Expr *B, ASTContext &Context) {
+  A = A->IgnoreImpCasts();
+  B = B->IgnoreImpCasts();
+
+  DeclRefExpr *DeclRefA = dyn_cast<DeclRefExpr>(A);
+  if (!DeclRefA)
+    return false;
+
+  DeclRefExpr *DeclRefB = dyn_cast<DeclRefExpr>(B);
+  if (!DeclRefB)
+    return false;
+
+  if (DeclRefA && DeclRefB) {
+    return DeclRefA->getDecl() == DeclRefB->getDecl();
+  }
+
+  MemberExpr *MemA = dyn_cast<MemberExpr>(A);
+  MemberExpr *MemB = dyn_cast<MemberExpr>(B);
+
+  if (MemA && MemB) {
+    return checkIsSameStructInstance(MemA->getBase(), MemB->getBase(), Context);
+  }
+
+  // Also check recursively pointer derefernces and array access.
+  UnaryOperator *UOA = dyn_cast<UnaryOperator>(A);
+  UnaryOperator *UOB = dyn_cast<UnaryOperator>(B);
+
+  if (UOA && UOB && UOA->getOpcode() == UOB->getOpcode()) {
+    return checkIsSameStructInstance(UOA->getSubExpr(), UOB->getSubExpr(),
+                                     Context);
+  }
+
+  return false;
+}
+
+bool checkIfLastStructAccess(MemberExpr *ToCheck, CompoundStmt *CS,
+                             ASTContext &Context) {
+  Expr *ToCheckBase = ToCheck->getBase()->IgnoreImpCasts();
+  SourceManager &SM = Context.getSourceManager();
+  SourceLocation ToCheckLoc = ToCheck->getExprLoc();
+  SourceLocation LastLoc = ToCheckLoc;
+
+  for (const Stmt *S : CS->body()) {
+    // Traverse the compound statement and visit it recursively.
+    // We store the last accessed member in LastLoc.
+    // When we encounter a member expr, we check if this is the same instance as
+    //  the ToBeChecked member expression.
+    // We also check if the member expression comes after the to be checked
+    // member,
+    //  if so we update Last loc.
+    for (const Stmt *Child : S->children()) {
+      if (auto *ME = dyn_cast<MemberExpr>(Child)) {
+        Expr *Base = ME->getBase()->IgnoreImpCasts();
+        if (Context.getParents(*Base).size() > 0 &&
+            SM.isBeforeInTranslationUnit(ToCheckLoc, ME->getExprLoc()) &&
+            checkIsSameStructInstance(Base, ToCheckBase, Context)) {
+          LastLoc = ME->getExprLoc();
+        }
+      }
+    }
+  }
+
+  // If the location of the member to be checked is the same as the last loc
+  // This is indeed the last access to the member.
+  return ToCheckLoc == LastLoc;
+}
+
 bool PulseVisitor::checkIsRecursiveFunction(FunctionDecl *FD) {
 
   bool result = false;
@@ -852,6 +919,8 @@ bool PulseVisitor::VisitFunctionDecl(FunctionDecl *FD) {
       auto *PulseBody = pulseFromCompoundStmt(CS, &Analyzer, Module);
 
       // Release declarations that are function parameters.
+      //TODO: Vidush Eventually we should get rid of these.
+      //This is just in case there are release expressions left and we need to release them.
       PulseSequence *NewSeq = nullptr;
       PulseSequence *Head = nullptr;
       for (auto It = TrackStructExplodeAndRecover.begin(); It != TrackStructExplodeAndRecover.end();) {
@@ -975,7 +1044,8 @@ PulseStmt *PulseVisitor::pulseFromCompoundStmt(Stmt *S,
 
     for (auto *InnerStmt : CS->body()) {
 
-      auto *NextPulseStmt = pulseFromStmt(InnerStmt, Analyzer, nullptr, Modul);
+      auto *NextPulseStmt =
+          pulseFromStmt(InnerStmt, Analyzer, nullptr, Modul, CS);
       if (NextPulseStmt == nullptr)
         continue;
 
@@ -998,7 +1068,8 @@ PulseStmt *PulseVisitor::pulseFromCompoundStmt(Stmt *S,
 }
 
 PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
-                                       Stmt *Parent, PulseModul *Module) {
+                                       Stmt *Parent, PulseModul *Module,
+                                       CompoundStmt *CS) {
 
   if (!S)
     return nullptr;
@@ -1243,8 +1314,6 @@ PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
           PulseCall->pushArg(ParenthesisDeref);
           Assignment->Lhs = PulseCall;
 
-          assert(ExprsBef.empty() && "Expected ExprsBefore to be empty!\n");
-
           auto It = TrackStructExplodeAndRecover.find(VD);
           if (It == TrackStructExplodeAndRecover.end()){
             auto *NewSeq = new PulseSequence();
@@ -1256,6 +1325,47 @@ PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
             return NewSeq;
           }
 
+          auto *RetSeq = releaseExprs(ExprsBef);
+
+          assert(ExprsBef.empty() && "Expected ExprsBefore to be empty!\n");
+
+          if (checkIfLastStructAccess(ME, CS, Ctx)) {
+
+            It = TrackStructExplodeAndRecover.find(VD);
+            auto ItElem = *It;
+            auto &Decl = ItElem.first;
+            auto &Info = ItElem.second;
+            // recover not released.
+            // In fact assert that a recover should not be released before.
+            assert(!Info.second && "A recover was released for the struct when "
+                                   "there are accesses remaining!\n");
+            if (auto *ParamD = dyn_cast<ParmVarDecl>(Decl)) {
+
+              auto StructName =
+                  ParamD->getType()->getPointeeType().getAsString();
+
+              auto *RecoverStatememt = new GenericStmt();
+              RecoverStatememt->body =
+                  StructName + "_recover " + ParamD->getNameAsString() + ";";
+              TrackStructExplodeAndRecover.erase(It);
+
+              auto *NewSeq = new PulseSequence();
+              NewSeq->assignS1(Assignment);
+              NewSeq->assignS2(RecoverStatememt);
+              if (RetSeq) {
+                RetSeq->assignS2(NewSeq);
+                return RetSeq;
+              }
+
+              return NewSeq;
+            }
+          }
+
+          if (RetSeq) {
+            RetSeq->assignS2(Assignment);
+            return RetSeq;
+          }
+
           return Assignment;
         }
 
@@ -1432,8 +1542,8 @@ PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
 
     auto PulseCond =
         getTermFromCExpr(Cond, Analyzer, ExprsBefore, Parent, Cond->getType(), Module);
-    auto *PulseElse = pulseFromStmt(Else, Analyzer, Parent, Module);
-    auto *PulseThen = pulseFromStmt(Then, Analyzer, Parent, Module);
+    auto *PulseElse = pulseFromStmt(Else, Analyzer, Parent, Module, CS);
+    auto *PulseThen = pulseFromStmt(Then, Analyzer, Parent, Module, CS);
 
     auto PulseIfStmt = new PulseIf();
     PulseIfStmt->setTag(PulseStmtTag::If);
@@ -1551,7 +1661,8 @@ PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
       }
 
       PulseWhile->setTag(PulseStmtTag::WhileStmt);
-      PulseWhile->Guard = pulseFromStmt(WhileCond, Analyzer, Parent, Module);
+      PulseWhile->Guard =
+          pulseFromStmt(WhileCond, Analyzer, Parent, Module, CS);
       PulseWhile->Body = pulseFromCompoundStmt(CompundBody, Analyzer, Module);
 
       return PulseWhile;
@@ -1560,7 +1671,8 @@ PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
       auto *PulseWhile = new PulseWhileStmt();
       PulseWhile->setTag(PulseStmtTag::WhileStmt);
 
-      PulseWhile->Guard = pulseFromStmt(WhileCond, Analyzer, Parent, Module);
+      PulseWhile->Guard =
+          pulseFromStmt(WhileCond, Analyzer, Parent, Module, CS);
       PulseWhile->Body = pulseFromCompoundStmt(WhileBody, Analyzer, Module);
 
       return PulseWhile;
@@ -1605,7 +1717,7 @@ PulseStmt *PulseVisitor::pulseFromStmt(Stmt *S, ExprMutationAnalyzer *Analyzer,
         }
       }
     }
-    NewSequence->assignS2(pulseFromStmt(SubStmt, Analyzer, Parent, Module));
+    NewSequence->assignS2(pulseFromStmt(SubStmt, Analyzer, Parent, Module, CS));
     return NewSequence;
   } else {
     llvm::outs() << "\n\nPrint in pulseFromStmt\n";
@@ -1715,9 +1827,6 @@ PulseVisitor::getTermFromCExpr(Expr *E, ExprMutationAnalyzer *MutAnalyzer,
     // Wrap Call Expr into a Paren to be safe.
     auto *NewParen = new Paren();
     NewParen->setInnerExpr(NewAppENode);
-
-    assert(ExprsBefore.empty() && "Unreleased expressions!\n");
-
     return NewParen;
 
     llvm::outs() << "\n\nPrint Expresion in PulseVisitor::getTermFromCExpr "
@@ -2049,8 +2158,7 @@ PulseVisitor::getTermFromCExpr(Expr *E, ExprMutationAnalyzer *MutAnalyzer,
     assert(false && "Should not reach here!");
     return nullptr;
   } else if (auto *ME = dyn_cast<MemberExpr>(E)) {
-   
-    
+
     auto *MemberExprDecl = ME->getMemberDecl();
 
     auto *BaseExpr = ME->getBase()->IgnoreParens()->IgnoreImpCasts();

test-transpiler/c/issues/issue18.c

@@ -0,0 +1,49 @@
+#include <stdint.h>
+#include <stdlib.h>
+#include "../../../include/PulseMacros.h"
+
+REQUIRES(emp)
+RETURNS(i:int32)
+ENSURES(emp)
+int test(void)
+{
+  return 0;
+}
+
+typedef struct _point {
+  int px;
+  int py;
+} point;
+
+
+INCLUDE (
+  let is_diag_point (p:ref point) (v:int32)
+  : slprop
+  = point_pred p {px=v; py=v}
+
+  let is_point (p:ref point) (xy : (int & int))
+  : slprop
+  = exists* v. point_pred p v ** pure (as_int v.px == fst xy) ** pure (as_int v.py == snd xy)
+
+  ghost
+  fn fold_is_point (p:ref point) (#s:point_spec)
+  requires point_pred p s
+  ensures exists* v. is_point p v ** pure (v == (as_int s.px, as_int s.py))
+  {
+    fold (is_point p (as_int s.px, as_int s.py));
+  }
+
+)
+
+ERASED_ARG(#v:erased _)
+REQUIRES(is_point p v)
+REQUIRES(pure <| fits (+) (fst v) (as_int dx))
+REQUIRES(pure <| fits (+) (snd v) (as_int dy))
+ENSURES(is_point p (fst v + as_int dx, snd v + as_int dy))
+void move(point *p, int dx, int dy)
+{
+  LEMMA(unfold(is_point));
+  p->px = p->px + dx;
+  p->py = p->py + dy;
+  LEMMA(fold_is_point p);
+}