isla_axiomatic/
graph.rs

1// BSD 2-Clause License
2//
3// Copyright (c) 2020 Alasdair Armstrong
4//
5// All rights reserved.
6//
7// Redistribution and use in source and binary forms, with or without
8// modification, are permitted provided that the following conditions are
9// met:
10//
11// 1. Redistributions of source code must retain the above copyright
12// notice, this list of conditions and the following disclaimer.
13//
14// 2. Redistributions in binary form must reproduce the above copyright
15// notice, this list of conditions and the following disclaimer in the
16// documentation and/or other materials provided with the distribution.
17//
18// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
19// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
20// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
21// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
22// HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
23// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
24// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
25// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
26// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
27// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
28// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
29
30use serde::{Deserialize, Serialize};
31use std::collections::{HashMap, HashSet};
32use std::error::Error;
33use std::fmt;
34use std::sync::atomic::{AtomicUsize, Ordering};
35
36use isla_lib::bitvector::BV;
37use isla_lib::ir::*;
38use isla_lib::smt::Event;
39
40use isla_cat::cat;
41
42use crate::axiomatic::model::Model;
43use crate::axiomatic::relations;
44use crate::axiomatic::{AxEvent, ExecutionInfo, Pairs, ThreadId};
45use crate::footprint_analysis::Footprint;
46use crate::litmus::instruction_from_objdump;
47use crate::litmus::Litmus;
48use crate::sexp::{InterpretError, SexpVal};
49
50#[derive(Serialize, Deserialize, Debug, Clone)]
51pub struct GraphEvent {
52    instr: Option<String>,
53    opcode: String,
54    po: usize,
55    thread_id: ThreadId,
56    name: String,
57    value: Option<String>,
58    color: Option<String>,
59}
60
61fn event_color<B: BV>(ev: &AxEvent<B>) -> Option<String> {
62    match ev.base {
63        Event::ReadMem { kind, .. } | Event::WriteMem { kind, .. } => {
64            if kind == &"stage 1" {
65                Some("darkslategray1".to_string())
66            } else if kind == &"stage 2" {
67                Some("wheat1".to_string())
68            } else {
69                None
70            }
71        }
72        _ => None,   
73    }
74}
75
76impl GraphEvent {
77    /// Create an event to display in a user-visible graph from an
78    /// underlying axiomatic event. For display, we use the objdump
79    /// output to find the human-readable assembly instruction, and
80    /// get values read/written by memory events as an event name ->
81    /// read/write description map.
82    pub fn from_axiomatic<'a, B: BV>(
83        ev: &'a AxEvent<B>,
84        objdump: &str,
85        rw_values: &mut HashMap<String, String>,
86    ) -> Self {
87        let instr = instruction_from_objdump(&format!("{:x}", ev.opcode), objdump);
88        GraphEvent {
89            instr,
90            opcode: format!("{}", ev.opcode),
91            po: ev.po,
92            thread_id: ev.thread_id,
93            name: ev.name.clone(),
94            value: rw_values.remove(&ev.name),
95            color: event_color(ev),
96        }
97    }
98}
99
100#[derive(Serialize, Deserialize, Debug, Clone)]
101pub struct GraphSet {
102    pub name: String,
103    pub elems: Vec<String>,
104}
105
106#[derive(Serialize, Deserialize, Debug, Clone)]
107pub struct GraphRelation {
108    pub name: String,
109    pub edges: Vec<(String, String)>,
110}
111
112#[derive(Serialize, Deserialize, Debug, Clone)]
113pub struct Graph {
114    pub events: Vec<GraphEvent>,
115    pub sets: Vec<GraphSet>,
116    pub relations: Vec<GraphRelation>,
117    pub show: Vec<String>,
118}
119
120static NEXT_COLOR: AtomicUsize = AtomicUsize::new(0);
121
122fn extra_color() -> &'static str {
123    let colors = [
124        "seagreen",
125        "steelblue",
126        "violetred",
127        "royalblue",
128        "orangered",
129        "navy",
130        "hotpink",
131        "green4",
132        "dogerblue",
133        "chartreuse3",
134        "darkorchid",
135        "coral3",
136        "darkolivegreen",
137        "cyan4",
138    ];
139    let n = NEXT_COLOR.fetch_add(1, Ordering::SeqCst);
140    colors[n % colors.len()]
141}
142
143fn relation_color(rel: &str) -> &'static str {
144    match rel {
145        "rf" => "crimson",
146        "co" => "goldenrod",
147        "fr" => "limegreen",
148        "addr" => "blue2",
149        "data" => "darkgreen",
150        "ctrl" => "darkorange2",
151        "rmw" => "firebrick4",
152        _ => extra_color(),
153    }
154}
155
156impl fmt::Display for Graph {
157    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
158        writeln!(f, "digraph Exec {{")?;
159        writeln!(f, "  IW [label=\"Initial State\",shape=hexagon];")?;
160
161        let mut thread_ids = HashSet::new();
162        for ev in &self.events {
163            thread_ids.insert(ev.thread_id);
164        }
165
166        for tid in thread_ids {
167            writeln!(f, "  subgraph cluster{} {{", tid)?;
168            writeln!(f, "    label=\"Thread #{}\"", tid)?;
169            writeln!(f, "    style=dashed")?;
170            writeln!(f, "    color=gray50")?;
171
172            let mut lowest_po = None;
173            let mut lowest_name = "";
174
175            let events: Vec<&GraphEvent> = self.events.iter().filter(|ev| ev.thread_id == tid).collect();
176
177            for ev in &events {
178                let instr = ev.instr.as_ref().unwrap_or(&ev.opcode);
179                let color = if let Some(color) = &ev.color {
180                    format!(",fillcolor={},style=filled", color)
181                } else {
182                    "".to_string()
183                };
184                
185                if let Some(value) = &ev.value {
186                    writeln!(f, "    {} [shape=box,label=\"{}\\l{}\"{}];", ev.name, instr, value, color)?;
187                } else {
188                    writeln!(f, "    {} [shape=box,label=\"{}\"{}];", ev.name, instr, color)?;
189                }
190
191                if lowest_po.is_none() || ev.po < lowest_po.unwrap() {
192                    lowest_po = Some(ev.po);
193                    lowest_name = &ev.name;
194                }
195            }
196
197            write!(f, "    ")?;
198            for (i, ev) in events.iter().enumerate() {
199                let last = i == events.len() - 1;
200                write!(f, "{}{}", ev.name, if last { ";\n" } else { " -> " })?;
201            }
202            writeln!(f, "  }}")?;
203
204            if lowest_po.is_some() {
205                writeln!(f, "  IW -> {} [style=invis,constraint=true]", lowest_name)?;
206            }
207        }
208
209        for to_show in &self.show {
210            for rel in &self.relations {
211                if rel.name == *to_show && !rel.edges.is_empty() {
212                    for (from, to) in &rel.edges {
213                        if !(rel.name == "rf" && from == "IW") {
214                            let color = relation_color(&rel.name);
215                            writeln!(
216                                f,
217                                "  {} -> {} [color={},label=\"  {}  \",fontcolor={}]",
218                                from, to, color, rel.name, color
219                            )?;
220                        }
221                    }
222                }
223            }
224        }
225
226        writeln!(f, "}}")
227    }
228}
229
230#[derive(Debug, Clone)]
231pub enum GraphError {
232    /// Will be caused if we cannot parse the SMT solver (z3) output
233    /// as a valid S-expression model.
234    SmtParseError,
235    /// Will be caused if we fail to interpret part of the model.
236    InterpretError(InterpretError),
237}
238
239impl fmt::Display for GraphError {
240    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
241        use GraphError::*;
242        match self {
243            SmtParseError => write!(f, "Failed to parse smt model"),
244            InterpretError(err) => write!(f, "{}", err),
245        }
246    }
247}
248
249impl Error for GraphError {
250    fn source(&self) -> Option<&(dyn Error + 'static)> {
251        None
252    }
253}
254
255/// Generate a graph from the output of a Z3 invocation that returned sat.
256pub fn graph_from_z3_output<B: BV>(
257    exec: ExecutionInfo<B>,
258    footprints: &HashMap<B, Footprint>,
259    z3_output: &str,
260    litmus: &Litmus<B>,
261    cat: &cat::Cat<cat::Ty>,
262    ifetch: bool,
263) -> Result<Graph, GraphError> {
264    use GraphError::*;
265
266    let mut event_names: Vec<&str> = exec.events.iter().map(|ev| ev.name.as_ref()).collect();
267    event_names.push("IW");
268    let model_buf = &z3_output[3..];
269    let mut model = Model::<B>::parse(&event_names, model_buf).ok_or(SmtParseError)?;
270
271    // We want to collect all the relations that were found by the SMT solver as part of the
272    // model, as well as the addr/data/ctrl etc raltions we passed as input to the solver so we
273    // can send them back to the client to be drawn.
274    let mut relations: Vec<GraphRelation> = Vec::new();
275
276    let footprint_relations: [(&str, relations::DepRel<B>); 4] =
277        [("addr", relations::addr), ("data", relations::data), ("ctrl", relations::ctrl), ("rmw", relations::rmw)];
278
279    for (name, rel) in footprint_relations.iter() {
280        let edges: Vec<(&AxEvent<B>, &AxEvent<B>)> = Pairs::from_slice(&exec.events)
281            .filter(|(ev1, ev2)| rel(ev1, ev2, &exec.thread_opcodes, footprints))
282            .collect();
283        relations.push(GraphRelation {
284            name: (*name).to_string(),
285            edges: edges.iter().map(|(from, to)| (from.name.clone(), to.name.clone())).collect(),
286        })
287    }
288
289    let mut builtin_relations = vec!["rf", "co"];
290    if ifetch {
291        builtin_relations.push("irf")
292    }
293
294    for rel in cat.relations().iter().chain(builtin_relations.iter()) {
295        let edges = model.interpret_rel(rel, &event_names).map_err(InterpretError)?;
296        relations.push(GraphRelation {
297            name: (*rel).to_string(),
298            edges: edges.iter().map(|(from, to)| ((*from).to_string(), (*to).to_string())).collect(),
299        })
300    }
301
302    // Now we want to get the memory read and write values for each event
303    let mut rw_values: HashMap<String, String> = HashMap::new();
304
305    for event in exec.events.iter() {
306        fn interpret<B: BV>(
307            model: &mut Model<B>,
308            ev: &str,
309            prefix: &str,
310            value: &Val<B>,
311            bytes: u32,
312            address: &Val<B>,
313        ) -> String {
314            let value = if value.is_symbolic() {
315                model
316                    .interpret(&format!("{}:value", ev), &[])
317                    .map(SexpVal::into_int_string)
318                    .unwrap_or_else(|_| "?".to_string())
319            } else {
320                value.as_bits().map(|bv| bv.signed().to_string()).unwrap_or_else(|| "?".to_string())
321            };
322
323            let address = if address.is_symbolic() {
324                model
325                    .interpret(&format!("{}:address", ev), &[])
326                    .map(SexpVal::into_truncated_string)
327                    .unwrap_or_else(|_| "?".to_string())
328            } else {
329                address.as_bits().map(|bv| format!("#x{:x}", bv)).unwrap_or_else(|| "?".to_string())
330            };
331
332            format!("{} {} ({}): {}", prefix, address, bytes, value)
333        }
334
335        match event.base {
336            Event::ReadMem { value, address, bytes, .. } => {
337                rw_values.insert(
338                    event.name.clone(),
339                    interpret(
340                        &mut model,
341                        &event.name,
342                        if event.is_ifetch { "IF" } else { "R" },
343                        value,
344                        *bytes,
345                        address,
346                    ),
347                );
348            }
349            Event::WriteMem { data, address, bytes, .. } => {
350                rw_values.insert(event.name.clone(), interpret(&mut model, &event.name, "W", data, *bytes, address));
351            }
352            _ => (),
353        }
354    }
355
356    Ok(Graph {
357        events: exec.events.iter().map(|ev| GraphEvent::from_axiomatic(ev, &litmus.objdump, &mut rw_values)).collect(),
358        sets: vec![],
359        relations,
360        show: cat.shows(),
361    })
362}
isla_axiomatic/graph.rs

isla_axiomatic/
graph.rs
