elliottt / easy-smt

Easy SMT solver interaction
Apache License 2.0
24 stars 4 forks source link

Helper method to turn an s-expr atom that is a bitvector into a rust number #5

Closed fitzgen closed 1 year ago

fitzgen commented 1 year ago

Reading bitvector results (and ints for that matter) from solver model results is kind of annoying. We should add helpers for extracting the value as a i32/usize/etc so it is easy to work with in rust.

Something like

impl SExprData {
    pub fn as_i32(&self) -> Option<i32> { ... }
}

Maybe generic so we wouldn't need multiple methods for i8, i16, i32, etc...?

Or maybe these should be

impl TryFrom<SExprData> for i8 { ... }
impl TryFrom<SExprData> for i16 { ... }
impl TryFrom<SExprData> for i32 { ... }
// etc...

cc @avanhatt

avanhatt commented 1 year ago

Another use case that may-or-may-not make sense as part of this issue (or part of the library)

It can be nice to print bitvector results as their full width, in both/either hex or binary. Right now we have a little glue code post-library to format hex values as binary as well, but this loses the width component (SMTLib always puts leadings zeros in hex and binary, to my knowledge):

    let sexpr_hex_prefix = "#x";
    let val_str = self.smt.display(value).to_string();
    if val_str.starts_with(sexpr_hex_prefix) {
        let without_prefix = val_str.trim_start_matches("#x");
        let as_unsigned = u64::from_str_radix(without_prefix, 16).unwrap();
        format!("{}\n{:#b}", self.smt.display(value), as_unsigned)
    } //...

It would be nice to be able to format an SExpr as SMTLIB-like strings, for example:

#x3 
#b0011

From something like:

impl SExprData {
    pub fn as_hex_string(&self) -> Option<String> { ... }
    pub fn as_bin_string(&self) -> Option<String> { ... }
}
fitzgen commented 1 year ago

Should be simple to do with the regular format!("{:b}", val) etc machinery once we can extract the value as an actual rust integer type. No reason not to have convenience helpers for it as well though.