Commit 5fc74657 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

removed readme

parents fc09945b 9dfc0411
.stack-work/
pwhile.cabal
*~
\ No newline at end of file
Copyright Author name here (c) 2018
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.
* Neither the name of Author name here nor the names of other
contributors may be used to endorse or promote products derived
from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# ecoimp
Expected Cost Analyser for Imperative Programs
\ No newline at end of file
import Distribution.Simple
main = defaultMain
set -o pipefail
tmout="120s"
opt="-degree 2 -dump-stats"
bin="./absynth-exe"
output="absynth-results.txt"
ostimeout="timeout"
pwd
cp /home/pldiae/absynth/source/absynth absynth-exe
cp -r /home/pldiae/absynth/gsl_caller .
cp -r /home/pldiae/absynth/llvm-reader .
rm -f ${output}
if [[ "$OSTYPE" == "darwin"* ]]; then
ostimeout="gtimeout"
fi
for ex in `find examples/oopsla -type f -name '*.imp' -o -name '*.absynth' | sort`
do
echo "------------------------------------" >> ${output}
echo $(basename "${ex}") >> ${output}
echo "------------------------------------" >> ${output}
tmp=/tmp/`basename ${ex}`.imp
cp $ex $tmp
echo -ne "`basename $ex`\t\t"
time $ostimeout $tmout $bin $opt $tmp | tee -a ${output} | tee "`basename $ex`.absynth-out" | head -n 1
code=$?
rm $tmp
code=$?
case $code in
124)
echo "[TIMEOUT]"
;;
esac
echo "" >> ${output}
done
echo "Done."
rm -f ${bin}
rm -rf gsl_caller
rm -rf llvm-reader
{-# LANGUAGE ImplicitParams #-}
import System.Environment
import qualified System.Timeout as Timeout
import Data.Maybe (listToMaybe)
import PWhile.InferEt
import Data.PWhile.CostExpression
import PWhile.Testbed.DSL
import PWhile.Parser
main :: IO ()
main = do
as <- getArgs
let ?to = 60
case as of
[fp] -> run1 fp Nothing
(fp:i:_) -> run1 fp (Just (read i))
_ -> print usage
where
usage = "<file>"
ec :: Program -> Maybe Int -> IO (Maybe (Result (CExp Rational)))
ec p i = listToMaybe <$> run (sel i) (ect (fst (gen p)) zero) where
sel = maybe Any Pick
run1 :: (?to :: Int) => FilePath -> Maybe Int -> IO ()
run1 fp i = do
programM <- fromFile fp
case programM of
Left err -> putStrLn (errorBundlePretty err)
Right p -> do
rM <- timeout ?to (ec p i)
case rM of
Nothing -> putStrLn "[Timeout]"
Just Nothing -> putStrLn "[Unknown]"
Just (Just res) -> putStrLn (showResult res)
timeout :: Int -> IO a -> IO (Maybe a)
timeout sec = Timeout.timeout (sec * 1000000)
{-# OPTIONS_GHC -fno-warn-type-defaults #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ViewPatterns #-}
import Control.Monad
import Data.Tree (drawForest)
import Data.List (intercalate, sort)
import qualified Data.Map.Strict as M
import Data.Ratio
import qualified Data.Set as S
import Data.Time
import qualified GUBS.Polynomial as P
import System.Environment
import System.FilePath (takeBaseName, (</>))
import System.Directory (createDirectoryIfMissing)
import System.IO
import System.IO.Unsafe (unsafePerformIO)
import System.Process (readCreateProcess, shell)
import qualified System.Timeout as Timeout
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.PWhile.CostExpression
import qualified PWhile.InferEt as InferEt
import PWhile.Parser (fromFile')
import PWhile.Testbed.DSL
import PWhile.Testbed.Examples
import PWhile.Util
-- A simple benchmarking tool.
--
-- The intended workflow is:
--
-- * make examples
-- * setup benchmark
-- * write result of benchmark to a file
-- * modify runime inference
-- * run benchmark against specified file
--
-- Problems are processed in order one by one as specified in the benchmark and
-- (de)serialised using Show and Read instances.
--
main :: IO ()
main = do
let bnch = oopsla
let ?to = 60
as <- getArgs
case as of
("--run":_) -> printBenchmark bnch
("--write":fp:_) -> writeBenchmark fp bnch
("--diff":fp:_) -> runBenchmarkAgainst fp bnch
("--tex":_) -> printBenchmarkTex bnch
("--md":_) -> printBenchmarkMd bnch
_ -> putStrLn usage
where
usage = unlines
[ "--run - run benchmark, print to stdout"
, "--write <fp> - write benchmark to fp"
, "--diff <fp> - test benchmark against fp"
, "--md <fp> - pretty print md format"
, "--tex - pretty print tex format" ]
type Name = String
type Time = String
data Benchmark = Benchmark Name [Problem]
data Problem = Problem Name Program
data Status = Timeout | Failed | Success (CExp Rational) InferEt.Log
deriving (Read, Show)
data Outcome = Outcome Name Status Time
deriving (Read, Show)
printBenchmark :: (?to :: Int) => Benchmark -> IO ()
printBenchmark (Benchmark _ ps) =
forM_ ps $ \p -> do
out <- run1 p
putStrLn (withColorCode ppOutcome out)
writeBenchmark :: (?to :: Int) => FilePath -> Benchmark -> IO ()
writeBenchmark fp (Benchmark _ ps) =
withFile fp WriteMode $ \hdl ->
forM_ ps $ \p@(Problem pid _) -> do
putStrLn ("processing ... " <> pid)
out <- run1 p
putStrLn (withColorCode (ppOutcome' " ") out)
hPrint hdl out
runBenchmarkAgainst :: (?to :: Int) => FilePath -> Benchmark -> IO ()
runBenchmarkAgainst fp (Benchmark _ ps) =
withFile fp ReadMode $ \hdl ->
forM_ ps $ \p -> do
old <- read <$> hGetLine hdl
new <- run1 p
putDiff old new
red, green, yellow :: String -> String
red xs = "\ESC[31m" ++ xs ++ "\ESC[m" -- worse
green xs = "\ESC[32m" ++ xs ++ "\ESC[m" -- better
yellow xs = "\ESC[33m" ++ xs ++ "\ESC[m" -- equal / incomparable
fill :: Int -> String -> String
fill i xs = take i $ take i xs ++ repeat ' '
ppOutcome' :: String -> Outcome -> String
ppOutcome' pfx (Outcome pid st t) =
pfx <> fill (50 - length pfx) pid <> ": " <> take 5 t <> "s : " <> ppStatus st
ppOutcome :: Outcome -> String
ppOutcome = ppOutcome' ""
withColorCode :: (Outcome -> String) -> Outcome -> String
withColorCode f o@(Outcome _ st _) = k st (f o) where
k Success{} = green
k _ = red
ppStatus :: Status -> String
ppStatus Timeout = "[Timeout]"
ppStatus Failed = "[Failed ]"
ppStatus (Success cexp _) = "[Success]" <> " " <> renderPretty cexp
putDiff :: Outcome -> Outcome -> IO ()
putDiff old@(Outcome pid1 st1 _) new@(Outcome pid2 st2 _)
| pid1 /= pid2 = putStrLn $ red $ "[Error] " <> pid1 <> " /= " <> pid2
| otherwise = do
putStrLn $ ppOutcome old
putStrLn $ cmp st1 st2 $ ppOutcome' " " new
cmp :: Status -> Status -> String -> String
cmp (Success _ _) (Success _ _) = yellow
cmp _ (Success _ _) = green
cmp (Success _ _) _ = red
cmp _ _ = yellow
run1 :: (?to :: Int) => Problem -> IO Outcome
run1 (Problem pid p) = do
start <- getCurrentTime
let exe = InferEt.runAny . flip InferEt.ect zero . fst $ gen p
rM <- timeout ?to exe
let stM = case rM of
Nothing -> Timeout
Just(Just (InferEt.Success cexp log)) -> Success cexp log
_ -> Failed
end <- stM `seq` getCurrentTime
let time = show $ diffUTCTime end start
return $ Outcome pid stM time
timeout :: Int -> IO a -> IO (Maybe a)
timeout sec = Timeout.timeout (sec * 1000000)
absynth :: Benchmark
absynth = Benchmark "absynth"
[ Problem "linear/2drdwalk" absynth2drdwalk
, Problem "linear/bayesian_Network" absynthBayesianNetwork
, Problem "linear/ber" absynthBer
, Problem "linear/bin" absynthBin
, Problem "linear/C4B_t09" absynthC4Bt09
, Problem "linear/C4B_t13" absynthC4Bt13
, Problem "linear/C4B_t15" absynthC4Bt15
, Problem "linear/C4B_t19" absynthC4Bt19
, Problem "linear/C4B_t30" absynthC4Bt30
, Problem "linear/C4B_t61" absynthC4Bt61
, Problem "linear/condand" absynthCondand
, Problem "linear/cooling" absynthCooling
, Problem "linear/filling_vol" absynthFillingVol
-- , Problem "linear/hyper" absynthHyper
, Problem "linear/linear01" absynthLinear01
, Problem "linear/trapped_miner" absynthTrappedMiner
, Problem "linear/prnes" absynthPrnes
, Problem "linear/prspeed" absynthPrspeed
, Problem "linear/race" absynthRace
, Problem "linear/rdseql" absynthRdseql
, Problem "linear/rdspeed" absynthRdspeed
, Problem "linear/rdwalk" absynthRdwalk
, Problem "linear/robot" absynthRobot
, Problem "linear/roulette" absynthRoulette
, Problem "linear/rejection_sampling" absynthSampling
, Problem "linear/sprdwalk" absynthSprdwalk
, Problem "polynomial/complex" absynthComplex
, Problem "polynomial/multirace" absynthMultirace
, Problem "polynomial/pol04" absynthPol04
, Problem "polynomial/pol05" absynthPol05
, Problem "polynomial/pol06" absynthPol06
, Problem "polynomial/pol07" absynthPol07
, Problem "polynomial/Rdbub" absynthRdbub
, Problem "polynomial/trader" absynthTrader
, Problem "couponCollector" couponCollector
]
{-# NOINLINE pldi #-}
pldi :: Benchmark
pldi = unsafePerformIO $ Benchmark "pldi" <$> do
fps <- sort . lines <$> readCreateProcess (shell "find examples/pldi -type f") mempty
forM fps $ \fp -> Problem fp <$> fromFile' fp
{-# NOINLINE oopsla #-}
oopsla :: Benchmark
oopsla = unsafePerformIO $ Benchmark "oopsla" <$> do
fps <- sort . lines <$> readCreateProcess (shell "find examples/oopsla -type f -name '*.imp' -o -name '*.pwhile' | sort") mempty
forM fps $ \fp -> Problem fp <$> fromFile' fp
printBenchmarkTex :: (?to :: Int) => Benchmark -> IO ()
printBenchmarkTex (Benchmark _ ps) =
forM_ ps $ \p -> do
out <- run1 p
putStrLn (texOutcome out)
where
texOutcome (Outcome n s t) = unwords
[ escaped (takeBaseName n)
,"&"
, math (texStatus s)
,"&"
, math (take 5 t)
, "\\\\"]
texStatus Timeout = "timeout"
texStatus Failed = "?"
texStatus (Success c _) = texCExp c
escaped [] = []
escaped ('_':xs) = '\\' : '_' : escaped xs
escaped (x:xs) = x : escaped xs
math s = "$" <> s <> "$"
-- parens t = "(" <> t <> ")"
-- braces t = "{" <> t <> "}"
-- a <+> b = a <> " " <> b
-- mulf = "\\mulf"
-- addf = "\\plusf"
-- divf = "\\divf"
-- texInt i = "\\bm" <> braces (show i)
-- texFrac q
-- | denominator q == 1 = texInt (numerator q)
-- | otherwise = braces (texInt (numerator q)) <> divf <> braces (texInt (denominator q))
-- BExp
-- texDisj (Disj (S.toList -> ds)) = intercalate " \\vee " (map texConj ds)
-- texConj (Conj (S.toList -> es)) = intercalate " \\wedge " (map texLit es)
-- texLit (e1 :>=: e2) = texExp e1 <+> "\\ge" <+> texExp e2
-- texExp :: Exp -> String
-- texExp = show . PP.pretty
texCExp = show . PP.pretty
printBenchmarkMd :: (?to :: Int) => Benchmark -> IO ()
printBenchmarkMd (Benchmark _ ps) = do
createDirectoryIfMissing True "results/"
putStrLn rule
putStrLn heading
putStrLn rule
forM_ ps $ \p -> do
out <- run1 p
putStrLn (mdOutcome out)
writeLog out
putStrLn ""
putStrLn rule
where
a <+> b = a <> " " <> b
link txt target = "[" <> txt <> "](" <> target <> ")"
code txt = "`" <> txt <> "`"
(l1,l2,l3) = (40,160,5)
rule = replicate l1 '-' <+> replicate l2 '-' <+> replicate l3 '-'
heading = fill l1 "Example" <+> fill l2 "Result" <+> fill l3 "secs"
mdOutcome (Outcome n s t) =
fill l1 (link fn ("examples/" <> fn <> ".imp"))
<+> fill l2 (link (code (mdStatus s)) ("results/" <> fn <> ".out"))
<+> fill l3 (take 5 t)
where
fn = takeBaseName n
mdStatus Timeout = "timeout"
mdStatus Failed = "?"
mdStatus (Success c _) = renderWidth l2 c
writeLog (Outcome n s _) = writeFile ("results" </> takeBaseName n <> ".out") (logStr s) where
logStr (Success _ l) = drawForest l
logStr _ = ""
renderWidth :: PP.Pretty a => Int -> a -> String
renderWidth w c = PP.displayS (PP.renderPretty 1.0 w (PP.pretty c)) ""
This diff is collapsed.
Bound: 2 max(0, 1 - d + n)
Degree: 1
Statistics:
Weakenings inserted per function:
38 for f
Number of LP variables: 7097
Number of LP constraints: 5084
Maximum focus functions in use: 75
LP solver time ratio: 36%
Total runtime: 0.278s
Bound: 8.27273 max(0, x)
Degree: 1
Statistics:
Weakenings inserted per function:
9 for f
Number of LP variables: 1231
Number of LP constraints: 991
Maximum focus functions in use: 50
LP solver time ratio: 40%
Total runtime: 0.062s
Bound: 1.25 max(0, x) + max(0, y)
Degree: 1
Statistics:
Weakenings inserted per function:
10 for f
Number of LP variables: 550
Number of LP constraints: 425
Maximum focus functions in use: 21
LP solver time ratio: 42%
Total runtime: 0.018s
Bound: max(0, -1 + x) + max(0, x)
Degree: 1
Statistics:
Weakenings inserted per function:
9 for f
Number of LP variables: 961
Number of LP constraints: 760
Maximum focus functions in use: 44
LP solver time ratio: 29%
Total runtime: 0.020s
Bound: max(0, 51 + i + k) + 2 max(0, i)
Degree: 1
Statistics:
Weakenings inserted per function:
8 for f
Number of LP variables: 663
Number of LP constraints: 586
Maximum focus functions in use: 30
LP solver time ratio: 49%
Total runtime: 0.015s
Bound: 0.333333 max(0, 2 + x) + 0.166667 max(0, 2 + x) max(0, 2 + y)
Degree: 2
Statistics:
Weakenings inserted per function:
5 for f
Number of LP variables: 7702
Number of LP constraints: 5991
Maximum focus functions in use: 654
LP solver time ratio: 45%
Total runtime: 0.228s
Bound: 0.0606061 max(0, -1 + l) + max(0, l)
Degree: 1
Statistics:
Weakenings inserted per function:
7 for f
Number of LP variables: 364
Number of LP constraints: 297
Maximum focus functions in use: 20
LP solver time ratio: 72%
Total runtime: 0.017s
Bound: 2 max(0, n - x)
Degree: 1
Statistics:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment