summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorJon French2018-11-01 10:39:56 +0000
committerJon French2018-11-01 10:39:56 +0000
commitd47313c00011be39ed1c2e411d401bb759ed65bf (patch)
treec4cc764fa2c6d2e14cf9d3558734585133489759 /src/value.ml
parent6305947a929778bb7781056124913c4c2ac23d5c (diff)
Interpreter: last couple of builtins to get RISC-V working
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index 90f6d947..8e920377 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -317,6 +317,14 @@ let value_negate = function
| [v1] -> V_int (Sail_lib.negate (coerce_int v1))
| _ -> failwith "value negate"
+let value_pow2 = function
+ | [v1] -> V_int (Sail_lib.pow2 (coerce_int v1))
+ | _ -> failwith "value pow2"
+
+let value_int_power = function
+ | [v1; v2] -> V_int (Sail_lib.int_power (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value int_power"
+
let value_mult = function
| [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
| _ -> failwith "value mult"
@@ -615,6 +623,8 @@ let primops =
("quotient", value_quotient);
("modulus", value_modulus);
("negate", value_negate);
+ ("pow2", value_pow2);
+ ("int_power", value_int_power);
("shr_int", value_shr_int);
("shl_int", value_shl_int);
("max_int", value_max_int);