1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119

// BSD 2-Clause License
//
// Copyright (c) 2019, 2020 Alasdair Armstrong
//
// All rights reserved.
// 
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:
// 
// 1. Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimer.
// 
// 2. Redistributions in binary form must reproduce the above copyright
// notice, this list of conditions and the following disclaimer in the
// documentation and/or other materials provided with the distribution.
// 
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

use std::collections::HashMap;
use std::sync::Mutex;

use crate::concrete::BV;
use crate::config::ISAConfig;
use crate::executor::{start_single, LocalFrame};
use crate::ir::*;
use crate::log;
use crate::zencode;

fn initialize_letbindings<'ir, B: BV>(
    arch: &'ir [Def<Name, B>],
    shared_state: &SharedState<'ir, B>,
    regs: &Bindings<'ir, B>,
    letbindings: &Mutex<Bindings<'ir, B>>,
) {
    for def in arch.iter() {
        if let Def::Let(bindings, setup) = def {
            let vars: Vec<_> = bindings.iter().map(|(id, ty)| (*id, ty)).collect();
            let task = {
                let lets = letbindings.lock().unwrap();
                LocalFrame::new(&vars, None, setup).add_regs(&regs).add_lets(&lets).task(0)
            };

            start_single(
                task,
                &shared_state,
                &letbindings,
                &move |_tid, _task_id, result, shared_state, _solver, letbindings| match result {
                    Ok((_, frame)) => {
                        for (id, _) in bindings.iter() {
                            let symbol = zencode::decode(shared_state.symtab.to_str(*id));
                            match frame.vars().get(id) {
                                Some(value) => {
                                    let mut state = letbindings.lock().unwrap();
                                    state.insert(*id, value.clone());
                                    let symbol = zencode::decode(shared_state.symtab.to_str(*id));
                                    log!(log::VERBOSE, &format!("{} = {:?}", symbol, value));
                                }
                                None => log!(log::VERBOSE, &format!("No value for symbol {}", symbol)),
                            }
                        }
                    }
                    Err(err) => log!(log::VERBOSE, &format!("Failed to evaluate letbinding: {:?}", err)),
                },
            );
        }
    }
}

fn initialize_register_state<'ir, B: BV>(
    defs: &'ir [Def<Name, B>],
    initial_registers: &HashMap<Name, Val<B>>,
) -> Bindings<'ir, B> {
    let mut registers = HashMap::new();
    for def in defs.iter() {
        if let Def::Register(id, ty) = def {
            if let Some(value) = initial_registers.get(id) {
                registers.insert(*id, UVal::Init(value.clone()));
            } else {
                registers.insert(*id, UVal::Uninit(ty));
            }
        }
    }
    registers
}

pub struct Initialized<'ir, B> {
    pub regs: Bindings<'ir, B>,
    pub lets: Bindings<'ir, B>,
    pub shared_state: SharedState<'ir, B>,
}

pub fn initialize_architecture<'ir, B: BV>(
    arch: &'ir mut [Def<Name, B>],
    symtab: Symtab<'ir>,
    isa_config: &ISAConfig<B>,
    mode: AssertionMode,
) -> Initialized<'ir, B> {
    insert_monomorphize(arch);
    insert_primops(arch, mode);

    let regs = initialize_register_state(arch, &isa_config.default_registers);
    let lets = Mutex::new(HashMap::new());
    let shared_state = SharedState::new(symtab, arch, isa_config.probes.clone());

    initialize_letbindings(arch, &shared_state, &regs, &lets);

    Initialized { regs, lets: lets.into_inner().unwrap(), shared_state }
}