isla_lib/
simplify.rs

1// BSD 2-Clause License
2//
3// Copyright (c) 2019, 2020 Alasdair Armstrong
4// Copyright (c) 2020 Brian Campbell
5//
6// All rights reserved.
7//
8// Redistribution and use in source and binary forms, with or without
9// modification, are permitted provided that the following conditions are
10// met:
11//
12// 1. Redistributions of source code must retain the above copyright
13// notice, this list of conditions and the following disclaimer.
14//
15// 2. Redistributions in binary form must reproduce the above copyright
16// notice, this list of conditions and the following disclaimer in the
17// documentation and/or other materials provided with the distribution.
18//
19// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
20// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
21// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
22// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
23// HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
24// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
25// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
26// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
27// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
28// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
29// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30
31//! This module implements various routines for simplifying event
32//! traces, as well as printing the generated traces.
33
34use std::borrow::{Borrow, BorrowMut};
35use std::collections::{HashMap, HashSet};
36use std::io::Write;
37
38use crate::bitvector::{write_bits64, BV};
39use crate::ir::{Name, Symtab, Val, HAVE_EXCEPTION};
40use crate::smt::smtlib::*;
41use crate::smt::Event::*;
42use crate::smt::{Accessor, Event, Sym};
43use crate::zencode;
44
45/// `renumber_event` Renumbers all the symbolic variables in an event such that multiple event
46/// sequences can have disjoint variable identifiers. It takes two `u32` arguments `i` and `total`,
47/// such that `i` is the index of our event sequence in the range `0..(total - 1)` inclusive where
48/// `total` is the number of event sequences we want to make disjoint.
49#[allow(clippy::unneeded_field_pattern)]
50pub fn renumber_event<B>(event: &mut Event<B>, i: u32, total: u32) {
51    assert!(i < total);
52    use Event::*;
53    match event {
54        Smt(def) => renumber_def(def, i, total),
55        Fork(_, v, _) | Sleeping(v) => *v = Sym { id: (v.id * total) + i },
56        ReadReg(_, _, value) | WriteReg(_, _, value) | Instr(value) => renumber_val(value, i, total),
57        Branch { address } => renumber_val(address, i, total),
58        Barrier { barrier_kind } => renumber_val(barrier_kind, i, total),
59        ReadMem { value, read_kind, address, bytes: _, tag_value, kind: _ } => {
60            renumber_val(value, i, total);
61            renumber_val(read_kind, i, total);
62            renumber_val(address, i, total);
63            if let Some(v) = tag_value {
64                renumber_val(v, i, total);
65            }
66        }
67        WriteMem { value: v, write_kind, address, data, bytes: _, tag_value, kind: _ } => {
68            *v = Sym { id: (v.id * total) + i };
69            renumber_val(write_kind, i, total);
70            renumber_val(address, i, total);
71            renumber_val(data, i, total);
72            if let Some(v) = tag_value {
73                renumber_val(v, i, total);
74            }
75        }
76        CacheOp { cache_op_kind, address } => {
77            renumber_val(cache_op_kind, i, total);
78            renumber_val(address, i, total);
79        }
80        Cycle | SleepRequest | WakeupRequest | MarkReg { .. } => (),
81    }
82}
83
84fn renumber_exp(exp: &mut Exp, i: u32, total: u32) {
85    exp.modify(
86        &(|exp| {
87            if let Exp::Var(v) = exp {
88                *v = Sym { id: (v.id * total) + i }
89            }
90        }),
91    )
92}
93
94fn renumber_val<B>(val: &mut Val<B>, i: u32, total: u32) {
95    use Val::*;
96    match val {
97        Symbolic(v) => *v = Sym { id: (v.id * total) + i },
98        I64(_) | I128(_) | Bool(_) | Bits(_) | Enum(_) | String(_) | Unit | Ref(_) | Poison => (),
99        List(vals) | Vector(vals) => vals.iter_mut().for_each(|val| renumber_val(val, i, total)),
100        Struct(fields) => fields.iter_mut().for_each(|(_, val)| renumber_val(val, i, total)),
101        Ctor(_, val) => renumber_val(val, i, total),
102    }
103}
104
105fn renumber_def(def: &mut Def, i: u32, total: u32) {
106    use Def::*;
107    match def {
108        DeclareConst(v, _) | DeclareFun(v, _, _) | DefineEnum(v, _) => *v = Sym { id: (v.id * total) + i },
109        DefineConst(v, exp) => {
110            *v = Sym { id: (v.id * total) + i };
111            renumber_exp(exp, i, total)
112        }
113        Assert(exp) => renumber_exp(exp, i, total),
114    }
115}
116
117/// `uses_in_exp` counts the number of occurences of each variable in an SMTLIB expression.
118fn uses_in_exp(uses: &mut HashMap<Sym, u32>, exp: &Exp) {
119    use Exp::*;
120    match exp {
121        Var(v) => {
122            uses.insert(*v, uses.get(&v).unwrap_or(&0) + 1);
123        }
124        Bits(_) | Bits64(_) | Enum(_) | Bool(_) => (),
125        Not(exp) | Bvnot(exp) | Bvneg(exp) | Extract(_, _, exp) | ZeroExtend(_, exp) | SignExtend(_, exp) => {
126            uses_in_exp(uses, exp)
127        }
128        Eq(lhs, rhs)
129        | Neq(lhs, rhs)
130        | And(lhs, rhs)
131        | Or(lhs, rhs)
132        | Bvand(lhs, rhs)
133        | Bvor(lhs, rhs)
134        | Bvxor(lhs, rhs)
135        | Bvnand(lhs, rhs)
136        | Bvnor(lhs, rhs)
137        | Bvxnor(lhs, rhs)
138        | Bvadd(lhs, rhs)
139        | Bvsub(lhs, rhs)
140        | Bvmul(lhs, rhs)
141        | Bvudiv(lhs, rhs)
142        | Bvsdiv(lhs, rhs)
143        | Bvurem(lhs, rhs)
144        | Bvsrem(lhs, rhs)
145        | Bvsmod(lhs, rhs)
146        | Bvult(lhs, rhs)
147        | Bvslt(lhs, rhs)
148        | Bvule(lhs, rhs)
149        | Bvsle(lhs, rhs)
150        | Bvuge(lhs, rhs)
151        | Bvsge(lhs, rhs)
152        | Bvugt(lhs, rhs)
153        | Bvsgt(lhs, rhs)
154        | Bvshl(lhs, rhs)
155        | Bvlshr(lhs, rhs)
156        | Bvashr(lhs, rhs)
157        | Concat(lhs, rhs) => {
158            uses_in_exp(uses, lhs);
159            uses_in_exp(uses, rhs)
160        }
161        Ite(cond, then_exp, else_exp) => {
162            uses_in_exp(uses, cond);
163            uses_in_exp(uses, then_exp);
164            uses_in_exp(uses, else_exp)
165        }
166        App(f, args) => {
167            uses.insert(*f, uses.get(&f).unwrap_or(&0) + 1);
168            for arg in args {
169                uses_in_exp(uses, arg);
170            }
171        }
172        Select(array, index) => {
173            uses_in_exp(uses, array);
174            uses_in_exp(uses, index)
175        }
176        Store(array, index, val) => {
177            uses_in_exp(uses, array);
178            uses_in_exp(uses, index);
179            uses_in_exp(uses, val)
180        }
181    }
182}
183
184fn uses_in_value<B>(uses: &mut HashMap<Sym, u32>, val: &Val<B>) {
185    use Val::*;
186    match val {
187        Symbolic(v) => {
188            uses.insert(*v, uses.get(&v).unwrap_or(&0) + 1);
189        }
190        I64(_) | I128(_) | Bool(_) | Bits(_) | Enum(_) | String(_) | Unit | Ref(_) | Poison => (),
191        List(vals) | Vector(vals) => vals.iter().for_each(|val| uses_in_value(uses, val)),
192        Struct(fields) => fields.iter().for_each(|(_, val)| uses_in_value(uses, val)),
193        Ctor(_, val) => uses_in_value(uses, val),
194    }
195}
196
197pub type Taints = HashSet<(Name, Vec<Accessor>)>;
198
199/// The `EventReferences` struct contains for every variable `v` in a
200/// trace, the set of all it's immediate dependencies, i.e. all the
201/// symbols used to directly define `v`, as computed by `uses_in_exp`.
202pub struct EventReferences {
203    references: HashMap<Sym, HashMap<Sym, u32>>,
204}
205
206impl EventReferences {
207    pub fn from_events<B, E: Borrow<Event<B>>>(events: &[E]) -> Self {
208        let mut references = HashMap::new();
209
210        for event in events.iter() {
211            if let Smt(Def::DefineConst(id, exp)) = event.borrow() {
212                let mut uses = HashMap::new();
213                uses_in_exp(&mut uses, exp);
214                references.insert(*id, uses);
215            }
216        }
217        EventReferences { references }
218    }
219
220    /// Follow all the dependencies of a symbol in the events,
221    /// returning the set of symbols it recursively depends on,
222    /// (including itself).
223    pub fn dependencies(&self, symbol: Sym) -> HashSet<Sym> {
224        let empty_map = HashMap::new();
225        // The dependencies for symbol
226        let mut deps = HashSet::new();
227        deps.insert(symbol);
228        // Add symbols to this set once all their immediate
229        // dependencies have been added to deps
230        let mut seen = HashSet::new();
231
232        loop {
233            let mut next = HashSet::new();
234
235            for symbol in deps.iter() {
236                if !seen.contains(symbol) {
237                    let immediate_deps = self.references.get(&symbol).unwrap_or_else(|| &empty_map);
238                    for k in immediate_deps.keys() {
239                        next.insert(*k);
240                    }
241                    seen.insert(*symbol);
242                }
243            }
244
245            // Terminate when we have no more dependencies to add
246            if next.is_empty() {
247                break;
248            } else {
249                for symbol in next.iter() {
250                    deps.insert(*symbol);
251                }
252            }
253        }
254
255        deps
256    }
257
258    /// Returns the set of registers a symbolic variable is tainted
259    /// by, i.e. any symbolic registers upon which the variable
260    /// depends upon. Also returns whether the value depends upon a
261    /// symbolic memory read.
262    pub fn taints<B: BV, E: Borrow<Event<B>>>(&self, symbol: Sym, events: &[E]) -> (Taints, bool) {
263        let mut taints = HashSet::new();
264        let mut memory = false;
265        self.collect_taints(symbol, events, &mut taints, &mut memory);
266        (taints, memory)
267    }
268
269    /// Like `taints` but for all symbolic variables in a value
270    pub fn value_taints<B: BV, E: Borrow<Event<B>>>(&self, val: &Val<B>, events: &[E]) -> (Taints, bool) {
271        let mut taints = HashSet::new();
272        let mut memory = false;
273        self.collect_value_taints(val, events, &mut taints, &mut memory);
274        (taints, memory)
275    }
276
277    pub fn collect_taints<B: BV, E: Borrow<Event<B>>>(
278        &self,
279        symbol: Sym,
280        events: &[E],
281        taints: &mut Taints,
282        memory: &mut bool,
283    ) {
284        let deps = self.dependencies(symbol);
285
286        for event in events.iter() {
287            match event.borrow() {
288                ReadReg(reg, accessor, value) => {
289                    let mut uses = HashMap::new();
290                    uses_in_value(&mut uses, value);
291                    for (taint, _) in uses.iter() {
292                        if deps.contains(taint) {
293                            taints.insert((*reg, accessor.clone()));
294                            break;
295                        }
296                    }
297                }
298
299                ReadMem { value: Val::Symbolic(taint), .. } if deps.contains(taint) => *memory = true,
300                ReadMem { tag_value: Some(Val::Symbolic(taint)), .. } if deps.contains(taint) => *memory = true,
301
302                _ => (),
303            }
304        }
305    }
306
307    pub fn collect_value_taints<B: BV, E: Borrow<Event<B>>>(
308        &self,
309        val: &Val<B>,
310        events: &[E],
311        taints: &mut Taints,
312        memory: &mut bool,
313    ) {
314        for symbol in val.symbolic_variables() {
315            self.collect_taints(symbol, events, taints, memory)
316        }
317    }
318}
319
320#[allow(clippy::unneeded_field_pattern)]
321fn calculate_uses<B, E: Borrow<Event<B>>>(events: &[E]) -> HashMap<Sym, u32> {
322    let mut uses: HashMap<Sym, u32> = HashMap::new();
323
324    for event in events.iter().rev() {
325        use Event::*;
326        match event.borrow() {
327            Smt(Def::DeclareConst(_, _)) => (),
328            Smt(Def::DeclareFun(_, _, _)) => (),
329            Smt(Def::DefineConst(_, exp)) => uses_in_exp(&mut uses, exp),
330            Smt(Def::DefineEnum(_, _)) => (),
331            Smt(Def::Assert(exp)) => uses_in_exp(&mut uses, exp),
332            ReadReg(_, _, val) => uses_in_value(&mut uses, val),
333            WriteReg(_, _, val) => uses_in_value(&mut uses, val),
334            ReadMem { value: val, read_kind, address, bytes: _, tag_value, kind: _ } => {
335                uses_in_value(&mut uses, val);
336                uses_in_value(&mut uses, read_kind);
337                uses_in_value(&mut uses, address);
338                if let Some(v) = tag_value {
339                    uses_in_value(&mut uses, v);
340                }
341            }
342            WriteMem { value: sym, write_kind, address, data, bytes: _, tag_value, kind: _ } => {
343                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
344                uses_in_value(&mut uses, write_kind);
345                uses_in_value(&mut uses, address);
346                uses_in_value(&mut uses, data);
347                if let Some(v) = tag_value {
348                    uses_in_value(&mut uses, v);
349                }
350            }
351            Branch { address } => uses_in_value(&mut uses, address),
352            Barrier { barrier_kind } => uses_in_value(&mut uses, barrier_kind),
353            CacheOp { cache_op_kind, address } => {
354                uses_in_value(&mut uses, cache_op_kind);
355                uses_in_value(&mut uses, address)
356            }
357            Fork(_, sym, _) => {
358                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
359            }
360            Cycle => (),
361            Instr(val) => uses_in_value(&mut uses, val),
362            Sleeping(sym) => {
363                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
364            }
365            MarkReg { .. } => (),
366            WakeupRequest => (),
367            SleepRequest => (),
368        }
369    }
370
371    uses
372}
373
374/// We cannot remove symbols from traces if they appear in a few
375/// places, this function returns the set of such symbols.
376fn calculate_required_uses<B, E: Borrow<Event<B>>>(events: &[E]) -> HashMap<Sym, u32> {
377    let mut uses: HashMap<Sym, u32> = HashMap::new();
378
379    for event in events.iter().rev() {
380        use Event::*;
381        match event.borrow() {
382            Smt(Def::DeclareConst(sym, _)) => {
383                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
384            }
385            Smt(Def::DeclareFun(sym, _, _)) => {
386                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
387            }
388            Smt(Def::DefineEnum(sym, _)) => {
389                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
390            }
391            Smt(_) => (),
392            ReadReg(_, _, val) => uses_in_value(&mut uses, val),
393            WriteReg(_, _, val) => uses_in_value(&mut uses, val),
394            ReadMem { value: val, read_kind, address, bytes: _, tag_value, kind: _ } => {
395                uses_in_value(&mut uses, val);
396                uses_in_value(&mut uses, read_kind);
397                uses_in_value(&mut uses, address);
398                if let Some(v) = tag_value {
399                    uses_in_value(&mut uses, v);
400                }
401            }
402            WriteMem { value: sym, write_kind, address, data, bytes: _, tag_value, kind: _ } => {
403                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
404                uses_in_value(&mut uses, write_kind);
405                uses_in_value(&mut uses, address);
406                uses_in_value(&mut uses, data);
407                if let Some(v) = tag_value {
408                    uses_in_value(&mut uses, v);
409                }
410            }
411            Branch { address } => uses_in_value(&mut uses, address),
412            Barrier { barrier_kind } => uses_in_value(&mut uses, barrier_kind),
413            CacheOp { cache_op_kind, address } => {
414                uses_in_value(&mut uses, cache_op_kind);
415                uses_in_value(&mut uses, address)
416            }
417            Fork(_, sym, _) => {
418                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
419            }
420            Cycle => (),
421            Instr(val) => uses_in_value(&mut uses, val),
422            Sleeping(sym) => {
423                uses.insert(*sym, uses.get(&sym).unwrap_or(&0) + 1);
424            }
425            MarkReg { .. } => (),
426            WakeupRequest => (),
427            SleepRequest => (),
428        }
429    }
430
431    uses
432}
433
434fn remove_unused_pass<B, E: Borrow<Event<B>>>(events: &mut Vec<E>) -> u32 {
435    let uses = calculate_uses(&events);
436    let mut removed = 0;
437
438    events.retain(|event| match event.borrow() {
439        Smt(Def::DeclareConst(v, _)) => {
440            if uses.contains_key(v) {
441                true
442            } else {
443                removed += 1;
444                false
445            }
446        }
447        Smt(Def::DefineConst(v, _)) => {
448            if uses.contains_key(v) {
449                true
450            } else {
451                removed += 1;
452                false
453            }
454        }
455        _ => true,
456    });
457
458    removed
459}
460
461/// Removes register effects from before the first `(cycle)`
462/// event. When combined with `remove_unused` this will reduce the
463/// amount of initialization that appears in the trace.
464pub fn hide_initialization<B: BV, E: Borrow<Event<B>>>(events: &mut Vec<E>) {
465    let mut keep = vec![true; events.len()];
466    let mut init_cycle = true;
467    for (i, event) in events.iter().enumerate().rev() {
468        match event.borrow() {
469            WriteReg { .. } if init_cycle => keep[i] = false,
470            ReadReg { .. } if init_cycle => keep[i] = false,
471            Cycle => init_cycle = false,
472            _ => (),
473        }
474    }
475    let mut i = 0;
476    events.retain(|_| {
477        i += 1;
478        keep[i - 1]
479    })
480}
481
482/// Removes SMT events that are not used by any observable event (such
483/// as a memory read or write).
484pub fn remove_unused<B: BV, E: Borrow<Event<B>>>(events: &mut Vec<E>) {
485    loop {
486        if remove_unused_pass(events) == 0 {
487            break;
488        }
489    }
490}
491
492/// This rewrite looks for events of the form `(define-const v
493/// (expression))`, and if `v` is only used exactly once in subsequent
494/// events it will replace that use of `v` by the expression.
495pub fn propagate_forwards_used_once<B: BV, E: BorrowMut<Event<B>>>(events: &mut Vec<E>) {
496    let uses = calculate_uses(&events);
497    let required_uses = calculate_required_uses(&events);
498
499    let mut substs: HashMap<Sym, Option<Exp>> = HashMap::new();
500
501    for (sym, count) in uses {
502        if count == 1 && !required_uses.contains_key(&sym) {
503            substs.insert(sym, None);
504        }
505    }
506
507    let mut keep = vec![true; events.len()];
508
509    for (i, event) in events.iter_mut().enumerate().rev() {
510        match event.borrow_mut() {
511            Event::Smt(Def::DefineConst(sym, exp)) => {
512                exp.subst_once_in_place(&mut substs);
513
514                if substs.contains_key(&sym) {
515                    let exp = std::mem::replace(exp, Exp::Bool(false));
516                    keep[i] = false;
517                    substs.insert(*sym, Some(exp));
518                }
519            }
520            Event::Smt(Def::Assert(exp)) => exp.subst_once_in_place(&mut substs),
521            _ => (),
522        }
523    }
524
525    let mut i = 0;
526    events.retain(|_| {
527        i += 1;
528        keep[i - 1]
529    })
530}
531
532/// Evaluate SMT subexpressions if all their arguments are constant
533pub fn eval<B: BV, E: BorrowMut<Event<B>>>(events: &mut Vec<E>) {
534    for event in events.iter_mut() {
535        match event.borrow_mut() {
536            Event::Smt(Def::DefineConst(_, exp)) | Event::Smt(Def::Assert(exp)) => {
537                let e = std::mem::replace(exp, Exp::Bool(false));
538                *exp = e.eval();
539            }
540            _ => (),
541        }
542    }
543}
544
545/// This rewrite pushes extract expressions inwards where possible, so
546/// ```text
547/// (extract (f a b))
548/// ```
549/// would be re-written to
550/// ```text
551/// (f (extract a) (extract b))
552/// ```
553///
554/// This enables further simplifications (such as the extract
555/// cancelling with an inner zero extend), which have the end result
556/// of reducing the size of bitvectors contained within the generated
557/// SMT.
558pub fn commute_extract<B: BV, E: BorrowMut<Event<B>>>(events: &mut Vec<E>) {
559    for event in events.iter_mut() {
560        match event.borrow_mut() {
561            Event::Smt(Def::DefineConst(_, exp)) | Event::Smt(Def::Assert(exp)) => exp.modify_top_down(&Exp::commute_extract),
562            _ => (),
563        }
564    }
565}
566
567fn accessor_to_string(acc: &[Accessor], symtab: &Symtab) -> String {
568    acc.iter()
569        .map(|elem| elem.to_string(symtab))
570        .fold(None, |acc, elem| if let Some(prefix) = acc { Some(format!("{} {}", prefix, elem)) } else { Some(elem) })
571        .map_or("nil".to_string(), |acc| format!("({})", acc))
572}
573
574/// Options for writing event traces
575pub struct WriteOpts {
576    /// A prefix for all variable identifiers
577    pub variable_prefix: String,
578    /// The prefix for enumeration members
579    pub enum_prefix: String,
580    /// Will add type annotations to DefineConst constructors
581    pub types: bool,
582    /// If true, just print the SMT parts of the trace. When false,
583    /// the trace is also wrapped in a `(trace ...)` S-expression.
584    pub just_smt: bool,
585    /// Print the sizes of enumerations declared during symbolic
586    /// evaluation.
587    pub define_enum: bool,
588}
589
590impl WriteOpts {
591    pub fn smtlib() -> Self {
592        WriteOpts {
593            variable_prefix: "v".to_string(),
594            enum_prefix: "e".to_string(),
595            types: true,
596            just_smt: true,
597            define_enum: false,
598        }
599    }
600}
601
602impl Default for WriteOpts {
603    fn default() -> Self {
604        WriteOpts {
605            variable_prefix: "v".to_string(),
606            enum_prefix: "e".to_string(),
607            types: false,
608            just_smt: false,
609            define_enum: true,
610        }
611    }
612}
613
614fn write_bits(buf: &mut dyn Write, bits: &[bool]) -> std::io::Result<()> {
615    if bits.len() % 4 == 0 {
616        write!(buf, "#x")?;
617        for i in (0..(bits.len() / 4)).rev() {
618            let j = i * 4;
619            let hex = (if bits[j] { 0b0001 } else { 0 })
620                | (if bits[j + 1] { 0b0010 } else { 0 })
621                | (if bits[j + 2] { 0b0100 } else { 0 })
622                | (if bits[j + 3] { 0b1000 } else { 0 });
623            write!(buf, "{:x}", hex)?;
624        }
625    } else {
626        write!(buf, "#b")?;
627        for bit in bits.iter().rev() {
628            if *bit {
629                write!(buf, "1")?
630            } else {
631                write!(buf, "0")?
632            }
633        }
634    }
635    Ok(())
636}
637
638fn write_exp(buf: &mut dyn Write, exp: &Exp, opts: &WriteOpts, enums: &[usize]) -> std::io::Result<()> {
639    use Exp::*;
640    match exp {
641        Var(v) => write!(buf, "{}{}", opts.variable_prefix, v),
642        Bits(bv) => write_bits(buf, bv),
643        Bits64(bv) => write_bits64(buf, bv.lower_u64(), bv.len()),
644        Enum(e) => write!(buf, "{}{}_{}", opts.enum_prefix, enums[e.enum_id], e.member),
645        Bool(b) => write!(buf, "{}", b),
646        Eq(lhs, rhs) => write_binop(buf, "=", lhs, rhs, opts, enums),
647        Neq(lhs, rhs) => {
648            write!(buf, "(not ")?;
649            write_binop(buf, "=", lhs, rhs, opts, enums)?;
650            write!(buf, ")")
651        }
652        And(lhs, rhs) => write_binop(buf, "and", lhs, rhs, opts, enums),
653        Or(lhs, rhs) => write_binop(buf, "or", lhs, rhs, opts, enums),
654        Not(exp) => write_unop(buf, "not", exp, opts, enums),
655        Bvnot(exp) => write_unop(buf, "bvnot", exp, opts, enums),
656        Bvand(lhs, rhs) => write_binop(buf, "bvand", lhs, rhs, opts, enums),
657        Bvor(lhs, rhs) => write_binop(buf, "bvor", lhs, rhs, opts, enums),
658        Bvxor(lhs, rhs) => write_binop(buf, "bvxor", lhs, rhs, opts, enums),
659        Bvnand(lhs, rhs) => write_binop(buf, "bvnand", lhs, rhs, opts, enums),
660        Bvnor(lhs, rhs) => write_binop(buf, "bvnor", lhs, rhs, opts, enums),
661        Bvxnor(lhs, rhs) => write_binop(buf, "bvxnor", lhs, rhs, opts, enums),
662        Bvneg(exp) => write_unop(buf, "bvneg", exp, opts, enums),
663        Bvadd(lhs, rhs) => write_binop(buf, "bvadd", lhs, rhs, opts, enums),
664        Bvsub(lhs, rhs) => write_binop(buf, "bvsub", lhs, rhs, opts, enums),
665        Bvmul(lhs, rhs) => write_binop(buf, "bvmul", lhs, rhs, opts, enums),
666        Bvudiv(lhs, rhs) => write_binop(buf, "bvudiv", lhs, rhs, opts, enums),
667        Bvsdiv(lhs, rhs) => write_binop(buf, "bvsdiv", lhs, rhs, opts, enums),
668        Bvurem(lhs, rhs) => write_binop(buf, "bvurem", lhs, rhs, opts, enums),
669        Bvsrem(lhs, rhs) => write_binop(buf, "bvsrem", lhs, rhs, opts, enums),
670        Bvsmod(lhs, rhs) => write_binop(buf, "bvsmod", lhs, rhs, opts, enums),
671        Bvult(lhs, rhs) => write_binop(buf, "bvult", lhs, rhs, opts, enums),
672        Bvslt(lhs, rhs) => write_binop(buf, "bvslt", lhs, rhs, opts, enums),
673        Bvule(lhs, rhs) => write_binop(buf, "bvule", lhs, rhs, opts, enums),
674        Bvsle(lhs, rhs) => write_binop(buf, "bvsle", lhs, rhs, opts, enums),
675        Bvuge(lhs, rhs) => write_binop(buf, "bvuge", lhs, rhs, opts, enums),
676        Bvsge(lhs, rhs) => write_binop(buf, "bvsge", lhs, rhs, opts, enums),
677        Bvugt(lhs, rhs) => write_binop(buf, "bvugt", lhs, rhs, opts, enums),
678        Bvsgt(lhs, rhs) => write_binop(buf, "bvsgt", lhs, rhs, opts, enums),
679        Extract(i, j, exp) => {
680            write!(buf, "((_ extract {} {}) ", i, j)?;
681            write_exp(buf, exp, opts, enums)?;
682            write!(buf, ")")
683        }
684        ZeroExtend(n, exp) => {
685            write!(buf, "((_ zero_extend {}) ", n)?;
686            write_exp(buf, exp, opts, enums)?;
687            write!(buf, ")")
688        }
689        SignExtend(n, exp) => {
690            write!(buf, "((_ sign_extend {}) ", n)?;
691            write_exp(buf, exp, opts, enums)?;
692            write!(buf, ")")
693        }
694        Bvshl(lhs, rhs) => write_binop(buf, "bvshl", lhs, rhs, opts, enums),
695        Bvlshr(lhs, rhs) => write_binop(buf, "bvlshr", lhs, rhs, opts, enums),
696        Bvashr(lhs, rhs) => write_binop(buf, "bvashr", lhs, rhs, opts, enums),
697        Concat(lhs, rhs) => write_binop(buf, "concat", lhs, rhs, opts, enums),
698        Ite(cond, then_exp, else_exp) => {
699            write!(buf, "(ite ")?;
700            write_exp(buf, cond, opts, enums)?;
701            write!(buf, " ")?;
702            write_exp(buf, then_exp, opts, enums)?;
703            write!(buf, " ")?;
704            write_exp(buf, else_exp, opts, enums)?;
705            write!(buf, ")")
706        }
707        App(f, args) => {
708            write!(buf, "({}{}", opts.variable_prefix, f)?;
709            for arg in args {
710                write!(buf, " ")?;
711                write_exp(buf, arg, opts, enums)?;
712            }
713            write!(buf, ")")
714        }
715        Select(array, index) => write_binop(buf, "select", array, index, opts, enums),
716        Store(array, index, val) => {
717            write!(buf, "(store ")?;
718            write_exp(buf, array, opts, enums)?;
719            write!(buf, " ")?;
720            write_exp(buf, index, opts, enums)?;
721            write!(buf, " ")?;
722            write_exp(buf, val, opts, enums)?;
723            write!(buf, ")")
724        }
725    }
726}
727
728fn write_unop(buf: &mut dyn Write, op: &str, exp: &Exp, opts: &WriteOpts, enums: &[usize]) -> std::io::Result<()> {
729    write!(buf, "({} ", op)?;
730    write_exp(buf, exp, opts, enums)?;
731    write!(buf, ")")
732}
733
734fn write_binop(
735    buf: &mut dyn Write,
736    op: &str,
737    lhs: &Exp,
738    rhs: &Exp,
739    opts: &WriteOpts,
740    enums: &[usize],
741) -> std::io::Result<()> {
742    write!(buf, "({} ", op)?;
743    write_exp(buf, lhs, opts, enums)?;
744    write!(buf, " ")?;
745    write_exp(buf, rhs, opts, enums)?;
746    write!(buf, ")")
747}
748
749pub fn write_events_with_opts<B: BV>(
750    buf: &mut dyn Write,
751    events: &[Event<B>],
752    symtab: &Symtab,
753    opts: &WriteOpts,
754) -> std::io::Result<()> {
755    let mut tcx: HashMap<Sym, Ty> = HashMap::new();
756    let mut ftcx: HashMap<Sym, (Vec<Ty>, Ty)> = HashMap::new();
757    let mut enums: Vec<usize> = Vec::new();
758
759    if !opts.just_smt {
760        write!(buf, "(trace").unwrap();
761    }
762    for event in events.iter().filter(|ev| !opts.just_smt || ev.is_smt()) {
763        (match event {
764            // TODO: rename this
765            Fork(n, _, loc) => write!(buf, "\n  (branch {} \"{}\")", n, loc),
766
767            Smt(Def::DefineEnum(_, size)) if !opts.define_enum => {
768                enums.push(*size);
769                Ok(())
770            }
771
772            Smt(def) => {
773                if opts.just_smt {
774                    writeln!(buf)?
775                } else {
776                    write!(buf, "\n  ")?;
777                }
778                match def {
779                    Def::DeclareConst(v, ty) => {
780                        tcx.insert(*v, ty.clone());
781                        write!(buf, "(declare-const {}{} {})", opts.variable_prefix, v, ty)
782                    }
783                    Def::DeclareFun(v, arg_tys, result_ty) => {
784                        ftcx.insert(*v, (arg_tys.clone(), result_ty.clone()));
785                        write!(buf, "(declare_fun {}{} (", opts.variable_prefix, v)?;
786                        for ty in arg_tys {
787                            write!(buf, "{} ", ty)?
788                        }
789                        write!(buf, ") {})", result_ty)
790                    }
791                    Def::DefineConst(v, exp) => {
792                        if opts.types {
793                            let ty = exp.infer(&tcx, &ftcx).expect("SMT expression was badly-typed");
794                            tcx.insert(*v, ty.clone());
795                            write!(buf, "(define-const v{} {} ", v, ty)?;
796                            write_exp(buf, exp, opts, &enums)?;
797                            write!(buf, ")")
798                        } else {
799                            write!(buf, "(define-const v{} ", v)?;
800                            write_exp(buf, exp, opts, &enums)?;
801                            write!(buf, ")")
802                        }
803                    }
804                    Def::DefineEnum(_, size) => {
805                        if !opts.just_smt {
806                            write!(buf, "(define-enum {})", size)?
807                        }
808                        enums.push(*size);
809                        Ok(())
810                    }
811                    Def::Assert(exp) => {
812                        write!(buf, "(assert ")?;
813                        write_exp(buf, exp, opts, &enums)?;
814                        write!(buf, ")")
815                    }
816                }
817            }
818
819            ReadMem { value, read_kind, address, bytes, tag_value, kind: _ } => write!(
820                buf,
821                "\n  (read-mem {} {} {} {} {})",
822                value.to_string(symtab),
823                read_kind.to_string(symtab),
824                address.to_string(symtab),
825                bytes,
826                match tag_value {
827                    None => "None".to_string(),
828                    Some(v) => format!("Some({})", v.to_string(symtab)),
829                }
830            ),
831
832            WriteMem { value, write_kind, address, data, bytes, tag_value, kind: _ } => write!(
833                buf,
834                "\n  (write-mem v{} {} {} {} {} {})",
835                value,
836                write_kind.to_string(symtab),
837                address.to_string(symtab),
838                data.to_string(symtab),
839                bytes,
840                match tag_value {
841                    None => "None".to_string(),
842                    Some(v) => format!("Some({})", v.to_string(symtab)),
843                }
844            ),
845
846            Branch { address } => write!(buf, "\n  (branch-address {})", address.to_string(symtab)),
847
848            Barrier { barrier_kind } => write!(buf, "\n  (barrier {})", barrier_kind.to_string(symtab)),
849
850            CacheOp { cache_op_kind, address } => {
851                write!(buf, "\n  (cache-op {} {})", cache_op_kind.to_string(symtab), address.to_string(symtab))
852            }
853
854            WriteReg(n, acc, v) => write!(
855                buf,
856                "\n  (write-reg |{}| {} {})",
857                zencode::decode(symtab.to_str(*n)),
858                accessor_to_string(acc, symtab),
859                v.to_string(symtab)
860            ),
861
862            ReadReg(n, acc, v) => {
863                if *n == HAVE_EXCEPTION {
864                    Ok(())
865                } else {
866                    write!(
867                        buf,
868                        "\n  (read-reg |{}| {} {})",
869                        zencode::decode(symtab.to_str(*n)),
870                        accessor_to_string(acc, symtab),
871                        v.to_string(symtab)
872                    )
873                }
874            }
875
876            MarkReg { regs, mark } => {
877                for reg in regs {
878                    write!(buf, "\n  (mark-reg |{}| \"{}\")", zencode::decode(symtab.to_str(*reg)), mark)?
879                }
880                Ok(())
881            }
882
883            Cycle => write!(buf, "\n  (cycle)"),
884
885            Instr(value) => write!(buf, "\n  (instr {})", value.to_string(symtab)),
886
887            Sleeping(value) => write!(buf, "\n  (sleeping v{})", value),
888
889            SleepRequest => write!(buf, "\n  (sleep-request)"),
890
891            WakeupRequest => write!(buf, "\n  (wake-request)"),
892        })?
893    }
894    if !opts.just_smt {
895        writeln!(buf, ")")?;
896    }
897    Ok(())
898}
899
900pub fn write_events<B: BV>(buf: &mut dyn Write, events: &[Event<B>], symtab: &Symtab) {
901    write_events_with_opts(buf, events, symtab, &WriteOpts::default()).unwrap()
902}
isla_lib/simplify.rs

isla_lib/
simplify.rs
