<commit_before>{- |
Module      :  Z3Backend
Description :  The Z3 backend for symbolic
Copyright   :  (c) 2014—2015 The F2J Project Developers (given in AUTHORS.txt)
License     :  BSD3

Maintainer  :  Weixin <<EMAIL>>
Stability   :  unstable
Portability :  portable

Symbolic evaluator will generates all possible execution paths for a given program. We use Z3 to kick out those infeasible execution paths.
-}

module Z3Backend where

import           Control.Monad
import           Control.Monad.IO.Class       (liftIO)
import qualified Data.IntMap                  as IntMap
import           Data.Maybe                   (fromJust)
import           Prelude                      hiding (EQ, GT, LT)
import           PrettyUtils
import qualified Src                          as S
import           SymbolicEvaluator
import           SystemFI
import           Text.PrettyPrint.ANSI.Leijen
import           Z3.Monad                     hiding (Z3Env)
import Data.Map (Map, fromList)

data Z3Env = Z3Env { index                      :: Int
                   , boolSort, intSort, adtSort :: Sort
                   -- , constrFuns :: SConstructor -> ConstrFun
                   , symVars                    :: IntMap.IntMap AST
                   , funVars                    :: IntMap.IntMap FuncDecl
                   , target                     :: Doc -> SymValue -> Z3 ()
                   }

solve :: Expr () ExecutionTree -> IO ()
solve = solve' 20

solve' :: Int -> Expr () ExecutionTree -> IO ()
solve' stop e =
    evalZ3 $ do
      int <- mkIntSort
      bool <- mkBoolSort
      -- All datatypes are treated as one adt
      adt <- mkStringSymbol "adtSort" >>= mkUninterpretedSort
      -- prelude (int,bool,adt) ts

      let (tree, i) = exec $ seval e
          env = Z3Env { index = i
                      , intSort = int, boolSort = bool , adtSort = adt
                      -- , constrFuns = cfs
                      , symVars = IntMap.empty
                      , funVars = IntMap.empty
                      , target = defaultTarget
                      }
      pathsZ3 env tree [] stop

defaultTarget :: Doc -> SymValue -> Z3 ()
defaultTarget s e = liftIO $ putDoc $ s <+> evalTo <+> pretty e <> linebreak

pathsZ3 :: Z3Env -> ExecutionTree -> [Doc] -> Int -> Z3 ()
pathsZ3 _ _ _ stop | stop <= 0 = return ()
pathsZ3 env (Exp e) conds _ =
    target env (foldr1 combineWithAnd conds') e<commit_msg>Print the model when the leaf is False<commit_after>{- |
Module      :  Z3Backend
Description :  The Z3 backend for symbolic
Copyright   :  (c) 2014—2015 The F2J Project Developers (given in AUTHORS.txt)
License     :  BSD3

Maintainer  :  <NAME> <<EMAIL>>
Stability   :  unstable
Portability :  portable

Symbolic evaluator will generates all possible execution paths for a given program. We use Z3 to kick out those infeasible execution paths.
-}

module Z3Backend where

import           Control.Monad
import           Control.Monad.IO.Class       (liftIO)
import qualified Data.IntMap                  as IntMap
import           Data.Maybe                   (fromJust)
import           Prelude                      hiding (EQ, GT, LT)
import           PrettyUtils
import qualified Src                          as S
import           SymbolicEvaluator
import           SystemFI
import           Text.PrettyPrint.ANSI.Leijen
import           Z3.Monad                     hiding (Z3Env)
import Data.Map (Map, fromList)

data Z3Env = Z3Env { index                      :: Int
                   , boolSort, intSort, adtSort :: Sort
                   -- , constrFuns :: SConstructor -> ConstrFun
                   , symVars                    :: IntMap.IntMap AST
                   , funVars                    :: IntMap.IntMap FuncDecl
                   , target                     :: Doc -> SymValue -> Z3 ()
                   }

solve :: Expr () ExecutionTree -> IO ()
solve = solve' 10

solve' :: Int -> Expr () ExecutionTree -> IO ()
solve' stop e =
    evalZ3 $ do
      int <- mkIntSort
      bool <- mkBoolSort
      -- All datatypes are treated as one adt
      adt <- mkStringSymbol "adtSort" >>= mkUninterpretedSort
      -- prelude (int,bool,adt) ts

      let (tree, i) = exec $ seval e
          env = Z3Env { index = i
                      , intSort = int, boolSort = bool , adtSort = adt
                      -- , constrFuns = cfs
                      , symVars = IntMap.empty
                      , funVars = IntMap.empty
                      , target = defaultTarget
                      }
      pathsZ3 env tree [] stop

defaultTarget :: Doc -> SymValue -> Z3 ()
defaultTarget s (SBool False) =
    do liftIO $ putDoc $ text "Counter example:" <$> s <+> evalTo <+> text "False" <> linebreak
       withModel ((>>= (liftIO . putStrLn)) . showModel)
       return ()
defaultTarget s e = liftIO $ putDoc $ s <+> evalTo <+> pretty e <> linebreak

pathsZ3 :: Z3Env -> ExecutionTree -> [Doc] -> Int -> Z3 ()
pathsZ3 _ _ _ stop | stop <= 0 = return ()
pathsZ3 env (Exp e) conds _ =
    target env (foldr1 combineWithAnd conds') e
{'fraction_non_alphanumeric': 0.08669950738916256, 'fraction_numerical': 0.012610837438423646, 'mean_word_length': 1.5623422513881877, 'pattern_counts': {'":': 0, '<': 26, '<?xml version=': 0, '>': 48, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1825430', 'n_tokens_mistral': 1475, 'n_tokens_neox': 1418, 'n_words': 454}