A Solidity parser in OCaml with Menhir

Authors: David Declerck
Date: 2020-05-19
Category: Blockchains



Solidity Logo


This article is cross-posted on Origin Labs’ Dune Network blog

We are happy to announce the first release of our Solidity parser, written in OCaml using Menhir. This is a joint effort with Origin Labs, the company dedicated to blockchain challenges, to implement a full interpreter for the Solidity language directly in a blockchain.

Solidity Logo

Solidity is probably the most popular language for smart-contracts, small pieces of code triggered when accounts receive transactions on a blockchain.Solidity is an object-oriented strongly-typed language with a Javascript-like syntax.

Ethereum Logo

Solidity was first implemented for the Ethereum blockchain, with a compiler to the EVM, the Ethereum Virtual Machine.

Dune Network Logo

Dune Network takes a different approach, as Solidity smart-contracts will be executed natively, after type-checking. Solidity will be the third native language on Dune Network, with Michelson, a low-level strongly-typed language inherited from Tezos, and Love, an higher-level strongly-typed language, also implemented jointly by OCamlPro and Origin Labs.

A first step has been accomplished, with the completion of the Solidity parser and printer, written in OCaml with Menhir.

This parser (and its printer companion) is now available as a standalone library under the LGPLv3 license with Linking Exception, allowing its integration in all projects. The source code is available at https://gitlab.com/o-labs/solidity-parser-ocaml.

Our parser should support all of Solidity 0.6, with the notable exception of inline assembly (may be added in a future release).

Example contract

Here is an example of a very simple contract that stores an integer value and allows the contract’s owner to add an arbitrary value to this value, and any other contract to read this value:

pragma solidity >=0.6.0 <0.7.0;

contract C {
    address owner;
    int x;

    constructor() public {
        owner = msg.sender;
        x = 0;
    }

    function add(int d) public {
        require(msg.sender == owner);
        x += d;
    }

    function read_x() public view returns(int) {
        return x;
    }
}

Parser Usage

Executable

Our parser comes with a small executable that demonstrates the library usage. Simply run:

./solp contract.sol

This will parse the file contract.sol and reprint it on the terminal.

Library

To use our parser as a library, add it to your program’s dependencies and use the following function:

Solidity_parser.parse_contract_file : string -> Solidity_parser.Solidity_types.module_

It takes a filename and returns a Solidity AST.

If you wish to print this AST, you may turn it into its string representation by sending it to the following function:

Solidity_parser.Printer.string_of_code : Solidity_parser.Solidity_types.module_ -> string

Conclusion

Of course, all of this is Work In Progress, but we are quite happy to share it with the OCaml community. We think there is a tremendous work to be done around blockchains for experts in formal methods. Do not hesitate to contact us if you want to use this library!

About Origin Labs

Origin Labs is a company founded in 2019 by the former blockchain team at OCamlPro. At Origin Labs, they have been developing Dune Network, a fork of the Tezos blockchain, its ecosystem, and applications over the Dune Network platform. At OCamlPro, they developed TzScan, the most popular block explorer at the time, Liquidity, a smart contract language, and were involved in the development of the core protocol and node.Do not hesitate to reach out by email: contact@origin-labs.com.



About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

  • We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, Wasm and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
  • We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we developed the prototype of the Tezos proof-of-stake blockchain.
  • We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
  • We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.