ISLE: built-in integer types (#9610)

Copyright (c) 2024, Arm Limited.

Signed-off-by: Karl Meakin <karl.meakin@arm.com>

cranelift/codegen/src/prelude.isle

@@ -16,34 +16,15 @@
 (model bool (type Bool))
 
 (model u8 (type (bv 8)))
-(type u8 (primitive u8))
-
 (model u16 (type (bv 16)))
-(type u16 (primitive u16))
-
 (model u32 (type (bv 32)))
-(type u32 (primitive u32))
-
 (model u64 (type (bv 64)))
-(type u64 (primitive u64))
-(type u128 (primitive u128))
-
 (model usize (type (bv)))
-(type usize (primitive usize))
 
 (model i8 (type (bv 8)))
-(type i8 (primitive i8))
-
 (model i16 (type (bv 16)))
-(type i16 (primitive i16))
-
 (model i32 (type (bv 32)))
-(type i32 (primitive i32))
-
 (model i64 (type (bv 64)))
-(type i64 (primitive i64))
-(type i128 (primitive i128))
-(type isize (primitive isize))
 
 ;; `cranelift-entity`-based identifiers.
 (model Type (type Int))

cranelift/isle/isle/isle_examples/fail/bound_var_type_mismatch.isle

@@ -1,6 +1,3 @@
-(type u32 (primitive u32))
-(type u64 (primitive u64))
-
 (decl A (u32 u64) u32)
 
 (rule 1 (A x x) x)

cranelift/isle/isle/isle_examples/fail/error1.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A (enum (A1 (x u32))))
 
 (decl Ext1 (u32) A)

cranelift/isle/isle/isle_examples/fail/extra_parens.isle

@@ -1,5 +1,3 @@
-(type u32 (primitive u32))
-
 (decl f (u32) u32)
 ;; Should get an error about `x` not being a term, with a suggestion that it is
 ;; a bound var instead.

cranelift/isle/isle/isle_examples/fail/impure_expression.isle

@@ -1,5 +1,3 @@
-(type u32 (primitive u32))
-
 (decl ctor (u32) u32)
 (rule (ctor x) x)
 

cranelift/isle/isle/isle_examples/fail/impure_rhs.isle

@@ -1,5 +1,3 @@
-(type u32 (primitive u32))
-
 (decl pure ctor (u32) u32)
 (decl impure (u32) u32)
 

cranelift/isle/isle/isle_examples/fail/multi_internal_etor.isle

@@ -1,4 +1,2 @@
-(type u32 (primitive u32))
-
 (decl multi A (u32) u32)
 (extractor (A x) x)

cranelift/isle/isle/isle_examples/fail/multi_prio.isle

@@ -1,4 +1,2 @@
-(type u32 (primitive u32))
-
 (decl multi A (u32) u32)
 (rule 0 (A x) x)

cranelift/isle/isle/isle_examples/link/borrows.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A extern (enum (B (x u32) (y u32))))
 
 (decl get_a (A) u32)

cranelift/isle/isle/isle_examples/link/iflets.isle

@@ -1,5 +1,3 @@
-(type u32 (primitive u32))
-
 (decl pure partial A (u32 u32) u32)
 (extern constructor A A)
 

cranelift/isle/isle/isle_examples/link/multi_constructor.isle

@@ -1,5 +1,3 @@
-(type u32 (primitive u32))
-
 (decl multi A (u32) u32)
 (decl multi B (u32) u32)
 (decl multi C (u32) u32)

cranelift/isle/isle/isle_examples/link/multi_extractor.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A extern (enum (B) (C)))
 
 (decl multi E1 (A u32) u32)

cranelift/isle/isle/isle_examples/link/test.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A (enum (A1 (x u32)) (A2 (x u32))))
 (type B (enum (B1 (x u32)) (B2 (x u32))))
 

cranelift/isle/isle/isle_examples/pass/bound_var.isle

@@ -1,5 +1,3 @@
-(type u32 (primitive u32))
-
 (decl A (u32 u32) u32)
 
 (rule 1 (A x x) x)

cranelift/isle/isle/isle_examples/pass/construct_and_extract.isle

@@ -1,5 +1,3 @@
-(type i32 (primitive i32))
-
 (type B (enum (B (x i32) (y i32))))
 
 ;; `isub` has a constructor and extractor.

cranelift/isle/isle/isle_examples/pass/conversions.isle

@@ -1,7 +1,6 @@
 (type T (enum (A) (B)))
 (type U (enum (C) (D)))
 (type V (enum (E) (F)))
-(type u32 (primitive u32))
 
 (convert T U t_to_u)
 (convert U T u_to_t)

cranelift/isle/isle/isle_examples/pass/let.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A (enum (Add (x u32) (y u32)) (Sub (x u32) (y u32))))
 (type B (enum (B (z u32))))
 

cranelift/isle/isle/isle_examples/pass/prio_trie_bug.isle

@@ -5,8 +5,6 @@
 ;; priority 1 below.
 
 (type Unit (primitive Unit))
-(type u8 (primitive u8))
-(type u32 (primitive u32))
 (type Reg (primitive Reg))
 (type MemFlags (primitive MemFlags))
 (type MachLabel (primitive MachLabel))

cranelift/isle/isle/isle_examples/pass/test2.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A (enum
   (A1 (x B) (y B))))
 (type B (enum

cranelift/isle/isle/isle_examples/pass/test3.isle

@@ -7,7 +7,6 @@
 (type Inst (primitive Inst))
 (type InstInput (primitive InstInput))
 (type Reg (primitive Reg))
-(type u32 (primitive u32))
 
 (decl Op (Opcode) Inst)
 (extern extractor infallible Op get_opcode)

cranelift/isle/isle/isle_examples/pass/test4.isle

@@ -1,4 +1,3 @@
-(type u32 (primitive u32))
 (type A (enum (A1 (x u32))))
 
 (decl Ext1 (u32) A)

cranelift/isle/isle/isle_examples/pass/tutorial.isle

@@ -1,8 +1,5 @@
 ;;;; Type Definitions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; Declare that we are using the `i32` primitive type from Rust.
-(type i32 (primitive i32))
-
 ;; Our high-level, RISC-y input IR.
 (type HighLevelInst
   (enum (Add (a Value) (b Value))

cranelift/isle/isle/isle_examples/pass/veri_spec.isle

@@ -1,5 +1,3 @@
-(type u8 (primitive u8))
-
 (form
   bv_unary_8_to_64
   ((args (bv  8)) (ret (bv  8)) (canon (bv  8)))

cranelift/isle/isle/isle_examples/run/iconst.isle

@@ -1,13 +1,9 @@
-(type i64 (primitive i64))
-
 (decl partial X (i64) i64)
 (rule (X -1) -2)
 (rule (X -2) -3)
 (rule (X 0x7fff_ffff_ffff_ffff) -0x8000_0000_0000_0000)
 (rule (X -16) 1)
 
-(type i128 (primitive i128))
-
 (decl partial Y (i128) i128)
 
 (rule (Y 0x1000_0000_0000_0000_1234_5678_9abc_def0) -1)
@@ -17,7 +13,6 @@
 (rule (Y -0xffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff) -3)
 
 ;; Test some various syntaxes for numbers
-(type i32 (primitive i32))
 (decl partial Z (i32) i32)
 (rule (Z 0) 0x01)
 (rule (Z 0x01) 0x0_2)

cranelift/isle/isle/isle_examples/run/let_shadowing.isle

@@ -1,6 +1,3 @@
-
-(type u64 (primitive u64))
-
 (decl foo (u64) u64)
 (rule (foo x) x)
 

cranelift/isle/isle/src/codegen.rs

@@ -1,7 +1,9 @@
 //! Generate Rust code from a series of Sequences.
 
 use crate::files::Files;
-use crate::sema::{ExternalSig, ReturnKind, Term, TermEnv, TermId, Type, TypeEnv, TypeId};
+use crate::sema::{
+    BuiltinType, ExternalSig, ReturnKind, Term, TermEnv, TermId, Type, TypeEnv, TypeId,
+};
 use crate::serialize::{Block, ControlFlow, EvalStep, MatchArm};
 use crate::stablemapset::StableSet;
 use crate::trie_again::{Binding, BindingId, Constraint, RuleSet};
@@ -915,18 +917,11 @@ impl<L: Length, C> Length for ContextIterWrapper<L, C> {{
         val: i128,
         ty: TypeId,
     ) -> Result<(), std::fmt::Error> {
-        // For the kinds of situations where we use ISLE, magic numbers are
-        // much more likely to be understandable if they're in hex rather than
-        // decimal.
-        // TODO: use better type info (https://github.com/bytecodealliance/wasmtime/issues/5431)
-        if val < 0
-            && self.typeenv.types[ty.index()]
-                .name(self.typeenv)
-                .starts_with('i')
-        {
-            write!(ctx.out, "-{:#X}", -val)
-        } else {
-            write!(ctx.out, "{val:#X}")
+        let ty_data = &self.typeenv.types[ty.index()];
+        match ty_data {
+            Type::Builtin(BuiltinType::Int(ty)) if ty.is_signed() => write!(ctx.out, "{val}_{ty}"),
+            Type::Builtin(BuiltinType::Int(ty)) => write!(ctx.out, "{val:#x}_{ty}"),
+            _ => write!(ctx.out, "{val:#x}"),
         }
     }
 }