diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md index e48b78850..702b6e07e 100644 --- a/crucible-llvm-syntax/README.md +++ b/crucible-llvm-syntax/README.md @@ -38,6 +38,7 @@ If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral, The LLVM parser hooks can be further customized by passing yet another `ParserHooks` to them. The `TypeAlias` module implements one such example, for translating -types like `Long` into `(Ptr n)` or `(Bitvector n)` for appropriate `n`. +types like `Long` into `(Bitvector n)` and `Pointer` into `(Ptr n)` for +appropriate `n`. [syn]: ../crucible-syntax diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs index 4b329089f..092d61231 100644 --- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs +++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs @@ -1,3 +1,19 @@ +{- +Module : Lang.Crucible.LLVM.Syntax.TypeAlias +Copyright : (c) Galois, Inc 2023 +Maintainer : Langston Barrett +License : BSD3 + +This module provides facilities for parsing C-like types and translating them +to appropriate Crucible-LLVM types, given a target triple. For example, the +syntax @Long@ is parsed as the Crucible-LLVM 64-bit bitvector type for the +x86_64 Linux target ('x86_64LinuxTypes'), but the 32-bit bitvector type for +32-bit ARM Linux targets ('aarch32LinuxTypes'). This can be useful if you want +to write Crucible CFGs that can be simulated in the context of LLVM modules +for several different architectures, for example if you want to override system +calls. +-} + {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-}