Add extra fields to configuration file

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

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 ++ " \"<value for " ++ c ++ ">\"\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)

Main.hs

@@ -1,37 +1,40 @@
 import System.Environment
 
-import ConfigParser (parseConfig, processNames)
+import ConfigParser
 import Control.Applicative
 import Elixir
 import Head
 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)

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
 
 

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"
 }