output-repair tool to fix truncated XML and JSON log files

[peterschrammel]

The XML version of that has been used by BTC for a couple of years now...

[tautschnig]

May I ask why this is even necessary? That is, why does a truncated file come into existence? Is it that we'd just need a proper signal handler?

[peterschrammel]

The main reason was that there is nothing equivalent to signals if cbmc is started through CreateProcess in Windows.

There are a couple of patches that do it with signals around bab8853 but we discarded them.

[tautschnig]

I am wondering whether we should accept to just have an increasing number of directories with smaller tools (the code-warrior transformation tool comes to my mind), or create a separate repository, or some sub directory hosting those tools. Otherwise this all looks good.

[peterschrammel]

Yes, I had similar discussions with Daniel. We should probably move musketeer, the symex tools, etc into a separate repo in order to reduce the number of folders in src/.

[tautschnig]

The problem of moving into a separate repository is that these effectively die a silent death, because APIs keep changing. It would seem more honest to just delete the directory.

[peterschrammel]

Of course, there must also be CI for these repos to prevent this from happening.

[tautschnig]

The problem is ownership: person A commits changes to cbmc that break the-other-repo. Who is going to notice this? (the-other-repo hasn't had a commit, hence travis wouldn't kick in.) Even if noticed, is person A going to fix the-other-repo?

One approach that could make all of this work is for cbmc to include a script that

1. fetches all dependent repositories
2. tries to build all of them
3. is triggered from the cbmc .travis.yml script
4. is updated whenever a tool is moved (or newly created) in a fresh repository.
   At the moment, this would be

#!/bin/bash
set -e
for r in 2ls ; do
  git clone https://github.com/diffblue/$r
  cd $r/src
  echo "CBMC = ../.." > config.inc
  make
  cd ../regression
  make test
done

[peterschrammel]

There are solutions for that, e.g. https://github.com/mernst/plume-lib/blob/master/bin/trigger-travis.sh, http://eng.rightscale.com/2015/04/27/dependent-builds-in-travis.html

[tautschnig]

Thanks, that's nice, but I'm not sure it would solve the ownership problem? It would certainly work for 2ls as @peterschrammel would care, but for those directories named above I'd doubt anyone would step up to fix them. Making the cbmc Travis job fail forces people to care.

[rjmunro]

Is this a generic utility to close open tags in truncated XML / JSON files, or something more specific to CBMC? If the former, it seems sensible to move it to it's own project. It may be useful to people doing completely unrelated things.

[peterschrammel]

Yes, @rjmunro, there is nothing CBMC-specific. I can move it into a separate repo.

[rjmunro]

I think that @tautschnig's comment about "dying a silent death, because APIs keep changing" isn't relevant if this is a generic tool. The JSON and XML specifications are not changing any time soon. :-)

[peterschrammel]

This is now available here: https://github.com/diffblue/output-repair