diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/Interp_interface.lem | 8 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 7 |
2 files changed, 10 insertions, 5 deletions
diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem index 136078aa..0e05fafe 100644 --- a/src/lem_interp/Interp_interface.lem +++ b/src/lem_interp/Interp_interface.lem @@ -14,11 +14,13 @@ type value = type instruction_state = Interp.stack type context = Interp.top_level +type slice = (integer * integer) + type reg_name = | Reg of string (*Name of the register, accessing the entire register*) -| Reg_slice of string * integer * integer (*Name of the register, accessing from the first to second integer*) -| Reg_field of string * string * integer * integer (*Name of the register, name of the field of the register accessed, the index range of the field*) -| Reg_f_slice of string * string * integer * integer * integer * integer (* Same as above but only accessing from the third to the fourth integer of the field *) +| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*) +| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*) +| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *) type outcome = | Read_mem of read_kind * value * (value -> instruction_state) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 8b7fdec3..98fbb8a3 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -2,14 +2,17 @@ import Interp import Interp_lib open import Interp_interface +import Num + val intern_value : value -> Interp.value val extern_value : Interp.value -> value let build_context defs = Interp.to_top_env defs let intern_value v = match v with - | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) - | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs) + | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | false -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) + | true -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs) + | Bytevector bys -> Interp.V_vector 0 true (List.map | Unknown -> Interp.V_unknown end |