diff options
| author | Peter Sewell | 2017-01-26 09:31:39 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-01-26 09:31:39 +0000 |
| commit | 9c825884245e1cb5f6ad1fbc66a7d0c9fca24fe9 (patch) | |
| tree | a3a63dc27883648ff9343117860064790a8c4f50 /src/lem_interp/interp_lib.lem | |
| parent | 4f2c4427c0f578ade8a7454220ad600bf190ae81 (diff) | |
| parent | db4d71f55e40747538c4df601fa5f4f6b0e6b0b6 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
Diffstat (limited to 'src/lem_interp/interp_lib.lem')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 3d354774..625dfb6c 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -350,6 +350,9 @@ let eq_vec v = else V_lit (L_aux L_zero Unknown) | (V_unknown, _) -> V_unknown | (_, V_unknown) -> V_unknown + | (V_vector _ _ [c1], _) -> eq (V_tuple [c1; v2]) + | (_, V_vector _ _ [c2]) -> eq (V_tuple [v1; c2]) + | (V_lit _, V_lit _) -> eq (V_tuple [v1;v2]) (*Vectors of one bit return one bit; we need coercion to match*) | _ -> Assert_extra.failwith ("eq_vec not given two vectors, given instead " ^ (string_of_value v)) end in match v with | (V_tuple [v1; v2]) -> binary_taint eq_vec_help v1 v2 @@ -384,6 +387,15 @@ let neq = compose neg eq ;; let neq_vec = compose neg eq_vec +let rec v_abs v = retaint v (match detaint v with + | V_lit (L_aux arg la) -> + V_lit (L_aux (match arg with + | L_num n -> if n < 0 then L_num (n * (0 - 1)) else L_num n + | _ -> Assert_extra.failwith ("abs given unexpected " ^ (string_of_value v)) end) la) + | V_unknown -> V_unknown + | V_tuple [v] -> v_abs v + | _ -> Assert_extra.failwith ("abs given unexpected " ^ (string_of_value v)) end) + let arith_op op v = let fail () = Assert_extra.failwith ("arith_op given unexpected " ^ (string_of_value v)) in let arith_op_help vl vr = @@ -1023,6 +1035,7 @@ let library_functions direction = [ ("most_significant", most_significant); ("min", min); ("max", max); + ("abs", v_abs); ] ;; let eval_external name v = match List.lookup name (library_functions IInc) with |