qsym

  1use qbe_reader::types::*;
  2use z3::{ast::BV, Context};
  3
  4// TODO: Would be cool if we could enforce some additional type
  5// safety via this abstraction. For example, avoiding that BVs
  6// of different sizes are added, multiplied, et cetera.
  7
  8pub const BYTE_SIZE: u32 = 8;
  9pub const HALF_SIZE: u32 = 16;
 10pub const WORD_SIZE: u32 = 32;
 11pub const LONG_SIZE: u32 = 64;
 12
 13pub struct ValueFactory<'ctx> {
 14    ctx: &'ctx Context,
 15}
 16
 17impl<'ctx> ValueFactory<'ctx> {
 18    pub fn new(ctx: &'ctx Context) -> ValueFactory<'ctx> {
 19        return ValueFactory { ctx };
 20    }
 21
 22    ////
 23    // Associated Methods
 24    ////
 25
 26    fn basety_to_size(ty: BaseType) -> u32 {
 27        match ty {
 28            BaseType::Word => WORD_SIZE,
 29            BaseType::Long => LONG_SIZE,
 30            BaseType::Single => panic!("floating points not supported"),
 31            BaseType::Double => panic!("floating points not supported"),
 32        }
 33    }
 34
 35    fn extty_to_size(ty: ExtType) -> u32 {
 36        match ty {
 37            ExtType::Base(b) => Self::basety_to_size(b),
 38            ExtType::Byte => BYTE_SIZE,
 39            ExtType::Halfword => HALF_SIZE,
 40        }
 41    }
 42
 43    fn subwty_to_size(ty: SubWordType) -> u32 {
 44        match ty {
 45            SubWordType::SignedByte => BYTE_SIZE,
 46            SubWordType::UnsignedByte => BYTE_SIZE,
 47            SubWordType::SignedHalf => HALF_SIZE,
 48            SubWordType::UnsignedHalf => HALF_SIZE,
 49        }
 50    }
 51
 52    fn sublty_to_size(ty: SubLongType) -> u32 {
 53        match ty {
 54            SubLongType::SubWord(x) => Self::subwty_to_size(x),
 55            SubLongType::UnsignedWord => 32,
 56            SubLongType::SignedWord => 32,
 57        }
 58    }
 59
 60    pub fn loadty_to_size(ty: LoadType) -> u32 {
 61        match ty {
 62            LoadType::Base(x) => Self::basety_to_size(x),
 63            LoadType::SubLong(x) => Self::sublty_to_size(x),
 64        }
 65    }
 66
 67    ////
 68    // Bitvector Factory Functions
 69    ////
 70
 71    pub fn from_ext(&self, ty: ExtType, name: String) -> BV<'ctx> {
 72        let size = Self::extty_to_size(ty);
 73        BV::new_const(self.ctx, name, size)
 74    }
 75
 76    pub fn from_ext_i64(&self, ty: ExtType, v: i64) -> BV<'ctx> {
 77        let size = Self::extty_to_size(ty);
 78        BV::from_i64(self.ctx, v, size)
 79    }
 80
 81    pub fn from_subw(&self, ty: SubWordType, name: String) -> BV<'ctx> {
 82        let size = Self::subwty_to_size(ty);
 83        BV::new_const(self.ctx, name, size)
 84    }
 85
 86    pub fn from_base(&self, ty: BaseType, name: String) -> BV<'ctx> {
 87        let size = Self::basety_to_size(ty);
 88        BV::new_const(self.ctx, name, size)
 89    }
 90
 91    pub fn from_base_u64(&self, ty: BaseType, v: u64) -> BV<'ctx> {
 92        let size = Self::basety_to_size(ty);
 93        BV::from_u64(self.ctx, v, size)
 94    }
 95
 96    pub fn from_base_i64(&self, ty: BaseType, v: i64) -> BV<'ctx> {
 97        let size = Self::basety_to_size(ty);
 98        BV::from_i64(self.ctx, v, size)
 99    }
100
101    ////
102    // Operations on created Bitvectors
103    ////
104
105    // Extend a bitvector of a SubWordType to a word, i.e. 32-bit.
106    // The extended bits are treated as unconstrained symbolic this
107    // is the case because QBE mandates that the most significant
108    // bits of an extended subword are unspecified/undefined.
109    pub fn extend_subword(&self, ty: SubWordType, val: BV<'ctx>) -> BV<'ctx> {
110        let size = Self::subwty_to_size(ty);
111        assert!(val.get_size() == size);
112
113        assert!(val.get_size() < 32);
114        let rem = WORD_SIZE - size;
115
116        let uncons = BV::fresh_const(self.ctx, "undef-msbsw", rem);
117        val.concat(&uncons) // TODO: Does this set the MSB?
118    }
119
120    pub fn cast_to(&self, ty: ExtType, val: BV<'ctx>) -> BV<'ctx> {
121        let cur_size = val.get_size();
122        let tgt_size = Self::extty_to_size(ty);
123
124        if tgt_size == cur_size {
125            val
126        } else if tgt_size > cur_size {
127            val.zero_ext(tgt_size - cur_size)
128        } else {
129            val.extract(tgt_size - 1, 0)
130        }
131    }
132
133    pub fn trunc_to(&self, ty: SubLongType, val: BV<'ctx>) -> BV<'ctx> {
134        let tgt_size = Self::sublty_to_size(ty);
135        let r = val.extract(tgt_size - 1, 0);
136        assert!(r.get_size() == tgt_size);
137        r
138    }
139
140    pub fn sign_ext_to(&self, ty: BaseType, val: BV<'ctx>) -> BV<'ctx> {
141        let cur_size = val.get_size();
142        let tgt_size = Self::basety_to_size(ty);
143        if cur_size == tgt_size {
144            return val;
145        }
146
147        assert!(tgt_size > cur_size);
148        val.sign_ext(tgt_size - cur_size)
149    }
150
151    pub fn zero_ext_to(&self, ty: BaseType, val: BV<'ctx>) -> BV<'ctx> {
152        let cur_size = val.get_size();
153        let tgt_size = Self::basety_to_size(ty);
154        if cur_size == tgt_size {
155            return val;
156        }
157
158        assert!(tgt_size > cur_size);
159        val.zero_ext(tgt_size - cur_size)
160    }
161
162    ////
163    // Syntatic Sugar
164    ////
165
166    pub fn make_byte(&self, v: u8) -> BV<'ctx> {
167        BV::from_u64(self.ctx, v.into(), BYTE_SIZE)
168    }
169    pub fn make_half(&self, v: u16) -> BV<'ctx> {
170        BV::from_u64(self.ctx, v.into(), HALF_SIZE)
171    }
172    pub fn make_word(&self, v: u32) -> BV<'ctx> {
173        BV::from_u64(self.ctx, v.into(), WORD_SIZE)
174    }
175    pub fn make_long(&self, v: u64) -> BV<'ctx> {
176        BV::from_u64(self.ctx, v, LONG_SIZE)
177    }
178}