Merge pull request #1017 from GaloisInc/T1007

Fix Haddock parse errors

.github/workflows/crucible-go-build.yml

@@ -99,3 +99,6 @@ jobs:
  - name: Build
  shell: bash
  run: .github/ci.sh build exe:crux-go
+ - name: Haddock
+ shell: bash
+ run: cabal v2-haddock crucible-go

.github/workflows/crucible-jvm-build.yml

@@ -99,3 +99,6 @@ jobs:
  - name: Build
  shell: bash
  run: .github/ci.sh build exe:crucible-jvm
+ - name: Haddock
+ shell: bash
+ run: cabal v2-haddock crucible-jvm

.github/workflows/crucible-wasm-build.yml

@@ -99,3 +99,6 @@ jobs:
  - name: Build
  shell: bash
  run: .github/ci.sh build exe:crucible-wasm
+ - name: Haddock
+ shell: bash
+ run: cabal v2-haddock crucible-wasm

.github/workflows/crux-llvm-build.yml

@@ -131,6 +131,10 @@ jobs:
  .github/ci.sh build exe:crux-llvm-svcomp
  .github/ci.sh build exe:uc-crux-llvm
 
+ - shell: bash
+ name: Haddock
+ run: cabal v2-haddock crucible-symio crucible-llvm crux-llvm uc-crux-llvm
+
  - shell: bash
  name: Test crucible
  run: .github/ci.sh test crucible

.github/workflows/crux-mir-build.yml

@@ -5,18 +5,20 @@ on:
  pull_request:
  workflow_dispatch:
 
-# The CACHE_VERSION can be updated to force the use of a new cache if
-# the current cache contents become corrupted/invalid. This can
-# sometimes happen when (for example) the OS version is changed but
-# older .so files are cached, which can have various effects
-# (e.g. cabal complains it can't find a valid version of the "happy"
-# tool).
-#
-# This also periodically happens on MacOS builds due to a tar bug
-# (symptom: "No suitable image found ... unknown file type, first
-# eight bytes: 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00")
 env:
+ # The CACHE_VERSION can be updated to force the use of a new cache if
+ # the current cache contents become corrupted/invalid. This can
+ # sometimes happen when (for example) the OS version is changed but
+ # older .so files are cached, which can have various effects
+ # (e.g. cabal complains it can't find a valid version of the "happy"
+ # tool).
+ #
+ # This also periodically happens on MacOS builds due to a tar bug
+ # (symptom: "No suitable image found ... unknown file type, first
+ # eight bytes: 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00")
  CACHE_VERSION: 4
+ # Work around https://github.com/rust-lang/cargo/issues/10303
+ CARGO_NET_GIT_FETCH_WITH_CLI: true
 
 jobs:
  outputs:
@@ -123,6 +125,10 @@ jobs:
  - shell: bash
  run: .github/ci.sh build exe:crux-mir
 
+ - shell: bash
+ name: Haddock
+ run: cabal v2-haddock crucible-syntax crucible-concurrency crux-mir
+
  - shell: bash
  run: cd crux-mir && bash ./translate_libs.sh
 

crucible-go/src/Lang/Crucible/Go/Builtin.hs

@@ -49,7 +49,7 @@ translateBuiltin _qual ident@(Ident _k name) args = do
  return $ mkTranslatedExpr retRepr $ do
  case name of
 
- -- | Compute the length of a value of appropriate type. The
+ -- Compute the length of a value of appropriate type. The
  -- length of a nil pointer to an array or a nil slice is zero.
  "len" -> do
  args' <- forM translated_args $ runTranslatedExpr retRepr
@@ -94,7 +94,7 @@ translateBuiltin _qual ident@(Ident _k name) args = do
  fail $ "translateBuiltin: expected exactly one argument to\
  \ 'len', got " ++ show args'
 
- -- | Create a new slice or map value.
+ -- Create a new slice or map value.
  "make" -> case zip args translated_args of
  (Pair arg_node _argM, TranslatedType (Some repr)) : t_args' ->
  tryAsSliceRepr repr
@@ -127,7 +127,7 @@ translateBuiltin _qual ident@(Ident _k name) args = do
  fail $ "translateBuiltin: expected type argument to 'make', got "
  ++ show (proj1 <$> args)
 
- -- | Allocate a new value and return a pointer to it.
+ -- Allocate a new value and return a pointer to it.
  "new" -> case zip args translated_args of
  [(Pair arg_node _argM, TranslatedType (Some repr))] -> do
  zero <- zeroValue' (typeOf' arg_node) repr
@@ -137,15 +137,15 @@ translateBuiltin _qual ident@(Ident _k name) args = do
  fail $ "translateBuiltin: expected exactly one type argument to\
  \ 'new', got " ++ show (proj1 <$> args)
 
- -- | Exit the program with an error message. Panics can actually
+ -- Exit the program with an error message. Panics can actually
  -- be recovered from in Go, sort of like exceptions, but we
  -- don't support such control flow for now.
  "panic" -> do
  args' <- forM translated_args $ runTranslatedExpr retRepr
  Gen.reportError $ Gen.App $ C.StringLit $
  UnicodeLiteral $ T.pack $ "panic: " ++ show args'
 
- -- | Print the arguments.
+ -- Print the arguments.
  "print" -> do
  args' <- forM translated_args $ runTranslatedExpr retRepr
  forM_ args' $ \(Some (GoExpr _loc arg')) ->

crucible-go/src/Lang/Crucible/Go/Translation.hs

@@ -515,7 +515,7 @@ translate_alg (IdentExpr _ tp qual ident@(Ident _kind name)) = TranslateM $ do
  e <- Gen.readRef ref
  return $ Some $ GoExpr (Just $ GoLocRef ref) e
  Nothing ->
- -- | Local lookup failure.
+ -- Local lookup failure.
  -- return $ mkSomeGoExpr' C.EmptyApp
  fail $ "translate_alg IdentExpr: unbound local " ++ show name
  Just q -> lookupGlobal q ident
@@ -826,7 +826,7 @@ translateHomoBinop :: Type -> BinaryOp -> Gen.Expr Go s a -> Gen.Expr Go s a
 translateHomoBinop tp op left right = case op of
  BPlus -> case exprType left of
  BVRepr w -> return $ Gen.App $ C.BVAdd w left right
- -- | Rounding uses IEEE 754 round-to-even rules but with an IEEE
+ -- Rounding uses IEEE 754 round-to-even rules but with an IEEE
  -- negative zero further simplified to an unsigned zero. -- SPEC
  FloatRepr fi -> return $ Gen.App $ C.FloatAdd fi C.RNE left right
  StringRepr si -> return $ Gen.App $ C.StringConcat si left right

crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs

@@ -175,7 +175,7 @@ data ParserHooks ext = ParserHooks {
  , MonadIO m
  , IsSyntaxExtension ext
  , ?parserHooks :: ParserHooks ext
- -- ^ ParserHooks instance to use recursively when parsing.
+ -- ParserHooks instance to use recursively when parsing.
  )
  => m (Pair TypeRepr (Atom s))
  -- ^ A pair containing a type and an atom of that type from evaluation of
@@ -1581,7 +1581,7 @@ operands :: forall s ext m tps
  , MonadSyntax Atomic m
  , IsSyntaxExtension ext
  , ?parserHooks :: ParserHooks ext )
- -- ^ ParserHooks to use for syntax extensions
+ -- ParserHooks to use for syntax extensions
  => Ctx.Assignment TypeRepr tps
  -- ^ Types of the operands
  -> m (Ctx.Assignment (Atom s) tps)