From db3b6d21c18f4ac516c2554db6890274d2b8292c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 10 May 2018 14:23:49 +0100
Subject: Remove buggy bit list comparison functions from Lem library

Found bugs by running CHERI test suite on Isabelle-exported model:  signed
less-than for bit lists was missing negations for the two's complement, and
unsigned less-than compared the reverse lists.

Since all other backends implement this in Sail, it seems best to just remove
this code.

Also add support for infix operators to Lem backend, by z-encoding their
identifiers like the other backends do.
---
 src/gen_lib/sail_operators_mwords.lem | 16 ----------------
 1 file changed, 16 deletions(-)

(limited to 'src/gen_lib/sail_operators_mwords.lem')

diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 077dfb02..22d5b246 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -329,21 +329,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 let inline eq_vec    = eq_mword
 let inline neq_vec   = neq_mword
-let inline ult_vec   = ucmp_mword (<)
-let inline slt_vec   = scmp_mword (<)
-let inline ugt_vec   = ucmp_mword (>)
-let inline sgt_vec   = scmp_mword (>)
-let inline ulteq_vec = ucmp_mword (<=)
-let inline slteq_vec = scmp_mword (<=)
-let inline ugteq_vec = ucmp_mword (>=)
-let inline sgteq_vec = scmp_mword (>=)
-- 
cgit v1.2.3