From 7f250ea1ff2d320501981a93c902552ca9f3e35c Mon Sep 17 00:00:00 2001 From: Gabriela Mafra Date: Sun, 7 Aug 2022 19:37:21 -0300 Subject: [PATCH] Add extra fields to configuration file --- ConfigParser.hs | 24 ++++++++++++++--- Elixir.hs | 17 ++++++------ Main.hs | 39 +++++++++++++++------------- elixir/lib/generated_code/er_c20.ex | 4 +-- tla_specifications/ERC20/config.json | 9 ++++++- 5 files changed, 61 insertions(+), 32 deletions(-) diff --git a/ConfigParser.hs b/ConfigParser.hs index acc1016..de91116 100644 --- a/ConfigParser.hs +++ b/ConfigParser.hs @@ -14,7 +14,7 @@ jsonFile :: FilePath jsonFile = "config-sample.json" data DistributionConfig = - Config [ProcessConfig] [String] [ConstantConfig] + Config [ProcessConfig] [String] [ConstantConfig] String String String String String [BlackboxTest] String deriving (Show, Generic) data ProcessConfig = @@ -25,13 +25,24 @@ data ConstantConfig = Constant String H.Value deriving (Show, Generic) +data BlackboxTest = + Test String String + deriving (Show, Generic) + instance FromJSON DistributionConfig where parseJSON = withObject "DistribuitionConfig" $ \obj -> do ps <- obj .: "processes" vs <- obj .: "shared_variables" cs <- obj .: "constants" - return (Config ps vs cs) + i <- obj .: "init" + n <- obj .: "next" + f <- obj .: "input_format" + file <- obj .: "input_file" + g <- obj .: "state_graph" + bs <- obj .: "blackbox_tests" + dest <- obj .: "destination_folder" + return (Config ps vs cs i n f file g bs dest) instance FromJSON ProcessConfig where parseJSON = @@ -51,6 +62,13 @@ instance FromJSON ConstantConfig where Left e -> fail ("Invalid value in:" ++ show v ++ ". Error: " ++ show e) Right val -> return (Constant n val) +instance FromJSON BlackboxTest where + parseJSON = + withObject "BlackboxTest" $ \obj -> do + n <- obj .: "name" + t <- obj .: "trace" + return (Test n t) + parseConfig :: FilePath -> IO (Either String DistributionConfig) parseConfig file = do content <- B.readFile file @@ -59,4 +77,4 @@ parseConfig file = do -- main = parseJson jsonFile >>= print processNames :: DistributionConfig -> [String] -processNames (Config ps _ _) = map (\(PConfig n _) -> n) ps +processNames (Config ps _ _ _ _ _ _ _ _ _) = map (\(PConfig n _) -> n) ps diff --git a/Elixir.hs b/Elixir.hs index a376d06..7afab3d 100644 --- a/Elixir.hs +++ b/Elixir.hs @@ -10,13 +10,13 @@ import Helpers import Snippets generate :: Spec -> DistributionConfig -> [(String, ElixirCode)] -generate (Spec m i n ds) (Config ps shared consts) = +generate (Spec m i n ds) (Config ps shared consts _ _ _ _ _ _ _) = let defs = filter (not . (specialDef i n)) ds cs = findConstants ds vs = findVariables ds header = moduleHeader (moduleName m) m shared False -- defNext = findIdentifier n ds - base = baseSpec header cs vs defs + base = baseSpec header cs vs defs consts in (moduleName m, base):map (generateForProcess m n vs cs defs) ps generateStarter :: Spec -> String -> (String, ElixirCode) @@ -52,24 +52,25 @@ spec m h cs vs ds dn = , "\nend\n\n" ] -baseSpec :: String -> [Constant] -> [Variable] -> [Definition] -> ElixirCode -baseSpec h cs vs ds = +baseSpec :: String -> [Constant] -> [Variable] -> [Definition] -> [ConstantConfig] -> ElixirCode +baseSpec h cs vs ds consts = let g = map (\c -> (c, "const")) cs ++ map (\v -> (v, "variable")) vs in concat [ h - , ident (concat [constants cs, mapAndJoin (definition g) ds, "\n", decideAction, "\n", waitLockFunction]) + , ident (concat [constants cs consts, mapAndJoin (definition g) ds, "\n", decideAction, "\n", waitLockFunction]) , "\nend\n\n" ] {-- \vdash_const --} -- (CONST) -constants :: [Constant] -> ElixirCode -constants cs = +constants :: [Constant] -> [ConstantConfig] -> ElixirCode +constants cs vs = unlines (map (\c -> let s = snake c - decl = "@" ++ s ++ " \"\"\n" + (Constant _ val) = head (dropWhile (\(Constant n _) -> n /= c) vs) + decl = "@" ++ s ++ " " ++ value [] val ++ "\n" acc = "def " ++ s ++ ", do: @" ++ s ++ "\n\n" in decl ++ acc) cs) diff --git a/Main.hs b/Main.hs index bcd3ceb..7441c88 100644 --- a/Main.hs +++ b/Main.hs @@ -1,6 +1,6 @@ import System.Environment -import ConfigParser (parseConfig, processNames) +import ConfigParser import Control.Applicative import Elixir import Head @@ -8,30 +8,33 @@ import Helpers import JSONParser (parseJson) import Parser -filename p = "elixir/lib/generated_code/" ++ snake p ++ ".ex" +filename dest p = dest ++ "/lib/generated_code/" ++ snake p ++ ".ex" -writeCode m (p, code) = - let f = filename p +writeCode dest m (p, code) = + let f = filename dest p in writeFile f code >> return f -writeStarter (name, code) = - let f = "elixir/lib/mix/tasks/" ++ snake name ++ "_starter.ex" +writeStarter dest (name, code) = + let f = dest ++ "/lib/mix/tasks/" ++ snake name ++ "_starter.ex" in writeFile f code >> return f -convert name init next config (m, ds) = do - files <- mapM (writeCode name) (generate (Spec m init next ds) config) - starter <- mapM (writeStarter . generateStarter (Spec m init next ds)) (processNames config) +convert name init next dest config (m, ds) = do + files <- mapM (writeCode dest name) (generate (Spec m init next ds) config) + starter <- mapM (writeStarter dest . generateStarter (Spec m init next ds)) (processNames config) return (starter, files) main = do - (mode:name:i:n:configFile:_) <- getArgs + (configFile:_) <- getArgs config <- parseConfig configFile - ls <- - if mode == "tla" - then parseTla name - else parseJson name - case liftA2 (convert name i n) config ls of + case config of Left e -> putStrLn e - Right f -> do - a <- f - putStrLn ("Elixirs files written to " ++ show a) + Right (Config _ _ _ i n mode file _ _ dest) -> do + ls <- + if mode == "tla" + then parseTla file + else parseJson file + case liftA2 (convert file i n dest) config ls of + Left e -> putStrLn e + Right f -> do + a <- f + putStrLn ("Elixirs files written to " ++ show a) diff --git a/elixir/lib/generated_code/er_c20.ex b/elixir/lib/generated_code/er_c20.ex index be8fdd4..707fd90 100644 --- a/elixir/lib/generated_code/er_c20.ex +++ b/elixir/lib/generated_code/er_c20.ex @@ -7,11 +7,11 @@ defmodule ERC20 do ] end require Oracle - @amounts [0, 100, 500] + @amounts MapSet.new([0, 100, 500]) def amounts, do: @amounts - @addr ["alice_OF_ADDR", "bob_OF_ADDR"] + @addr MapSet.new(["alice_OF_ADDR", "bob_OF_ADDR"]) def addr, do: @addr diff --git a/tla_specifications/ERC20/config.json b/tla_specifications/ERC20/config.json index 1acb032..11007af 100644 --- a/tla_specifications/ERC20/config.json +++ b/tla_specifications/ERC20/config.json @@ -35,5 +35,12 @@ "name": "AMOUNTS", "value": "{0, 100, 500}" } - ] + ], + "init": "Init", + "next": "Next", + "input_format": "json", + "input_file": "ERC20.json", + "state_graph": "states.json", + "blackbox_tests": [{"name": "exploit_trace", "trace": "trace.out"}], + "destination_folder": "../../elixir" }