latest changes

cbits/demangler.cpp

@@ -0,0 +1,19 @@
+#include <cxxabi.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include "demangler.h"
+
+char* demangler(char *argv){
+
+size_t sz = 256;
+char *buffer = (char *)malloc(sz);
+char *symbol = argv;
+
+char *begin = strchr(symbol, '_');
+char *demangled_name = NULL;
+int status;
+demangled_name = abi::__cxa_demangle(begin, buffer, &sz, &status);
+
+return demangled_name;
+}

include/demangler.h

@@ -0,0 +1,4 @@
+#ifndef DEMANGLER_H
+#define DEMANGLER_H
+char *demangler(char *argv);
+#endif

llvmvf.cabal

@@ -21,6 +21,10 @@ Executable llvmvf
                     , llvm-base
                     , llvm
                     , smtlib        == 1.0
+                    , demangler     == 1.0
     Hs-Source-Dirs:   src/
-    Extensions: 	  TypeOperators, FlexibleInstances, TypeSynonymInstances, DeriveDataTypeable
-    ghc-options:     -O3 -rtsopts 
+    include-dirs: include
+    C-Sources:        cbits/demangler.cpp
+    Extensions:       TypeOperators, FlexibleInstances, TypeSynonymInstances, DeriveDataTypeable
+    ghc-options:      -O3 -rtsopts 
+    extra-libraries: stdc++

src/Concurrent/Model.hs

@@ -10,7 +10,7 @@ import qualified Data.IntMap as IM
 import qualified Data.Map as Map
 
 import Language.LLVMIR
-import Language.LLVMIR.Printer.Module
+import Language.LLVMIR.Printer.Module hiding (emptyFunction)
 
 import Language.SMTLib2.Base
 
@@ -51,6 +51,10 @@ data Model t = Model { nmdtys :: NamedTypes
                      } 
 
 data Process = Process { ident :: String, unProc :: Function }
+
+emptyProcess :: Process
+emptyProcess = Process "undefined" emptyFunction
+
 type Declarations = Map.Map String (Type, Parameters) 
 type Processes = IM.IntMap Process
 
@@ -201,8 +205,6 @@ type Transaction = [TTransition]
 -- Happens-before
 
 
-
--- Printing
 instance Show (Model t) where
   show (Model nmdtys gvars mainf procs decls) = show mainf ++ "\n" ++ show procs ++ "\n" ++ show decls
 
@@ -212,3 +214,14 @@ instance Pretty Function where
 instance Show Process where
   show (Process i f) = show $ pretty f
 
+
+-- Printing
+{-instance Show (Model t) where
+  show (Model nmdtys gvars mainf procs decls) = show mainf ++ "\n" ++ show procs ++ "\n" ++ show decls
+
+instance Pretty Function where
+    pretty f = pp_Syn_Function $ wrap_Function (sem_Function f) $ Inh_Function {}
+
+instance Show Process where
+  show (Process i f) = show $ pretty f
+-}

src/Concurrent/Model/Analysis/ControlFlow.ag

@@ -97,7 +97,9 @@ attr Functions
 
 sem Functions
   | Entry 
-      lhs.bbentrypc = Map.insert @key @val.bbentrypc @tl.bbentrypc
+      lhs.bbentrypc = if @key == "sc_main" 
+                      then @tl.bbentrypc
+                      else Map.insert @key @val.bbentrypc @tl.bbentrypc
 
 attr Function BasicBlocks BasicBlock Instructions Instruction
   syn entrypc :: {Int}
@@ -115,7 +117,7 @@ sem Function
 
 sem BasicBlocks
   | Nil
-      lhs.entrypc = error "'entrypc' of an empty bb list"
+      lhs.entrypc = -1 -- error "'entrypc' of an empty bb list"
   | Cons
       lhs.entrypc = @hd.entrypc
 

src/Concurrent/Model/Encoder.hs

@@ -4,7 +4,7 @@
 -- Copyright :  (c) 2012 Marcelo Sousa
 -------------------------------------------------------------------------------
 
-module Concurrent.Model.Encoder (encode) where
+module Concurrent.Model.Encoder (encode,encodeSysC) where
 
 import Concurrent.Model                    hiding (State)
 
@@ -47,13 +47,27 @@ encode m@Model{..} k = let ccfg@ControlFlow{..} = controlflow m
                            (smod, sf) = runState (encModel m k) s0                             
                        in smod --trace (show s0 ++ show sf) $ smod
 
+encodeSysC :: (SCModel t) => Model t -> Int -> SMod
+encodeSysC m@Model{..} k = let ccfg@ControlFlow{..} = controlflow m
+                               tvs = Map.map (\pci -> ThreadState pci Map.empty) $ Map.delete "undefined" cte  -- ^ Set the initial PC for each thread
+                               s0  = GlobalState Map.empty (-1) Map.empty tvs                                  -- ^ Initial state
+                               (smod, sf) = runState (encSysCModel m k) s0                             
+                           in smod --trace (show s0 ++ show sf) $ smod
+
 -- | Main encode function.
 encModel :: (SCModel t) => Model t -> Int -> State GlobalState SMod
 encModel m k = do tyenc <- encNmdTys  m   -- ^ Encode Named Types
                   gvenc <- encGlobals m   -- ^ Encode Global Variables
                   menc  <- encFunctions m k  -- ^ Encode Functions
                   return $ nub $ preamble ++ tyenc ++ gvenc ++ menc ++ final
 
+-- | Main encode function.
+encSysCModel :: (SCModel t) => Model t -> Int -> State GlobalState SMod
+encSysCModel m k = do --tyenc <- encNmdTys  m   -- ^ Encode Named Types
+                      --gvenc <- encGlobals m   -- ^ Encode Global Variables
+                      menc  <- encSCFunctions m k  -- ^ Encode Functions
+                      return $ nub $ preamble ++ menc ++ final
+
 -- | Initial part of an smt module
 preamble :: SExpressions
 preamble = [ setlogic QF_AUFBV           -- ^ Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.
@@ -110,6 +124,18 @@ encFunctions m@Model{..} k = do gs@GlobalState{..} <- get
                                 return $ s ++ se ++ pcs ++ [ assert $ wrap sAnd sexprs ] ++ cpcs ++ [ assert csexprs ] 
                                 --trace ("----\n" ++ show p ++ "--- ---\n" ++ show l) $ return $ s ++ se ++ pcs ++ [ assert $ wrap sAnd sexprs ] ++ cpcs ++ [ assert csexprs ] 
 
+encSCFunctions :: (SCModel t) => Model t -> Bound -> State GlobalState SExpressions
+encSCFunctions m@Model{..} k = do gs@GlobalState{..} <- get
+                                  let ccfg@ControlFlow {..} = controlflow m 
+                                      fs = toFunctions procs 
+                                      (s,p)  = preEncoder fs defsorts decls
+                                      se = preEncode p
+                                      l = Map.empty
+                                      --(l, pcs, sexprs) = encodeMain    (unProc mainf) p decls
+                                      --(cpcs, csexprs)  = encodeThreads (toFunctions procs)  k p l (Map.delete "main" cte) $ Map.delete "main" cfg 
+                                  trace (show $ fails p) $ return $ s ++ se -- ++ cpcs ++ [ assert csexprs ] 
+                                --trace ("----\n" ++ show p ++ "--- ---\n" ++ show l) $ return $ s ++ se ++ pcs ++ [ assert $ wrap sAnd sexprs ] ++ cpcs ++ [ assert csexprs ] 
+
 preEncode :: PreEncoder -> SExpressions
 preEncode p@PreEncoder{..} = Map.foldrWithKey (\i (t, pcs) se -> (concatMap (\(_,c) -> (declSVar (i ++ show c) t sortEnv):[]) (zip pcs [0..])) ++ se ) [] fStore 
 

src/Concurrent/Model/Encoder/PreEncoder.ag

@@ -48,7 +48,6 @@ sem Instruction
       mres.sortexpr = fst <$> Map.lookup @loc.ty @lhs.sortEnv
       lhs.argToPar = foldr (\((Parameter v _,a),i) m -> Map.insert (@pc.self, i, a) v m) Map.empty $ zip (zip (getFnParams @lhs.fdcl @callee.self) @args.self) [0..]
       lhs.locals   = if @mres.ident  == ""              then Map.empty  else Map.singleton @mres.ident @loc.ty
-      lhs.fails    = if @callee.self == "__assert_fail" then [@pc.self] else []
       lhs.declexpres = @mres.declexpr
   | CreateThread
       loc.thn = getFnValueName $ @args.self !! 2
@@ -99,6 +98,8 @@ sem Instruction
       ty.mn       = Nothing
       lhs.locals  = Map.singleton @id.ident @ty.self
       lhs.declexpres = @id.declexpr
+  | WaitEvent NotifyEvent WaitTime 
+      lhs.fails    = [@pc.self] 
 
 {
 -- | Get return type