diff options
Diffstat (limited to 'backend/SplitLong.vp')
-rw-r--r-- | backend/SplitLong.vp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 5891adef..f7eeebd0 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -38,7 +38,9 @@ Class helper_functions := mk_helper_functions { i64_umod: ident; (**r unsigned remainder *) i64_shl: ident; (**r shift left *) i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident (**r shift right signed *) + i64_sar: ident; (**r shift right signed *) + i64_umulh: ident; (**r unsigned multiply high *) + i64_smulh: ident; (**r signed multiply high *) }. Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. @@ -255,6 +257,11 @@ Definition mull (e1 e2: expr) := | _, _ => mull_base e1 e2 end. +Definition mullhu (e1: expr) (n2: int64) := + Eexternal i64_umulh sig_ll_l (e1 ::: longconst n2 ::: Enil). +Definition mullhs (e1: expr) (n2: int64) := + Eexternal i64_smulh sig_ll_l (e1 ::: longconst n2 ::: Enil). + Definition shrxlimm (e: expr) (n: int) := if Int.eq n Int.zero then e else Elet e (shrlimm (addl (Eletvar O) |