search

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Improve readability our constraint printing #300

Open gltrost opened 3 years ago

gltrost commented 3 years ago

Currently when printing constraints, we print them in a hard to read syntax. For example: 

Internal : (SP in stack range: (and (bvult (bvadd (bvsub #x0000000040000000 #x0000000000800000)
                   #x0000000000000080)
            RSP0)
     (bvule RSP0 #x0000000040000000)): (let ((a!1 (not (and (= ((_ extract 63 30) RSP0)
                        #b0000000000000000000000000000000000)
                     (bvule ((_ extract 29 0) RSP0)
                            #b111111100000000000000010000000)))))
  (and a!1
       (= ((_ extract 63 31) RSP0) #b000000000000000000000000000000000)
       (bvule ((_ extract 30 0) RSP0) #b1000000000000000000000000000000)))|#540| = |init_\|#540\||: (= |#540| |init_\|#540\||)|#510| = |init_\|#510\||: (= |#510| |init_\|#510\||)|#480| = |init_\|#480\||: (= |#480| |init_\|#480\||)mem0 = init_mem0: (= mem0 init_mem0)ZF0 = init_ZF0: (= ZF0 init_ZF0)YMM90 = init_YMM90: (= YMM90 init_YMM90)YMM80 = init_YMM80: (= YMM80 init_YMM80)YMM70 = init_YMM70: (= YMM7

is difficult to understand. Things that should be fixed include

  1. the explicitly long strings of zeros
  2. the \n printings
  3. left-sided binary operations like =
  4. long indentations

If anyone has other requests with respect to printing constraints, please share!

codyroux commented 3 years ago

I was actually hoping that Constraint.to_string could be significantly improved as well, e.g. by printing the constructors in an easy to read format, e.g. ITE (a, b, c) as if a then b else c, Subst(a, b, c) as let b = c in a etc.

codyroux commented 3 years ago

Based on comments from here: https://github.com/draperlaboratory/cbat_tools/pull/244#discussion_r597048015 I'd recommend never having Z3 variables contain #. Sadly BIL "nameless" variables by default are of the form e.g. #123, so probably hooking Expr.mk_const_s, or just Environment.mk_init_var would be a good idea.