search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
640 stars 74 forks source link

Pretty printing `ite` expressions #203

Closed rachitnigam closed 3 years ago

rachitnigam commented 3 years ago

Is there a library function to pretty print ite expressions generated from symbolic execution? I want to store the results of symbolically evaluating program as golden outputs in my repository so that future changes to the internals of my system don't affect the generated representation.

I have something like:

(ite (bvult (bvadd (bv #x1 4) r0) (bv #xa 4)) (ite (bvult (bvadd (bv #x2 4) r0) (bv #xa 4)) (ite (bvult (bvadd (bv #x3 4) r0) (bv #xa 4)) (ite (bvult (bvadd (bv #x4 4) r0) (bv #xa 4)) (ite (bvult (bvadd (bv #x5 4) r0) (bv #xa 4)) (ite (bvult (bvadd (bv #x6 4) r0) ...) ...) ...) ...) ...) ...) ...)

I would like to print it in human readable form, ideally similar to Racket's cond form:

(cond 
  [(<= (+ r0 1)) ...]
  ...)
sorawee commented 3 years ago

If I understand what you want to do correctly, one easy hack is to write it as a string, read it back as an S-exp, and then use racket/pretty to format it.

(define (convert obj)
  (pretty-format (read (open-input-string (~a result)))))
rachitnigam commented 3 years ago

Okay, that's helpful. Is there no standard way to convert an ite into a cond or something? I can implement something that does it but it'll be some work.

sorawee commented 3 years ago

I don't think we have anything like that.

But also note that ite is already a callable function if you are willing to (require rosette/base/core/polymorphic) (which is Rosette internals, so you might or might not want to use it, depending on your use case)