cogent/examples/search/Search.hs

{-# LANGUAGE DisambiguateRecordFields #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Main where

import Control.Arrow    (first)
import Data.Char        (isPrint)
import Data.Foldable    (foldl')
import Data.Monoid
import Data.List        (find)
import Data.Word
import Foreign
import Foreign.C.String hiding (CString)
import Foreign.C.Types
import Foreign.Marshal.Alloc
import Foreign.Ptr
import Foreign.Storable
import Test.QuickCheck hiding (Success)
import Test.QuickCheck.Gen
import Test.QuickCheck.Monadic

import FFI
import Search_Shallow_Desugar
import Util

spec_main = 
  case spec_find_str buffer "Cogent\NUL" of
    Nothing -> putStrLn "Not found!"
    Just nd -> putStrLn $ (key :: Node -> CString) nd

main = 
  let (R12 _ r) = find_str (R13 {p1 = (), p2 = buffer, p3 = "Cogent\NUL"} :: R13 _ _ _)
  in case r of
       None _  -> putStrLn "Not found!"
       Some nd -> putStrLn $ (key :: Node -> CString) nd

-- should find it!!!
bad_main = do
  let str = "libstartup-notification0"
      (R12 _ r) = find_str (R13 () buffer_1 str)
  case r of
    None _  -> putStrLn "Not found!"
    Some nd -> putStrLn $ (key :: Node -> CString) nd

-- -----------------------------------------------

buffer :: Buffer
buffer = [b10,b11,b12,b13] ++ map (fromIntegral . fromEnum) "Data61" ++ [0]
      ++ [b20,b21,b22,b23] ++ map (fromIntegral . fromEnum) "TS"     ++ [0]
      ++ [b30,b31,b32,b33] ++ map (fromIntegral . fromEnum) "Cogent" ++ [0]
  where l1@(b10,b11,b12,b13) = readWord32 7
        l2@(b20,b21,b22,b23) = readWord32 3
        l3@(b30,b31,b32,b33) = l1

buffer_1 = [9,0,0,0,108,105,98,115,101,112,111,108,49,13,0,0,0,108,105,98,112,114,111,116,111,98,117,102,49,48,19,0,0,0,108,105,98,112,97,110,103,111,99,97,105,114,111,45,49,46,48,45,48,24,0,0,0,108,105,98,115,116,97,114,116,117,112,45,110,111,116,105,102,105,99,97,116,105,111,110,48,10,0,0,0,108,105,98,115,111,109,98,111,107,51,20,0,0,0,108,105,98,112,121,116,104,111,110,51,46,53,45,109,105,110,105,109,97,108,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

pretty cs = concat $ map (\c -> let c' = (toEnum . fromIntegral $ c) in if isPrint c' then [c',','] else 'd':show c ++ ",") cs

keys :: [CString]
keys = words "libpam-pwquality libpam-runtime libpam-sss libpam0g libpango-1.0-0 libpango1.0-0 libpangocairo-1.0-0 \
  \ libpangoft2-1.0-0 libpangox-1.0-0 libpangoxft-1.0-0 libparams-validationcompiler-perl \
  \ libparse-debianchangelog-perl libparted-fs-resize0 libparted2 libpath-tiny-perl libpci3 libpciaccess0 \
  \ libpcre16-3 libpcre2-8-0 libpcre3 libpcsclite1 libpeas-1.0-0 libperl5.24 libplist3 libplot2c2 libpng12-0 \
  \ libpng16-16 libpopt0 libpostproc54 libpotrace0 libprotobuf10 libproxy-tools libproxy1v5 libpst4 libptexenc1 \
  \ libpulse-mainloop-glib0 libpulse0 libpulsedsp libpwquality1 libpython-all-dev libpython-dev \
  \ libpython-stdlib libpython2.7 libpython2.7-dev libpython2.7-minimal libpython2.7-stdlib libpython3-stdlib \
  \ libpython3.5 libpython3.5-minimal libpython3.5-stdlib libqca2 libqca2-plugins libqt5dbus5 libqt5network5 \
  \ libqt5opengl5 libqt5printsupport5 libqt5svg5 libqt5xml5 libqtwebkit4 libquadmath0 libraptor2-0 librasqal3 \
  \ libraw1394-11 libraw15 librdf0 libreadline7 libroar2 librsvg2-2 librsvg2-common librtmp1 librubberband2 \
  \ libsamplerate0 libsane libsane-common libsane-extras libsane-extras-common libsasl2-2 libsasl2-modules \
  \ libsasl2-modules-db libsasl2-modules-gssapi-mit libscalar-list-utils-perl libsdl-image1.2 libsdl2-2.0-0 \
  \ libsecret-1-0 libsecret-common libselinux1 libsemanage-common libsemanage1 libsepol1 libsm6 libsmartcols1 \
  \ libsmbclient libsndfile1 libsodium18 libsombok3 libsoprano4 libsoup-gnome2.4-1 libsoup2.4-1 libsoxr0 \
  \ libspecio-perl libspeechd2 libspeex1 libspeexdsp1 libsqlite3-0 libss2 libssh-gcrypt-4 libssl1.0.0 \
  \ libssl1.0.2 libssl1.1 libsss-idmap0 libsss-nss-idmap0 libsss-sudo libstartup-notification0 libstdc++-6-dev"

-- -----------------------------------------------

bufGen :: [CString] -> Gen Buffer
bufGen ws = frequency [(1, badBufGen ws), (3, goodBufGen ws)]

goodBufGen ws = do
  ns <- elements [1..6] 
  ws' <- take ns <$> shuffle ws
  let ls = map ((\(b0,b1,b2,b3) -> b0:b1:b2:b3:[]) . readWord32 . fromIntegral . length) ws' :: [[Word8]]
      ks = map (map (fromIntegral . fromEnum)) ws' :: [[Word8]]
  return $ concat (zipWith (++) ls ks) ++ replicate 500 0   -- assumptions is that the buffer is long enough

badBufGen  ws = shuffle =<< goodBufGen ws

keyGen :: [CString] -> Gen CString
keyGen = elements

-- -----------------------------------------------
-- properties

-- spec vs. haskell embedding (not very useful for our purpose)
prop_cogent_eq_haskell = forAll (bufGen keys) $ \buf ->
                         forAll (keyGen keys) $ \key ->
                           spec_find_str buf key `match_results` find_str (R13 () buf key)
  where
    match_results :: Maybe Node -> R12 SysState (V17 () (R9 Word32 CString)) -> Bool
    match_results (Just n1) (R12 _ (Some n2)) = (len :: Node -> Word32) n1 == (len :: Node -> Word32) n2 && (key :: Node -> CString) n1 == (key :: Node -> CString) n2
    match_results Nothing (R12 _ (None ())) = True
    match_results _ _ = False

-- exe spec vs. cogent impl'n
prop_model_to_cogent = monadicIO $ 
                         forAllM (bufGen keys) $ \buf ->
                         forAllM (keyGen keys) $ \key -> run $ do
                           let r1 = spec_find_str buf key
                           r2 <- cogent_find_str buf key
                           return $ r1 == r2

-- the refinement theorem. (now equiv. in the prop)
-- forall c'. c' = fc c, alpha c = a ===> exists a'. a' = fa a
-- abs spec vs. exe spec
prop_abs_to_model = forAll (bufGen keys) $ \buf ->
                    forAll (keyGen keys) $ \key ->
                      case alpha buf of
                        Nothing -> spec_find_str buf key == Nothing
                        Just ns -> spec_find_str buf key == abs_find_str ns key

-- -----------------------------------------------
-- data refinement

alpha :: [Word8] -> Maybe [Node]
alpha buf = snd $ foldl' (\(restb,mns) _ -> case mns of
                                      Nothing -> (restb, Nothing);
                                      Just ns -> case spec_deserialise_Node restb of
                                        Error _ -> (restb, Nothing)
                                        Success (n,buf') -> (buf', Just $ n:ns)) (buf,Just []) [0,1,2]

-- -----------------------------------------------
-- abstract spec

abs_find_str :: [Node] -> CString -> Maybe Node
abs_find_str (take 3 -> ns) s = find (\n -> (key :: Node -> CString) n == s) ns

-- -----------------------------------------------
-- concrete impl'n

foreign import ccall unsafe "main_pp_inferred.c ffi_find_str"
  c_find_str :: Ptr Ct27 -> IO (Ptr Ct29)

cogent_find_str :: [Word8] -> CString -> IO (Maybe Node)
cogent_find_str buf s = do
  pstate <- (malloc :: IO (Ptr CSysState))
  pbuf   <- newArray buf
  cstr <- newCString s
  pargs <- new $ Ct27 pstate (castPtr pbuf) cstr
  prets <- c_find_str pargs
  Ct29 _ (Ct28 (Ctag_t tag) none some) <- peek prets
  free pstate
  free pbuf
  free pargs
  if fromEnum tag == fromEnum tagEnumNone
    then return Nothing
    else if fromEnum tag == fromEnum tagEnumSome
      then do
        Ct4 l k <- peek some
        k' <- peekCString k
        return $ Just $ R9 (fromIntegral l) k'
      else case fromEnum tag of {}  -- impossible


-- -----------------------------------------------
-- executable spec

spec_find_str :: [Word8] -> CString -> Maybe Node
spec_find_str buf s = snd $ foldl' (\(restb, found) _ -> spec_cmp_inc restb found s) (buf, Nothing) [0,1,2]

spec_cmp_inc :: [Word8] -> Maybe Node -> CString -> ([Word8], Maybe Node)
spec_cmp_inc buf (Just n) _ = (buf, Just n)
spec_cmp_inc buf Nothing  s = 
  case spec_deserialise_Node buf of
    Success (n, buf') -> if s == (key :: Node -> CString) n then (buf', Just n) else (buf', Nothing)
    Error   err       -> (buf, Nothing)

spec_deserialise_Node :: [Word8] -> R (Node, [Word8]) ErrCode
spec_deserialise_Node buf = do
  (l, buf) <- spec_deserialise_U32 buf
  (k, buf) <- spec_deserialise_CString buf l
  return (R9 l k, buf)

spec_deserialise_U32 :: [Word8] -> R (Word32, [Word8]) ErrCode
spec_deserialise_U32 (b0:b1:b2:b3:bs) = Success (buildWord32 b0 b1 b2 b3, bs)
spec_deserialise_U32 _ = Error 1

spec_deserialise_CString :: [Word8] -> Word32 -> R (CString, [Word8]) ErrCode
spec_deserialise_CString buf len = 
  if fromIntegral len > length buf
    then Error 1
    else return $ (first $ map (toEnum . fromIntegral)) $ splitAt (fromIntegral len) buf

instance Functor (V16 e) where
  fmap _ (Error   e) = Error e
  fmap f (Success a) = Success (f a)

instance Applicative (V16 e) where
  pure = Success
  Error   e <*> _ = Error e
  Success f <*> a = fmap f a

instance Monad (V16 e) where
  return = pure
  Error e   >>= _ = Error e
  Success a >>= f = f a