Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

uc-crux-llvm: Serialization of data structures #994

Merged
merged 26 commits into from
Jun 3, 2022
Merged

Conversation

langston-barrett
Copy link
Contributor

@langston-barrett langston-barrett commented May 20, 2022

Introduce functions for (de)serializing the many type-indexed GADTs in UC-Crux. The reasoning behind the overall shape of the implementation is recorded in the module comment on UCCrux.LLVM.View. This will enable features like #982.

This is still a draft because error handling would need to be improved, many of the errors lack sufficient context to really make it easy to see what went wrong during deserialization. However, since this is already fairly large, I wanted to get some initial feedback on the direction before polishing it off.

uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs Outdated Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/View/Cursor.hs Outdated Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs Outdated Show resolved Hide resolved
@langston-barrett
Copy link
Contributor Author

I'm having trouble reproducing the CI failures. Here's what they look like:

    view-shape:                                                           FAIL
      *** Failed! (after 1 test):
      Exception while generating shrink-list:
        Test.QuickCheck.resize: negative size
        CallStack (from HasCallStack):
          error, called at src/Test/QuickCheck/Gen.hs:135:22 in QuickCheck-2.14.2-0c7f5115b9190e0c296f816bfcd00c19cd356a8b5211cf667467a3d51faa6351:Test.QuickCheck.Gen
      Exception thrown while showing test case:
        Test.QuickCheck.resize: negative size
        CallStack (from HasCallStack):
          error, called at src/Test/QuickCheck/Gen.hs:135:22 in QuickCheck-2.14.2-0c7f5115b9190e0c296f816bfcd00c19cd356a8b5211cf667467a3d51faa6351:Test.QuickCheck.Gen

I can't reproduce this with --quickcheck-replay with GHC 9.0 nor 8.10, though both of these are failing in CI on Ubuntu 20.04 (but not 18.04 nor Windows nor OSX). I also tried cabal update to no avail. The build configuration also looks similar, both CI and I are compiling with -O1. I suppose I'll try writing a Dockerfile for testing this on Ubuntu 20.04.

@langston-barrett
Copy link
Contributor Author

I was also unable to reproduce the failure using an Ubuntu 20.04 Dockerfile.

Dockerfile
FROM ubuntu:20.04
ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update -qq && apt-get install -y -qq build-essential curl libffi-dev libffi7 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libz-dev
RUN curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh
ENV PATH=$PATH:/root/.ghcup/bin:/root/.cabal/bin
RUN ghcup install ghc 9.2.1 && \
    ghcup install cabal 3.6.2
CMD bash
docker build -t ubuntu . && docker run --mount src=/tmp/cabal,target=/root/.cabal,type=bind --mount src=$PWD,target=/w,type=bind -w /w --rm -it ubuntu bash -c "cd uc-crux-llvm && cabal update && cabal --builddir=build-ubuntu-20.04 run test:uc-crux-llvm-test -- -p /view/"

Encountered weird errors in CI with QuickCheck:

    view-shape:
      *** Failed! (after 1 test):
      Exception while generating shrink-list:
        Test.QuickCheck.resize: negative size
        CallStack (from HasCallStack):
          error, called at src/Test/QuickCheck/Gen.hs:135:22 in QuickCheck-2.14.2-0c
      Exception thrown while showing test case:
        Test.QuickCheck.resize: negative size
        CallStack (from HasCallStack):
          error, called at src/Test/QuickCheck/Gen.hs:135:22 in QuickCheck-2.14.2-0c

Later commits will port the remainder of the view tests; this commit is a
minimal switch which compiles, passes tests, and shows the feasibility of using
Hedgehog.

Unfortunately, both libraries for creating Hedgehog generators from Generic
instances turned out to be unsuitable.

- hedgehog-generic didn't work for modern GHC
- hedgehog-gen needed *all* the datatypes involved to be Generic, which e.g.,
  Alignment is not.
@langston-barrett langston-barrett marked this pull request as ready for review June 3, 2022 13:24
@langston-barrett langston-barrett merged commit 4158b6f into master Jun 3, 2022
@langston-barrett langston-barrett deleted the lb/views branch June 3, 2022 21:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants