diff options
| -rw-r--r-- | lib/rts.c | 15 | ||||
| -rw-r--r-- | lib/rts.h | 3 | ||||
| -rw-r--r-- | src/c_backend.ml | 6 |
3 files changed, 22 insertions, 2 deletions
@@ -238,6 +238,21 @@ bool write_ram(const mpz_t addr_size, // Either 32 or 64 return true; } +sbits fast_read_ram(const int64_t data_size, + const uint64_t addr) +{ + uint64_t r = 0; + + uint64_t byte; + for(uint64_t i = (uint64_t) data_size; i > 0; --i) { + byte = read_mem(addr + (i - 1)); + r = r << 8; + r = r + byte; + } + sbits res = {.len = data_size * 8, .bits = r }; + return res; +} + void read_ram(lbits *data, const mpz_t addr_size, const mpz_t data_size_mpz, @@ -65,6 +65,9 @@ void read_ram(lbits *data, const lbits hex_ram, const lbits addr_bv); +sbits fast_read_ram(const int64_t data_size, + const uint64_t addr_bv); + unit write_tag_bool(const fbits, const bool); bool read_tag_bool(const fbits); diff --git a/src/c_backend.ml b/src/c_backend.ml index 65702764..f02cdb9c 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1399,9 +1399,11 @@ let compile_type_def ctx (TD_aux (type_def, _)) = CTD_struct (id, Bindings.bindings ctors), { ctx with records = Bindings.add id ctors ctx.records } - | TD_variant (id, _, _, tus, _) -> + | TD_variant (id, _, typq, tus, _) -> let compile_tu = function - | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id + | Tu_aux (Tu_ty_id (typ, id), _) -> + let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in + ctyp_of_typ ctx typ, id in let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in CTD_variant (id, Bindings.bindings ctus), |