microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Running solc on Ubuntu 18.04: Unhandled Exception: System.ComponentModel.Win32Exception: No such file or directory at Interop.Sys.ForkAndExecProcess #256

Closed syscoopco closed 4 years ago

syscoopco commented 4 years ago

Trying to verify a smart contract on Ubuntu 18.04. Everything seems to be installed OK, according to instructions. When running the VeriSol command, the below exception raises. This path format I think is wrong: c:\verisol\sources\VeriSol\VeriSolExecuter.cs (this is a path on Windows machine, not Linux)


Command line args = {/home/work/mis emprendimientos/smart contracts/manicato, ManicatoTokenVeriSol.sol} SpecFilesDir = /home/work/mis emprendimientos/smart contracts ... running Solc on /home/work/mis emprendimientos/smart contracts/manicato

Unhandled Exception: System.ComponentModel.Win32Exception: No such file or directory at Interop.Sys.ForkAndExecProcess(String filename, String[] argv, String[] envp, String cwd, Boolean redirectStdin, Boolean redirectStdout, Boolean redirectStderr, Boolean setUser, UInt32 userId, UInt32 groupId, Int32& lpChildPid, Int32& stdinFd, Int32& stdoutFd, Int32& stderrFd, Boolean shouldThrow) at System.Diagnostics.Process.StartCore(ProcessStartInfo startInfo) at System.Diagnostics.Process.Start() at SolidityAST.SolidityCompiler.RunSolc(String solcPath, String derivedFilePath) in c:\verisol\sources\SolidityAST\SolidityCompiler.cs:line 62 at SolidityAST.SolidityCompiler.Compile(String solcPath, String derivedFilePath) in c:\verisol\sources\SolidityAST\SolidityCompiler.cs:line 24 at VeriSolRunner.VeriSolExecutor.ExecuteSolToBoogie() in c:\verisol\sources\VeriSol\VeriSolExecuter.cs:line 353 at VeriSolRunner.VeriSolExecutor.Execute() in c:\verisol\sources\VeriSol\VeriSolExecuter.cs:line 63 at VeriSolRunner.Program.Main(String[] args) in c:\verisol\sources\VeriSol\Program.cs:line 58 Aborted (core dumped)

shuvendu-lahiri commented 4 years ago

I suspect the space in teh path name (e.g. "smart contracts" and "mis empre") may be causing this issue. Can you remove spaces in path and try again?

syscoopco commented 4 years ago

Hi Shuvendu,

Thank you very much for your fast response. Spaces did matter. Also, I simplified my folders tree (I moved out them from my truffle layout):

Contract under verification: /home/user/work/smart_contracts/manicato/contracts/ManicatoTokenVeriSol.sol

I'm running VeriSol from the source root: /home/user/work/smart_contracts/manicato

OpenZeppelin folder: /home/user/work/smart_contracts/manicato/node_modules/@openzeppelin

A new error raises having to do with parsing the lines importing openzeppelin sol files. Any helps would be appreciated:


~/work/smart_contracts/manicato$ VeriSol contracts/ManicatoTokenVeriSol.sol ManicatoToken Command line args = {contracts/ManicatoTokenVeriSol.sol, ManicatoToken} SpecFilesDir = /home/user/work/smart_contracts/manicato/contracts ... running Solc on /home/user/work/smart_contracts/manicato/contracts/ManicatoTokenVeriSol.sol ManicatoTokenVeriSol.sol:8:1: ParserError: Source "home/user/work/smart_contracts/manicato/node_modules/@openzeppelin/contracts/math/Math.sol" not found: File outside of allowed directories. import "home/user/work/smart_contracts/manicato/node_modules/@openzeppelin/contracts/math/Math.sol"; ^--------------------------------------------------------------------------------------------------^

ManicatoTokenVeriSol.sol:9:1: ParserError: Source "home/user/work/smart_contracts/manicato/node_modules/@openzeppelin/contracts/math/SafeMath.sol" not found: File outside of allowed directories. import "home/user/work/smart_contracts/manicato/node_modules/@openzeppelin/contracts/math/SafeMath.sol"; ^------------------------------------------------------------------------------------------------------^

Unhandled Exception: System.SystemException: Compilation Error at VeriSolRunner.VeriSolExecutor.ExecuteSolToBoogie() in c:\verisol\sources\VeriSol\VeriSolExecuter.cs:line 362 at VeriSolRunner.VeriSolExecutor.Execute() in c:\verisol\sources\VeriSol\VeriSolExecuter.cs:line 63 at VeriSolRunner.Program.Main(String[] args) in c:\verisol\sources\VeriSol\Program.cs:line 58 Aborted (core dumped)

syscoopco commented 4 years ago

"File outside of allowed dir..." exception was solved moving the OpenZeppelin libraries (.sol files) to the same folder as the contract under verification and updating the corresponding import statements.