diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index edc7ebfd..1aed6521 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -430,7 +430,7 @@ let rec compare_op op (V_tuple args) = match args with then V_lit(L_aux L_one lx) else V_lit(L_aux L_zero lx) end ;; -let rec compare_op_vec op (V_tuple args) = match args with +let rec compare_op_vec op sign (V_tuple args) = match args with | [V_track v1 r1;V_track v2 r2] -> taint (compare_op_vec op (V_tuple [v1;v2])) (r1++r2) | [V_track v1 r1;v2] -> @@ -440,7 +440,7 @@ let rec compare_op_vec op (V_tuple args) = match args with | [V_unknown;_] -> V_unknown | [_;V_unknown] -> V_unknown | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] -> - let (l1',l2') = (to_num Signed l1, to_num Signed l2) in + let (l1',l2') = (to_num sign l1, to_num sign l2) in compare_op op (V_tuple[l1';l2']) end ;; let rec compare_op_vec_unsigned op (V_tuple args) = match args with @@ -559,10 +559,14 @@ let function_map = [ ("gt", compare_op (>)); ("lteq", compare_op (<=)); ("gteq", compare_op (>=)); - ("lt_vec", compare_op_vec (<)); - ("gt_vec", compare_op_vec (>)); - ("lteq_vec", compare_op_vec (<=)); - ("gteq_vec", compare_op_vec (>=)); + ("lt_vec", compare_op_vec Unsigned (<)); + ("gt_vec", compare_op_vec Unsigned (>)); + ("lteq_vec", compare_op_vec Unsigned (<=)); + ("gteq_vec", compare_op_vec Unsigned (>=)); + ("lt_vec_signed", compare_op_vec Signed (<)); + ("gt_vec_signed", compare_op_vec Signed (>)); + ("lteq_vec_signed", compare_op_vec Signed (<=)); + ("gteq_vec_signed", compare_op_vec Signed (>=)); ("ltu", compare_op_vec_unsigned (<)); ("gtu", compare_op_vec_unsigned (>)); ("duplicate", duplicate); |