Fixing up call signature generation

src/EVM/Dapp.hs

@@ -100,7 +100,7 @@ mkSig method
   | "check" `isPrefixOf` testname = Just (Sig testname argtypes)
   | otherwise = Nothing
   where
-    testname = method.methodSignature
+    testname = method.name
     argtypes = snd <$> method.inputs
 
 findUnitTests :: Text -> ([SolcContract] -> [(Text, [Sig])])

src/EVM/Solvers.hs

@@ -129,10 +129,10 @@ withSolvers solver count threads timeout cont = do
         when (conf.dumpQueries) $ writeSMT2File smt2 fileCounter "abstracted"
         if (isJust fuzzResult)
           then do
-            when (conf.debug) $ putStrLn $ "Cex found via fuzzing:" <> (show fuzzResult)
+            when (conf.debug) $ putStrLn $ "   Cex found via fuzzing:" <> (show fuzzResult)
             writeChan r (Sat $ fromJust fuzzResult)
           else if not conf.onlyCexFuzz then do
-            when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex"
+            when (conf.debug) $ putStrLn "   Fuzzing failed to find a Cex"
             -- reset solver and send all lines of provided script
             out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
             case out of

src/EVM/SymExec.hs

@@ -596,16 +596,16 @@ verify
 verify solvers opts preState maybepost = do
   conf <- readConfig
   let call = mconcat ["prefix 0x", getCallPrefix preState.state.calldata]
-  when conf.debug $ liftIO $ putStrLn $ "Exploring call " <> call
+  when conf.debug $ liftIO $ putStrLn $ "   Exploring call " <> call
 
   exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters opts.loopHeuristic preState runExpr
   when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
   liftIO $ do
-    when conf.debug $ putStrLn "Simplifying expression"
+    when conf.debug $ putStrLn "   Simplifying expression"
     let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
     when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
 
-    when conf.debug $ putStrLn $ "Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
+    when conf.debug $ putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
 
     let flattened = flattenExpr expr
     when (any isPartial flattened) $ do

src/EVM/UnitTest.hs

@@ -114,15 +114,19 @@ makeVeriOpts opts =
 -- | Top level CLI endpoint for hevm test
 unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m Bool
 unitTest opts (Contracts cs) = do
-  let unitTests = findUnitTests opts.match $ Map.elems cs
-  results <- concatMapM (runUnitTestContract opts cs) unitTests
+  let unitTestContrs = findUnitTests opts.match $ Map.elems cs
+  conf <- readConfig
+  when conf.debug $ liftIO $ do
+    putStrLn $ "Found " ++ show (length unitTestContrs) ++ " unit test contract(s) to test:"
+    let x = map (\(a,b) -> "  --> " <> a <> "  ---  functions: " <> (Text.pack $ show b)) unitTestContrs
+    putStrLn $ unlines $ map Text.unpack x
+  results <- concatMapM (runUnitTestContract opts cs) unitTestContrs
   pure $ and results
 
 -- | Assuming a constructor is loaded, this stepper will run the constructor
 -- to create the test contract, give it an initial balance, and run `setUp()'.
 initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper Concrete s ()
 initializeUnitTest opts theContract = do
-
   let addr = opts.testParams.address
 
   Stepper.evm $ do
@@ -157,11 +161,9 @@ runUnitTestContract
   -> Map Text SolcContract
   -> (Text, [Sig])
   -> m [Bool]
-runUnitTestContract
-  opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do
-
+runUnitTestContract opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do
   -- Print a header
-  liftIO $ putStrLn $ "\nChecking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
+  liftIO $ putStrLn $ "Checking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
 
   -- Look for the wanted contract by name from the Solidity info
   case Map.lookup name contractMap of
@@ -190,9 +192,10 @@ runUnitTestContract
 -- | Define the thread spawner for symbolic tests
 symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m Bool
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
-    liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack testName
-    let cd = symCalldata testName types [] (AbstractBuf "txdata")
-        shouldFail = "proveFail" `isPrefixOf` testName
+    let callSig = testName <> "(" <> (Text.intercalate "," (map abiTypeSolidity types)) <> ")"
+    liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack callSig
+    let cd = symCalldata callSig types [] (AbstractBuf "txdata")
+        shouldFail = "proveFail" `isPrefixOf` callSig
         testContract store = fromMaybe (internalError "test contract not found in state") (Map.lookup vm.state.contract store)
 
     -- define postcondition depending on `shouldFail`
@@ -278,23 +281,14 @@ symFailure UnitTestOptions {..} testName cd types failures' =
         ["Counterexample:"
         ,"  result:   " <> showRes leaf
         ,"  calldata: " <> let ?context = dappContext (traceContext leaf)
-                           in prettyCalldata cex cd testName types
+                            in prettyCalldata cex cd testName types
         ] <> verbText leaf
       verbText leaf = case verbose of
             Just _ -> [Text.unlines [ indentLines 2 (showTraceTree' dapp leaf)]]
             _ -> mempty
       dappContext TraceContext { contracts, labels } =
         DappContext { info = dapp, contracts, labels }
 
-execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper Symbolic RealWorld (Expr End)
-execSymTest UnitTestOptions{ .. } method cd = do
-  -- Set up the call to the test method
-  Stepper.evm $ do
-    makeTxCall testParams cd
-    pushTrace (EntryTrace method)
-  -- Try running the test method
-  runExpr
-
 indentLines :: Int -> Text -> Text
 indentLines n s =
   let p = Text.replicate n " "

test/test.hs

@@ -1581,7 +1581,7 @@ tests = testGroup "hevm"
             }
           |]
         let opts = defaultVeriOpts
-        let sig = Nothing
+        let sig = Just $ Sig "prove_tuple_pass((uint256,uint256))" [AbiTupleType (V.fromList [AbiUIntType 256, AbiUIntType 256])]
         (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] opts
         putStrLnM "Qed, memory tuple is good"
     , test "symbolic-loops-not-reached" $ do