No Description

Pat Hickey 9b3664eec2 example idl: make sure we have a bool_t for test coverage 9 years ago
executables 30e1edc4d6 gidl: command line frontend ftw 9 years ago
src dfd75dc394 ivory backend: some fixes for compiling bool_t to IBool 9 years ago
support d283c0676e haskell-rpc: fix snap server to serve both rpc and directory using alternative 9 years ago
tests 9b3664eec2 example idl: make sure we have a bool_t for test coverage 9 years ago
.gitignore 2e22972f0a Ignore cabal sandboxes. 9 years ago
.travis.yml 34f93635a0 Travis-CI: IVORY_REPO/etc. are already in the environment. 9 years ago
LICENSE d456b97842 gidl: oops, wrong license, its bsd3 now 9 years ago
Makefile 59b930ba21 Use my new cabal dependency snippets. 9 years ago
Makefile.deps 59b930ba21 Use my new cabal dependency snippets. 9 years ago
Makefile.sandbox 59b930ba21 Use my new cabal dependency snippets. 9 years ago
README.md 44da197efd bump readme 9 years ago
Setup.hs 89d04f0623 gidl: initial commit 9 years ago
gidl.cabal 732d51aa72 Install Makefile.sandbox for use in ivory and tower backends. 9 years ago

README.md

Gidl

TravisCI

Gidl (for Galois Interface Description Language) is a simple IDL for describing structured types and RPC-style interfaces.

Overview

Jump right to an example of gidl.

Types

Gidl has a type language which permits the user to define types using the following primitives:

  • Atomic types:
    • Signed integers of 8, 16, 32, 64 bit width
    • Unsigned integers of 8, 16, 32, 64 bit width
    • IEEE 754 single and double precision floating point numbers
    • Boolean values
  • User-defined Enum types:
    • Pairs of names and values, where names and values must have a one-to-one correspondence
    • User specified representation width (8, 16, 32, or 64 bits)
  • User-defined Newtypes:
    • Wraps an existing atomic or enum type with a new type
  • User-defined Structures:
    • Set of named fields. Corresponds to a record or a C struct.
    • Fields may be of any other user-defined type

Interfaces

Gidl interfaces are composed of the following primitives:

  • Streams, which are sent from server to client whenever the server wants. (We expect to refine this and allow clients to control stream rate.)
  • Attributes, which are read and written according to requests by the client. Attributes have a user defined read/writable permissions.

Interfaces can be composed by subtyping. (We expect interface composition may change in the future.)

Protocol drift is detected by identifying each stream and attribute message on the wire by a hash of its name, its type, and all child types. Therefore

IDL format

The gidl IDL uses a s-expression based format. The IDL format currently is documented in tests/example.idl

Backends

Gidl currently has backends for:

  • Haskell backend: translates types to algebraic datatypes, creates cereal instances for serialization.
  • Haskell-RPC backend: all of the features of the Haskell backend, and also creates an HTTP server that exposes a JSON RPC-style interface for gidl interfaces.
  • Ivory backend: translates types to Ivory types, creates ivory-serialize instances for serialization.
  • Tower backend: all of the features of the Ivory backend, and also creates datatypes of tower channels for interface streams and attributes, and a tower monitor which implements a server for a given interface.

Prerequisites

Gidl requires the GHC 7.8 haskell compiler, and a modern Cabal (>= 1.18).

It also requires the s-cargot package, which is not yet available through hackage. In the parent directory, run

git clone https://github.com/aisamanra/s-cargot

In order to build the code generated by the the Ivory and Tower backends, we require the Ivory, Tower, and ivory-tower-stm32 repositories. These should also be found, by default, in the parent directory.

git clone https://github.com/galoisinc/ivory
git clone https://github.com/galoisinc/tower
git clone https://github.com/galoisinc/ivory-tower-stm32

Build and Test

Use the create-sandbox target in the Makefile to create a local cabal sandbox and install all dependencies.

The default target builds the gidl library. You can then use cabal run gidl -- <OPTIONS> to run the code generator. Use the --help option to get usage information.

Use the test target in the Makefile to generate and test each backend implementation. The tests/example.idl file is used as the input language. You may then browse generated code for each implementation, which is generated and built in subdirectories of the tests directory.

About

Gidl was created at Galois by Pat Hickey, with help from Getty Ritter and Trevor Elliott, as part of the SMACCMPilot project.

Gidl was inspired in part by John Van Enk's excellent Cauterize tools. Look for gidl to switch to using cauterize as the type language in the future!

Gidl is still experimental - anything may change at any time. Please get in touch if you're interested in using or working on gidl.