The Printable.S signature has some functions whose necessity isn't clear to me. I want to know which of these do we really need and which we could get rid of. The signature is massive and thus super annoying to implement. So the fewer functions it contains, the better.

isSimple

There are only two actual (non-delegating) calls of this function and both just use it to determine whether to avoid printing an extra \n:

pretty_f

This seems to be only used for defining pretty. Might as well define pretty directly.

short

This seems to just be used for debug printing and warning without Pretty. The massive downside of this function is its "width" argument:

• Many definitions outright ignore it and can produce longer string.
• Every call of short passes some completely random and different number as width, making the code full of weird magic constants.
• Often you find ridiculously high constants like 800 because there's actually no need to trim the large textual representation but instead we care about some information it may contain. It'd argue it's even harmful for debugging to see truncated strings because you can't tell if <foo, ...> and <foo, ...> are the same thing or not.
• Some calls even use width 0, which total nonsense and a sign that the width is meaningless.
• Many of these calls are also in commented out debugging code that tries to use Printf not Pretty or tracing.
• Mutex, symbolic locks and thread ID analyses use short to construct our fabulous string-based access partitions and lock sets, which are used to determine races:

  analyzer/src/analyses/mutexAnalysis.ml

  Lines 92 to 93 in 08b4336

  	let ls = Lockset.Lock.short 80 l in
  	LSSet.add ("lock",ls)

  analyzer/src/analyses/symbLocks.ml

  Line 178 in 08b4336

  LSSet.add ("i-lock",ValueDomain.Addr.short 80 lock) xs

  analyzer/src/analyses/threadId.ml

  Lines 76 to 77 in 08b4336

  	let tid = ThreadLifted.short 20 tid in
  	(Access.LSSSet.singleton es, Access.LSSet.add ("thread",tid) es)

  
  What if two different locks have insanely long names but share the 80-character prefix?

to_yojson

This is just needed for "json" value for "result". What actually consumes these JSON results? If I understand correctly from git history, this was added to save results into MongoDB: 8a4c722. The MongoDB related code now is just around commented out.

Not that this is completely separate from our JSON configuration, which we have our own from-scratch JSON implementation for anyway.