working on #3: setup infrastructure to handle on the fly method calls

benchmarks/github/voldemort/1f0db5f73a_PipelineRoutedStore_getAll_o.java

@@ -18,4 +18,4 @@ void getAll() {
     throw pipelineData.getFatalError();
   return pipelineData.getResult();
 }
-}
+}

src/Analysis/Engine.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE RecordWildCards #-}
 -------------------------------------------------------------------------------
 -- Module    :  Analysis.Engine
 -- Copyright :  (c) 2016 Marcelo Sousa
@@ -41,7 +42,7 @@ helper pre post = do
 prelude :: [FormalParam] -> Z3 (Params, [AST])
 prelude params = do
   let arity = 4
-      ps = getParIdents params 
+      ps = ["o"] -- getParIdents params 
       parsId = map (\s -> map (\ar -> s ++ show ar) [1..arity]) ps 
   intSort <- mkIntSort
   pars <- mapM (mapM (\par -> mkFreshConst par intSort)) parsId
@@ -114,56 +115,62 @@ enc_ident str i sort = mapM (\j -> do
   let nstr = str ++ "_" ++ show j ++ "_" ++ show i
   sym <- mkStringSymbol nstr
   mkVar sym sort) [1..4]
-
-enc_new_var :: (SSAMap, AssignMap, AST) -> Sort -> VarDecl -> Int -> Z3 (SSAMap, AssignMap, AST)
-enc_new_var (ssamap', _assmap, pre') sort (VarDecl varid mvarinit) i = do
-  (ident, idAsts) <-
+
+-- encode the first variable definition 
+enc_new_var :: Sort -> Int -> VarDecl -> EnvOp ()
+enc_new_var sort i (VarDecl varid mvarinit) = do
+  env@Env{..} <- get
+  (ident, idAsts) <- lift $ 
     case varid of
       VarId ident@(Ident str) -> do
         vars <- enc_ident str i sort
         return (ident, vars)
       _ -> error $ "enc_new_var: not supported " ++ show varid
-  let nssamap = M.insert ident [(idAst, sort, i) | idAst <- idAsts] ssamap'
+  let nssamap = M.insert ident [(idAst, sort, i) | idAst <- idAsts] _ssamap
+  updateSSAMap nssamap
   case mvarinit of
-    Nothing -> return (nssamap, _assmap, pre')
+    Nothing -> return ()
     Just (InitExp expr) -> do
-      expAsts <- enc_exp 0 nssamap expr
+      expAsts <- enc_exp 0 expr
       let id_exp = zip idAsts expAsts
-      eqIdExps <- mapM (\(idAst,expAst) -> mkEq idAst expAst) id_exp
-      pre <- mkAnd (pre':eqIdExps)
-      let assmap = M.insert ident expr _assmap
-      return (nssamap, assmap, pre)
+      eqIdExps <- lift $ mapM (\(idAst,expAst) -> mkEq idAst expAst) id_exp
+      let nassmap = M.insert ident expr _assmap
+      updateAssignMap nassmap
+      npre <- lift $ mkAnd (_pre:eqIdExps)
+      updatePre npre 
     Just _ -> error "enc_new_var: not supported"
-
-enc_exp :: Int -> SSAMap -> Exp -> Z3 [AST]
-enc_exp p env expr = do
+
+-- enc_exp: encodes an expression for a version 
+enc_exp :: Int -> Exp -> EnvOp [AST]
+enc_exp p expr = do
   let l = if p == 0 then [1..4] else [p]
-  mapM (\p -> enc_exp_inner (p,env) expr) l
+  mapM (\p -> enc_exp_inner p expr) l
 
 -- | Encode an expression for a version 
 --   (ast,sort,count)pre-condition: pid != 0 
-enc_exp_inner :: (Int, SSAMap) -> Exp -> Z3 AST
-enc_exp_inner env expr = case expr of
-  Lit lit -> enc_literal lit
-  ExpName name -> enc_name env name []
+enc_exp_inner :: Int -> Exp -> EnvOp AST
+enc_exp_inner p expr = do
+ case expr of
+  Lit lit -> lift $ enc_literal lit 
+  ExpName name -> enc_name p (toIdent name) []
   BinOp lhsE op rhsE -> do
-    lhs <- enc_exp_inner env lhsE
-    rhs <- enc_exp_inner env rhsE
-    enc_binop op lhs rhs
+    lhs <- enc_exp_inner p lhsE
+    rhs <- enc_exp_inner p rhsE
+    lift $ enc_binop op lhs rhs
   PreMinus nexpr -> do 
-    nexprEnc <- enc_exp_inner env nexpr
-    mkUnaryMinus nexprEnc
+    nexprEnc <- enc_exp_inner p nexpr
+    lift $ mkUnaryMinus nexprEnc
   MethodInv (MethodCall name args) -> do
-    argsAST <- mapM (enc_exp_inner env) args
-    enc_name env name argsAST
+    argsAST <- mapM (enc_exp_inner p) args
+    enc_name p (toIdent name) argsAST
   Cond cond _then _else -> do
-    condEnc <- enc_exp_inner env cond
-    _thenEnc <- enc_exp_inner env _then
-    _elseEnc <- enc_exp_inner env _else
-    mkIte condEnc _thenEnc _elseEnc        
+    condEnc <- enc_exp_inner p cond
+    _thenEnc <- enc_exp_inner p _then
+    _elseEnc <- enc_exp_inner p _else
+    lift $ mkIte condEnc _thenEnc _elseEnc        
   PreNot nexpr -> do
-    nexprEnc <- enc_exp_inner env nexpr
-    mkNot nexprEnc
+    nexprEnc <- enc_exp_inner p nexpr
+    lift $ mkNot nexprEnc
   _ -> error $  "enc_exp_inner: " ++ show expr
 
 enc_literal :: Literal -> Z3 AST
@@ -177,13 +184,18 @@ enc_literal lit =
 --    Just (ast, _, _) -> return ast
     _ -> error "processLit: not supported"
 
-enc_name :: (Int, SSAMap) -> Name -> [AST] -> Z3 AST
-enc_name (pid, ssamap) (Name [obj]) [] =
-  case M.lookup obj ssamap of
-    Nothing -> error $ "enc_name: not in map " ++ show obj
+toIdent :: Name -> Ident
+toIdent (Name []) = error $ "nameToIdent: Name []"
+toIdent (Name l) = foldr (\(Ident a) (Ident b) -> Ident (a ++ "." ++ b)) (Ident "") l 
+
+enc_name :: Int -> Ident -> [AST] -> EnvOp AST
+enc_name pid ident [] = do
+  env@Env{..} <- get
+  case M.lookup ident _ssamap of
+    Nothing -> error $ "enc_name: not in map " ++ show ident 
     Just l -> case l !! (pid-1) of
       (ast,_,_) -> return ast
-enc_name (pid, ssamap) _ _ = error "enc_name: not supported yet"
+enc_name pid ident args = error "enc_name: not supported yet"
 {-
 processName env@(objSort, pars, res, fields, ssamap) (Name [ident]) args = do
   let fn = safeLookup ("processName: declared func")  ident fields

src/Analysis/Verifier.hs

@@ -42,7 +42,7 @@ verify (pars, Block body) e_o e_a e_b e_m = do
  iSSAMap <- initial_SSAMap params res
  let iEnv = Env iSSAMap M.empty pre post post e_o e_a e_b e_m True 0 0 
      p = [(0, body)]
- ((res, model),_) <- runStateT (analyser p) iEnv
+ ((res, model), _) <- runStateT (analyser p) iEnv
  case res of 
   Unsat -> return (Unsat, Nothing)
   Sat -> do
@@ -100,14 +100,7 @@ analyser_pid (pid,stmts) rest = case stmts of
     LocalVars mods ty vars -> do
       env@Env{..} <- get
       sort <- lift $ processType ty    
-      (nssamap, nassmap, npre) <- 
-        lift $ foldM (\(ssamap', assmap', pre') v ->
-          -- we assume that different versions cannot define the same variable 
-          enc_new_var (ssamap', assmap', pre') sort v 0) 
-          (_ssamap, _assmap, _pre) vars
-      updatePre npre
-      updateSSAMap nssamap
-      updateAssignMap nassmap
+      mapM_ (enc_new_var sort 0) vars 
       analyser ((pid,stmts_pid):rest)
 
 analyser_stmt :: (Pid, Stmt) -> ProdProgram -> EnvOp (Result, Maybe Model)
@@ -166,8 +159,8 @@ analyse_conditional pid cond s1 s2 rest = T.trace ("analyse conditional of pid "
   resElse <- analyser ((pid, [BlockStmt s2]):rest)
   combine resThen resElse                
  else do
+  condSmt <- enc_exp pid cond
   env@Env{..} <- get
-  condSmt <- lift $ enc_exp pid _ssamap cond
   -- then branch
   preThen <- lift $ mkAnd (_pre:condSmt)
   resThen <- analyse_branch preThen s1
@@ -333,13 +326,13 @@ ret pid _exp pro = do
 
 ret_inner :: Pid -> Maybe Exp -> EnvOp ()
 ret_inner pid mexpr = do
- env@Env{..} <- get
- exprPsi <- lift $ 
+ exprPsi <- 
    case mexpr of
      Nothing -> error "ret: return Nothing"
-     Just (Lit (Boolean True)) -> mkIntNum 1
-     Just (Lit (Boolean False)) -> mkIntNum 0
-     Just expr -> enc_exp_inner (pid,_ssamap) expr
+     Just (Lit (Boolean True)) -> lift $ mkIntNum 1
+     Just (Lit (Boolean False)) -> lift $ mkIntNum 0
+     Just expr -> enc_exp_inner pid expr
+ env@Env{..} <- get
  let res_str = Ident "_res_"
      (res_ast,sort, i) = (safeLookup "ret_inner" res_str _ssamap) !! (pid-1)
  r <- lift $ mkEq res_ast exprPsi
@@ -355,8 +348,8 @@ assign pid _exp lhs aOp rhs = do
 
 assign_inner :: Pid -> Exp -> Lhs -> AssignOp -> Exp -> EnvOp ()
 assign_inner pid _exp lhs aOp rhs = do
+ rhsAst <- enc_exp_inner pid rhs
  env@Env{..} <- get
- rhsAst <- lift $ enc_exp_inner (pid, _ssamap) rhs
  case lhs of
   NameLhs (Name [ident@(Ident str)]) -> do
    let (plhsAST,sort, i) = (safeLookup "Assign" ident _ssamap) !! (pid-1)
@@ -382,8 +375,8 @@ post_op pid _exp lhs op str = do
 
 post_op_inner :: Pid -> Exp -> Exp -> Op -> String -> EnvOp ()
 post_op_inner pid _exp lhs op str = do
+ rhsAst <- enc_exp_inner pid (BinOp lhs op (Lit $ Int 1))
  env@Env{..} <- get
- rhsAst <- lift $ enc_exp_inner (pid,_ssamap) (BinOp lhs op (Lit $ Int 1))
  case lhs of
   ExpName (Name [ident@(Ident str)]) -> do
    let (plhsAST,sort, i) = (safeLookup "post_op_inner" ident _ssamap) !! (pid-1)

src/Main.hs

@@ -45,7 +45,7 @@ instance Default InvGen where
 data Option = Parse   { file :: FilePath }
             | Diff2   { prog :: FilePath, a :: FilePath }
             | Diff4   { prog :: FilePath, a :: FilePath, b :: FilePath, merge :: FilePath }
-            | Verify  { prog :: FilePath, a :: FilePath, b :: FilePath, merge :: FilePath }
+            | Verify  { base :: FilePath } 
             | Product { prog :: FilePath, a :: FilePath, b :: FilePath, merge :: FilePath }
             | Merge   { prog :: FilePath, a :: FilePath, b :: FilePath, merge :: FilePath, output :: FilePath }
   deriving (Show, Data, Typeable, Eq)
@@ -56,8 +56,7 @@ productMode = Product { prog = def, a = def
                       , b = def, merge = def } &= help _helpProduct
 diffMode = Diff4 { prog = def, a = def, b = def
                 , merge = def } &= help _helpDiff
-verifyMode = Verify { prog = def, a = def, b = def
-                , merge = def } &= help _helpVerify 
+verifyMode = Verify { base = def } &= help _helpVerify 
 diff2Mode = Diff2 { prog = def, a = def } &= help _helpDiff2
 mergeMode = Merge { prog = def, a = def, b = def
                   , merge = def, output = def } &= help _helpMerge
@@ -81,7 +80,12 @@ runOption opt = case opt of
     putStrLn $ prettyPrint prog
   Diff2 o a -> diff2 o a
   Diff4 o a b m -> diff4 o a b m
-  Verify o a b m -> verify o a b m
+  Verify f -> do
+    let o = f ++ "_o.java"
+        a = f ++ "_a.java"
+        b = f ++ "_b.java"
+        m = f ++ "_m.java"
+    verify o a b m
   _ -> error $ "wiz: option currently not supported"
 {-
   Product p a b m -> do
@@ -158,6 +162,9 @@ verify ofl afl bfl mfl = do
   let (fo,e_o,e_a,e_b,e_m) = diff4gen o a b m 
       pairs = [(o,fo,e_o),(a,fo,e_a),(b,fo,e_b),(m,fo,e_m)]
       es = [e_o,e_a,e_b,e_m]
+  putStrLn "Program with holes:"
+  putStrLn $ prettyPrint fo 
+  putStrLn ""
   mapM_ print_edit $ zip es [0..]
   let res = map check_edit_soundness pairs
   if all id res