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
|
#pragma once
#include<inttypes.h>
#include<stdlib.h>
#include<stdio.h>
#include"sail.h"
/*
* This function should be called whenever a pattern match failure
* occurs. Pattern match failures are always fatal.
*/
void sail_match_failure(sail_string msg);
/*
* sail_assert implements the assert construct in Sail. If any
* assertion fails we immediately exit the model.
*/
unit sail_assert(bool b, sail_string msg);
unit sail_exit(unit);
/*
* ASL->Sail model has an EnterLowPowerState() function that calls a
* sleep request builtin. If it gets called we print a message and
* exit the model.
*/
unit sleep_request(const unit u);
/* ***** Memory builtins ***** */
void write_mem(uint64_t, uint64_t);
uint64_t read_mem(uint64_t);
// These memory builtins are intended to match the semantics for the
// __ReadRAM and __WriteRAM functions in ASL.
unit write_ram(const mpz_t addr_size, // Either 32 or 64
const mpz_t data_size_mpz, // Number of bytes
const sail_bits hex_ram, // Currently unused
const sail_bits addr_bv,
const sail_bits data);
void read_ram(sail_bits *data,
const mpz_t addr_size,
const mpz_t data_size_mpz,
const sail_bits hex_ram,
const sail_bits addr_bv);
unit load_raw(mach_bits addr, const sail_string file);
void load_image(char *);
/* ***** Tracing ***** */
static int64_t g_trace_depth;
static int64_t g_trace_max_depth;
static bool g_trace_enabled;
/*
* Bind these functions in Sail to enable and disable tracing (see
* lib/trace.sail):
*
* val "enable_tracing" : unit -> unit
* val "disable_tracing" : unit -> unit
* val "is_tracing" : unit -> bool
*
* Compile with sail -c -c_trace.
*/
unit enable_tracing(const unit);
unit disable_tracing(const unit);
bool is_tracing(const unit);
/*
* Tracing is implemented by void trace_TYPE functions, each of which
* takes the Sail value to print as the first argument, and prints it
* directly to stderr with no linebreaks.
*
* For types that don't have printing function we have trace_unknown,
* which simply prints '?'. trace_argsep, trace_argend, and
* trace_retend are used for formatting function arguments. They won't
* overlap with user defined types because the type names used for
* TYPE are zencoded. trace_start(NAME) and trace_end() are called
* before printing the function arguments and return value
* respectively.
*/
void trace_sail_int(const sail_int);
void trace_bool(const bool);
void trace_unit(const unit);
void trace_sail_string(const sail_string);
void trace_mach_bits(const mach_bits);
void trace_sail_bits(const sail_bits);
void trace_unknown(void);
void trace_argsep(void);
void trace_argend(void);
void trace_retend(void);
void trace_start(char *);
void trace_end(void);
/*
* Functions to get info from ELF files.
*/
static uint64_t g_elf_entry;
void elf_entry(sail_int *rop, const unit u);
void elf_tohost(sail_int *rop, const unit u);
/*
* setup_rts and cleanup_rts are responsible for calling setup_library
* and cleanup_library in sail.h.
*/
void setup_rts(void);
void cleanup_rts(void);
|