Add fcmp and icmp to the generator.

vellvm · Mar 25, 2024 · 7e3336f · 7e3336f
1 parent 5ad0473
commit 7e3336f
Showing 1 changed file with 44 additions and 6 deletions.
diff --git a/src/coq/QC/GenAST.v b/src/coq/QC/GenAST.v
@@ -1575,6 +1575,13 @@ Section TypGenerators.
         ; TYPE_I 64
       ].
 
+  (* TODO: look up identifiers *)
+  Definition gen_float_typ : GenLLVM typ :=
+    elems_LLVM
+      [ TYPE_Float
+        (* ; TYPE_Double *)
+      ].
+
   (* TODO: IPTR not implemented *)
   Definition gen_int_typ_for_ptr_cast : GenLLVM typ :=
     ret (TYPE_I 64).
@@ -2078,10 +2085,17 @@ Section ExpGenerators.
         let gens :=
           match t with
           | TYPE_I isz =>
-              (* TODO: If I1 also allow ICmp and FCmp *)
-              [gen_ibinop_exp gen_global_of_typ gen_ident_of_typ isz]
+              if N.eqb isz 1%N
+              then
+                [ gen_ibinop_exp gen_global_of_typ gen_ident_of_typ isz
+                  ; τ <- gen_int_typ;;
+                    gen_icmp_exp_typ gen_global_of_typ gen_ident_of_typ τ
+                  ; τ <- gen_float_typ;;
+                    gen_fcmp_exp_typ gen_global_of_typ gen_ident_of_typ τ
+                ]
+              else
+                [ gen_ibinop_exp gen_global_of_typ gen_ident_of_typ isz ]
           | TYPE_IPTR =>
-              (* TODO: If I1 also allow ICmp and FCmp *)
               [gen_ibinop_exp_typ gen_global_of_typ gen_ident_of_typ TYPE_IPTR]
           | TYPE_Pointer t         => [] (* GEP? *)
 
@@ -2160,7 +2174,23 @@ Section ExpGenerators.
                     then ret (OP_FBinop fbinop nil) <*> ret ty <*> gen_exp_size' gen_global_of_typ gen_ident_of_typ 0%nat ty <*> gen_exp_size' gen_global_of_typ gen_ident_of_typ 0%nat ty
                     else ret (OP_FBinop fbinop nil) <*> ret ty <*> gen_exp_size' gen_global_of_typ gen_ident_of_typ 0%nat ty <*> gen_exp_size' gen_global_of_typ gen_ident_of_typ 0%nat ty
     | _ => failGen "gen_fbinop_exp"
-    end.
+    end
+  with
+  gen_icmp_exp_typ (gen_global_of_typ : typ -> GenLLVM (option ident)) (gen_ident_of_typ : typ -> GenLLVM (option ident)) (t : typ) {struct t} : GenLLVM (exp typ)
+  := cmp <- lift gen_icmp;;
+     ret (OP_ICmp cmp) <*> ret t <*> gen_exp_size' gen_global_of_typ gen_ident_of_typ 0%nat t <*> gen_non_zero_exp_size 0%nat t
+  with
+  gen_fcmp_exp_typ (gen_global_of_typ : typ -> GenLLVM (option ident)) (gen_ident_of_typ : typ -> GenLLVM (option ident)) (t : typ) {struct t} : GenLLVM (exp typ)
+  := cmp <- lift gen_fcmp;;
+     ret (OP_FCmp cmp) <*> ret t <*> gen_exp_size' gen_global_of_typ gen_ident_of_typ 0%nat t <*> gen_non_zero_exp_size 0%nat t.
+
+  Definition gen_icmp_exp (gen_global_of_typ : typ -> GenLLVM (option ident)) (gen_ident_of_typ : typ -> GenLLVM (option ident)) : GenLLVM (exp typ)
+    := τ <- gen_int_typ;;
+       gen_icmp_exp_typ gen_global_of_typ gen_ident_of_typ τ.
+
+  Definition gen_fcmp_exp (gen_global_of_typ : typ -> GenLLVM (option ident)) (gen_ident_of_typ : typ -> GenLLVM (option ident)) : GenLLVM (exp typ)
+    := τ <- gen_float_typ;;
+       gen_fcmp_exp_typ gen_global_of_typ gen_ident_of_typ τ.
 
   Definition gen_deterministic_global_ident :=
     gen_var_of_typ_ident (gen_context' .@ is_global') (withl is_deterministic').
@@ -2192,8 +2222,16 @@ Section ExpGenerators.
          (fun sz =>
             match t with
             | TYPE_I isz =>
-                (* TODO: If I1 also allow ICmp and FCmp *)
-                gen_ibinop_exp gen_deterministic_global_ident gen_deterministic_ident isz
+                if N.eqb isz 1%N
+                then
+                  (* If I1 also allow ICmp and FCmp *)
+                  oneOf_LLVM
+                    [ gen_ibinop_exp gen_deterministic_global_ident gen_deterministic_ident isz
+                      ; gen_icmp_exp gen_deterministic_global_ident gen_deterministic_ident
+                      ; gen_fcmp_exp gen_deterministic_global_ident gen_deterministic_ident
+                    ]
+                else
+                  gen_ibinop_exp gen_deterministic_global_ident gen_deterministic_ident isz
             | TYPE_Float => gen_fbinop_exp gen_deterministic_global_ident gen_deterministic_ident TYPE_Float
             | TYPE_Double => gen_fbinop_exp gen_deterministic_global_ident gen_deterministic_ident TYPE_Double
             | _ => failGen "gen_op"