Type annotator

language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs

@@ -38,7 +38,7 @@ import           Prelude                          hiding (mapM, mapM_)
 data SemPhase
 
 
-type instance AnnTranslationUnit SemPhase = (NodeInfo, GlobalDecls)
+type instance AnnTranslationUnit SemPhase = NodeInfo
 type instance AnnFunctionDef SemPhase     = NodeInfo
 type instance AnnAsmExt SemPhase          = NodeInfo
 type instance AnnStringLiteral SemPhase   = NodeInfo
@@ -69,7 +69,7 @@ analyseAST (CTranslUnit decls _file_node) = do
     getDefTable >>= \dt -> unless (inFileScope dt) $
         error "Internal Error: Not in filescope after analysis"
     gld <- globalDefs <$> getDefTable
-    return $ CTranslUnit decls' (_file_node, gld)
+    return $ CTranslUnit decls' (_file_node)
 
 
 analyseExt :: (MonadTrav m) => CExternalDeclaration NodeInfo -> m (CExternalDeclaration SemPhase)

vdiff/app/vdiff-take/Main.hs

@@ -148,7 +148,7 @@ testParse :: FilePath -> IO Bool
 testParse f = timeoutM (5 * 1000 * 1000) testParse' `catch` (\(_ :: IOException) -> return False)
   where
     testParse' = do
-      res <- liftIO $ runRIO NoLogging $ openCFile f
+      res <- liftIO $ runRIO NoLogging $ openCFile DefaultTypechecker f
       case force $ prettyp <$> res of
         Nothing -> return False
         Just  _ -> return True

vdiff/app/vdiff/Main.hs

@@ -14,26 +14,26 @@ infos = fullDesc <> progDesc "vdiff - a simple tool to compare program verifiers
 
 main :: IO ()
 main = runVDiffApp parseMainParameters infos $ \case
-  (CmdRun seed dp)       -> cmdDiff seed dp
-  (CmdParseTest fn)      -> cmdParseTest fn
-  (CmdMarkReads mode fn) -> cmdMarkReads mode fn
+  (CmdRun tc seed dp)       -> cmdDiff tc seed dp
+  (CmdParseTest tc fn)      -> cmdParseTest tc fn
+  (CmdMarkReads mode tc fn) -> cmdMarkReads mode tc fn
   CmdVersions            -> cmdVersions
   CmdRunVerifiers dp     -> cmdRunVerifiers dp
 
 
-data Cmd  = CmdRun (Maybe Int) DiffParameters -- first parameter is the seed
+data Cmd  = CmdRun TypecheckerFlag (Maybe Int) DiffParameters -- first parameter is the seed
           | CmdRunVerifiers DiffParameters
-          | CmdParseTest FilePath
-          | CmdMarkReads SearchMode FilePath
+          | CmdParseTest TypecheckerFlag FilePath
+          | CmdMarkReads SearchMode TypecheckerFlag FilePath
           | CmdVersions
 
 
 parseMainParameters :: Parser Cmd
 parseMainParameters = hsubparser $ mconcat [versionCommand, parseCommand, markCommand, runCommand, diffCommand]
   where
     versionCommand = command "versions" (info (pure CmdVersions) (progDesc "display the versions of the integrated verifiers"))
-    parseCommand   = command "parse" (info (CmdParseTest <$> cFile) (progDesc "parses and prints the given file"))
-    markCommand    = command "mark-reads" (info (CmdMarkReads <$> Args.searchMode <*> cFile) (progDesc "marks the reads in the given file"))
+    parseCommand   = command "parse" (info (CmdParseTest <$> Args.typechecker <*> cFile) (progDesc "parses and prints the given file"))
+    markCommand    = command "mark-reads" (info (CmdMarkReads <$> Args.searchMode <*> Args.typechecker <*> cFile) (progDesc "marks the reads in the given file"))
     runCommand     = command "run" (info (CmdRunVerifiers <$> Args.diffParameters) (progDesc "execute verifiers"))
-    diffCommand    = command "diff" (info (CmdRun <$> Args.seed <*> Args.diffParameters) (progDesc "diff verifiers"))
+    diffCommand    = command "diff" (info (CmdRun <$> Args.typechecker <*> Args.seed <*> Args.diffParameters) (progDesc "diff verifiers"))
 

vdiff/assets/test/typecheck/benghazi.c

@@ -0,0 +1,24 @@
+/*
+ * Date: 06/07/2015
+ * Created by: Ton Chanh Le (chanhle@comp.nus.edu.sg)
+ * Adapted from Benghazi_true-termination.c
+ */
+
+typedef enum {false, true} bool;
+
+extern int __VERIFIER_nondet_int(void);
+
+int main()
+{
+    int x, d1, d2, d1old;
+    x = __VERIFIER_nondet_int();
+    d1 = __VERIFIER_nondet_int();
+    d2 = __VERIFIER_nondet_int();
+	while (x >= 0) {
+		x = x - d1;
+		d1old = d1;
+		d1 = d2 + 1;
+		d2 = d1old + 1;
+	}
+	return 0;
+}

vdiff/assets/test/typecheck/newton_1_3_true-unreach-call_true-termination.c

@@ -0,0 +1,58 @@
+extern void __VERIFIER_error(void);
+extern void __VERIFIER_assume(int);
+extern float __VERIFIER_nondet_float(void);
+
+#define NR 3
+
+#if NR == 1
+#define VAL 0.2f
+#elif NR == 2
+#define VAL 0.4f
+#elif NR == 3
+#define VAL 0.6f
+#elif NR == 4
+#define VAL 0.8f
+#elif NR == 5
+#define VAL 1.0f
+#elif NR == 6
+#define VAL 1.2f
+#elif NR == 7
+#define VAL 1.4f
+#elif NR == 8
+#define VAL 2.0f
+#endif
+
+#define ITERATIONS 1
+
+#if !(ITERATIONS >= 1 && ITERATIONS <= 3)
+#error Number of iterations must be between 1 and 3
+#endif 
+
+float f(float x)
+{
+  return x - (x*x*x)/6.0f + (x*x*x*x*x)/120.0f + (x*x*x*x*x*x*x)/5040.0f;
+}
+
+float fp(float x)
+{
+  return 1 - (x*x)/2.0f + (x*x*x*x)/24.0f + (x*x*x*x*x*x)/720.0f;
+}
+
+int main()
+{
+  float IN = __VERIFIER_nondet_float();
+  __VERIFIER_assume(IN > -VAL && IN < VAL);
+
+  float x = IN - f(IN)/fp(IN);
+#if ITERATIONS > 1 
+  x = x - f(x)/fp(x);
+#if ITERATIONS > 2
+  x = x - f(x)/fp(x);
+#endif 
+#endif
+
+  if(!(x < 0.1))
+    __VERIFIER_error();
+
+  return 0;
+}

vdiff/assets/test/typecheck/standard_copy9_true-unreach-call_ground.i

@@ -0,0 +1,52 @@
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
+extern int __VERIFIER_nondet_int();
+int main( ) {
+  int a1[100000];
+  int a2[100000];
+  int a3[100000];
+  int a4[100000];
+  int a5[100000];
+  int a6[100000];
+  int a7[100000];
+  int a8[100000];
+  int a9[100000];
+  int a0[100000];
+  int a;
+  for ( a = 0 ; a < 100000 ; a++ ) {
+    a1[a] = __VERIFIER_nondet_int();
+  }
+  int i;
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a2[i] = a1[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a3[i] = a2[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a4[i] = a3[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a5[i] = a4[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a6[i] = a5[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a7[i] = a6[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a8[i] = a7[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a9[i] = a8[i];
+  }
+  for ( i = 0 ; i < 100000 ; i++ ) {
+    a0[i] = a9[i];
+  }
+  int x;
+  for ( x = 0 ; x < 100000 ; x++ ) {
+    __VERIFIER_assert( a1[x] == a0[x] );
+  }
+  return 0;
+}

vdiff/assets/test/typecheck/sum10_true-unreach-call_true-termination.c

@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers" 
+ * which was published at TACAS 2015 and 
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ * 
+ * We checks if a function is "deterministic" w.r.t. all possible permutations 
+ * of an input array.  Such property is desirable for reducers in the 
+ * map-reduce programming model.  It ensures that the program always computes 
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sum
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int sum (int x[N])
+{
+  int i;
+  long long ret;
+  ret = 0;
+  for (i = 0; i < N; i++) {
+    ret = ret + x[i];
+  }
+  return ret;
+}
+
+int main ()
+{
+  int x[N];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < N; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = fun(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = fun(x);
+  temp=x[0];
+  for(int i =0 ; i<N-1; i++){
+     x[i] = x[i+1];
+  }
+  x[N-1] = temp;
+  ret5 = fun(x);
+
+  if(ret != ret2 || ret !=ret5){ 
+    __VERIFIER_error();
+  }
+  return 1;
+}

vdiff/assets/test/typecheck/underapprox_false-unreach-call2_true-termination.c

@@ -0,0 +1,20 @@
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+void __VERIFIER_assert(int cond) {
+  if (!(cond)) {
+    ERROR: __VERIFIER_error();
+  }
+  return;
+}
+
+int main(void) {
+  unsigned int x = 0;
+  unsigned int y = 1;
+
+  while (x < 6) {
+    x++;
+    y *= 2;
+  }
+
+  __VERIFIER_assert(x != 6);
+}

vdiff/src/VDiff/Arguments.hs

@@ -121,6 +121,14 @@ resources =  do
           "GB" -> GB
 
 
+
+typechecker ::  Parser TypecheckerFlag 
+typechecker = option tc (long "typechecker" <> value DefaultTypechecker)
+  where
+    tc = str >>= \case
+      "default" -> return DefaultTypechecker
+      "simple"  -> return SimpleTypechecker
+
 -- | The verifier list is a space separated list of verifiers. A verifier can be indicated by either:
 -- * its name, e.g. @smack@
 -- * its name with a combination of parameters @smack(--loop-unroll=1)@

vdiff/src/VDiff/Diff.hs

@@ -26,14 +26,15 @@ import           VDiff.ArithmeticExpressions (evalExpr)
 import           VDiff.Data
 import           VDiff.Execute
 import           VDiff.Instrumentation
+import           VDiff.SimpleTypecheck (simpleTypechecker)
 import           VDiff.Strategy
 import           VDiff.Util.ResourcePool
 import           VDiff.Verifier
 
 
 
-cmdDiff :: HasMainEnv a => Maybe Int -> DiffParameters -> RIO a ()
-cmdDiff seed params = do
+cmdDiff :: HasMainEnv a => TypecheckerFlag -> Maybe Int -> DiffParameters -> RIO a ()
+cmdDiff tcFlag seed params = do
   logInfo "starting diff"
 
   s <- case seed of
@@ -42,8 +43,7 @@ cmdDiff seed params = do
   logInfo $ "seed for random generator: " <> display s
   liftIO $ setStdGen $ mkStdGen s
 
-
-  mAst <- openCFile (params ^. inputFile)
+  mAst <- openCFile tcFlag (params ^. inputFile)
   case mAst of
     Nothing -> liftIO exitFailure
     Just ast -> do
@@ -54,21 +54,21 @@ cmdDiff seed params = do
 
 -- | parses the file, runs the semantic analysis (type checking), and pretty-prints the resulting semantic AST.
 -- Use this to test the modified language-c-extensible library.
-cmdParseTest :: HasLogFunc env => FilePath -> RIO env ()
-cmdParseTest fn = openCFile fn >>= \case
+cmdParseTest :: HasLogFunc env => TypecheckerFlag ->  FilePath -> RIO env ()
+cmdParseTest tc fn = openCFile tc fn >>= \case
   Nothing -> liftIO exitFailure
   Just ast -> liftIO $ putStrLn $ render $ pretty ast
 
 
-cmdMarkReads :: HasLogFunc env => SearchMode -> FilePath -> RIO env ()
-cmdMarkReads mode fn = do
+cmdMarkReads :: HasLogFunc env => SearchMode -> TypecheckerFlag -> FilePath -> RIO env ()
+cmdMarkReads mode tc fn = do
   logDebug $ "mode is " <> display (tshow mode)
-  (Just ast) <- openCFile fn
+  (Just ast) <- openCFile tc fn
   let ast' = markAllReads mode ast
   liftIO . putStrLn . render . pretty $ ast'
 
 cmdVersions :: RIO a ()
-cmdVersions = liftIO $ forM_ (sortBy (comparing (^. name)) allVerifiers) $ \verifier -> do
+cmdVersions = liftIO $ forM_ (L.sortOn (^. name) allVerifiers) $ \verifier -> do
     T.putStr $ verifier ^. name
     putStr ": "
     sv <- try (verifier ^. version) >>= \case

vdiff/src/VDiff/Instrumentation.hs

@@ -9,6 +9,7 @@ module VDiff.Instrumentation
  (
    -- * Handling C files
   openCFile
+ , defaultTypechecker
  , preprocess
  , maskAsserts
  , defineAssert
@@ -55,23 +56,35 @@ import           UnliftIO.Directory
 import           VDiff.Instrumentation.Browser
 import qualified VDiff.Instrumentation.Fragments   as Fragments
 import           VDiff.Instrumentation.Reads
+import           VDiff.SimpleTypecheck
 
 
+defaultTypechecker :: Typechecker
+defaultTypechecker tu = runTrav_ (analyseAST tu)
 
 -- | short-hand for open, parse and type annotate, will log parse and type checking errors and warnings.
-openCFile :: HasLogFunc env => FilePath -> RIO env (Maybe TU)
-openCFile fn = do
+openCFile :: HasLogFunc env => TypecheckerFlag -> FilePath -> RIO env (Maybe TU)
+openCFile tcFlag fn = do
   -- we need GCC to remove preprocessor tokens and comments,
   -- unfortunately, GCC only works on files with .c ending. Hence this hack.
   let templateName = takeFileName $ replaceExtension fn ".c"
+
+  typechecker <- case tcFlag of
+    DefaultTypechecker -> do
+      logInfo "using default typechecker (language-c)"
+      return defaultTypechecker
+    SimpleTypechecker  -> do
+      logInfo "using simple typechecker"
+      return simpleTypechecker
+
   withSystemTempFile  templateName $  \fnC _ ->  do
     copyFile fn fnC
     x <- liftIO $ parseCFile (newGCC "gcc") Nothing [] fnC
     case x of
       Left parseError -> do
         logError $ "parse error: " <> displayShow parseError
         return Nothing
-      Right tu -> case runTrav_ (analyseAST tu) of
+      Right tu -> case typechecker tu of
           Left typeError -> do
             logError $ "type error: " <> displayShow typeError
             return Nothing