diff options
| author | Shaked Flur | 2018-02-08 12:06:00 +0000 |
|---|---|---|
| committer | Shaked Flur | 2018-02-08 12:06:00 +0000 |
| commit | 043ea8ec3faecadf34ef9010bdd539f595f9c6da (patch) | |
| tree | eb44af3b9dec8e1a222872f56d4e32781596fa9e /src/gen_lib | |
| parent | 151d86b911c9a266465638ee3514156dfb178e92 (diff) | |
replaced NIA_LR/CTR/register with NIA_indirect;
removed IK_cond_branch, and added IK_branch
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/deep_shallow_convert.lem | 4 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 8 |
2 files changed, 4 insertions, 8 deletions
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 76880dbd..7fea0409 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -532,7 +532,7 @@ let instruction_kindToInterpValue = function | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) - | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) + | IK_branch -> V_ctor (Id_aux (Id "IK_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) end @@ -541,7 +541,7 @@ let rec instruction_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v) - | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch + | V_ctor (Id_aux (Id "IK_branch") _) _ _ v -> IK_branch | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v) | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple | V_tuple [v] -> instruction_kindFromInterpValue v diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 121f6cc8..ffccaa7e 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -912,9 +912,7 @@ type regfp = type niafp = | NIAFP_successor | NIAFP_concrete_address of vector bitU - | NIAFP_LR - | NIAFP_CTR - | NIAFP_register of regfp + | NIAFP_indirect_address (* only for MIPS *) type diafp = @@ -946,9 +944,7 @@ end let niafp_to_nia reginfo = function | NIAFP_successor -> NIA_successor | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) - | NIAFP_LR -> NIA_LR - | NIAFP_CTR -> NIA_CTR - | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) + | NIAFP_indirect_address -> NIA_indirect_address end let diafp_to_dia reginfo = function |