Add support for float literals

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.38"
+let supported_charon_version = "0.1.39"

charon-ml/src/GAstOfJson.ml

@@ -330,9 +330,9 @@ and literal_type_of_json (js : json) : (literal_type, string) result =
     | `Assoc [ ("Integer", integer) ] ->
         let* integer = integer_type_of_json integer in
         Ok (TInteger integer)
-    | `Assoc [ ("Float", float) ] ->
-        let* float = float_type_of_json float in
-        Ok (TFloat float)
+    | `Assoc [ ("Float", float_) ] ->
+        let* float_ = float_type_of_json float_ in
+        Ok (TFloat float_)
     | `String "Bool" -> Ok TBool
     | `String "Char" -> Ok TChar
     | _ -> Error "")
@@ -912,6 +912,9 @@ and literal_of_json (js : json) : (literal, string) result =
     | `Assoc [ ("Scalar", scalar) ] ->
         let* scalar = scalar_value_of_json scalar in
         Ok (VScalar scalar)
+    | `Assoc [ ("Float", float_) ] ->
+        let* float_ = float_value_of_json float_ in
+        Ok (VFloat float_)
     | `Assoc [ ("Bool", bool_) ] ->
         let* bool_ = bool_of_json bool_ in
         Ok (VBool bool_)
@@ -926,6 +929,15 @@ and literal_of_json (js : json) : (literal, string) result =
         Ok (VStr str)
     | _ -> Error "")
 
+and float_value_of_json (js : json) : (float_value, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("value", value); ("ty", ty) ] ->
+        let* float_value = string_of_json value in
+        let* float_ty = float_type_of_json ty in
+        Ok ({ float_value; float_ty } : float_value)
+    | _ -> Error "")
+
 and assumed_fun_id_of_json (js : json) : (assumed_fun_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with

charon-ml/src/NameMatcher.ml

@@ -792,8 +792,9 @@ let literal_to_pattern (_c : to_pat_config) (lit : Values.literal) : literal =
   | VScalar sv -> LInt sv.value
   | VBool v -> LBool v
   | VChar v -> LChar v
-  | VStr _ | VByteStr _ ->
-      raise (Failure "String and byte string literals are not valid in names")
+  | VFloat _ | VStr _ | VByteStr _ ->
+      raise
+        (Failure "Float, string and byte string literals are not valid in names")
 
 let rec name_with_generic_args_to_pattern_aux (ctx : ctx) (c : to_pat_config)
     (n : T.name) (generics : generic_args option) : pattern =

charon-ml/src/PrintValues.ml

@@ -35,9 +35,13 @@ let big_int_to_string (bi : big_int) : string = Z.to_string bi
 let scalar_value_to_string (sv : scalar_value) : string =
   big_int_to_string sv.value ^ ": " ^ integer_type_to_string sv.int_ty
 
+let float_value_to_string (fv : float_value) : string =
+  fv.float_value ^ ": " ^ float_type_to_string fv.float_ty
+
 let literal_to_string (lit : literal) : string =
   match lit with
   | VScalar sv -> scalar_value_to_string sv
+  | VFloat fv -> float_value_to_string fv
   | VBool b -> Bool.to_string b
   | VChar c -> String.make 1 c
   | VStr s -> "\"" ^ s ^ "\""

charon-ml/src/Values.ml

@@ -80,13 +80,16 @@ and literal_type =
  *)
 and scalar_value = { value : big_int; int_ty : integer_type }
 
+and float_value = { float_value : string; float_ty : float_type }
+
 (** A literal value.
 
     Can be used by operands (in which case it represents a constant) or by
     the interpreter to represent a concrete, literal value.
  *)
 and literal =
   | VScalar of scalar_value
+  | VFloat of float_value
   | VBool of bool
   | VChar of char
   | VStr of string

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.38"
+version = "0.1.39"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 license = "Apache-2.0"
@@ -60,6 +60,7 @@ nom-supreme = "0.8.0"
 petgraph = "0.6.2"
 pretty = "0.12"
 regex = "1.7.1"
+rustc_apfloat = "0.2.1"
 rustc_version = "0.4"
 serde_json = { version = "1.0.91", features = ["unbounded_depth"] }
 serde-map-to-array = { version = "1.1.1", features = ["std"] }
@@ -74,8 +75,8 @@ tracing-tree = { git = "https://github.com/Nadrieril/tracing-tree", features = [
 tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_warn" ] }
 which = "6.0.1"
 
-# hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
-hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "charon", optional = true }
+hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "afromher_float", optional = true }
+# hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "charon", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

charon/src/ast/values.rs

@@ -1,5 +1,6 @@
 //! Contains definitions for variables and constant values.
 
+use crate::ast::FloatTy;
 use core::hash::Hash;
 use derive_visitor::{Drive, DriveMut};
 use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
@@ -35,6 +36,7 @@ generate_index_type!(VarId, "");
 #[charon::variants_prefix("V")]
 pub enum Literal {
     Scalar(ScalarValue),
+    Float(FloatValue),
     Bool(bool),
     Char(char),
     ByteStr(Vec<u8>),
@@ -81,3 +83,16 @@ pub enum ScalarValue {
     U64(u64),
     U128(u128),
 }
+
+/// This is simlar to the Scalar value above. However, instead of storing
+/// the float value itself, we store its String representation. This allows
+/// to derive the Eq and Ord traits, which are not implemented for floats
+#[derive(
+    Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Hash, PartialOrd, Ord, Drive, DriveMut,
+)]
+pub struct FloatValue {
+    #[charon::rename("float_value")]
+    pub value: String,
+    #[charon::rename("float_ty")]
+    pub ty: FloatTy,
+}

charon/src/bin/charon-driver/translate/translate_constants.rs

@@ -43,6 +43,28 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 };
                 Literal::Scalar(scalar)
             }
+            hax::ConstantLiteral::Float(bits, float_type) => {
+                use rustc_apfloat::Float;
+                let value = match float_type {
+                    hax::FloatTy::F16 => FloatValue {
+                        value: rustc_apfloat::ieee::Half::from_bits(*bits).to_string(),
+                        ty: FloatTy::F16,
+                    },
+                    hax::FloatTy::F32 => FloatValue {
+                        value: rustc_apfloat::ieee::Single::from_bits(*bits).to_string(),
+                        ty: FloatTy::F32,
+                    },
+                    hax::FloatTy::F64 => FloatValue {
+                        value: rustc_apfloat::ieee::Double::from_bits(*bits).to_string(),
+                        ty: FloatTy::F64,
+                    },
+                    hax::FloatTy::F128 => FloatValue {
+                        value: rustc_apfloat::ieee::Quad::from_bits(*bits).to_string(),
+                        ty: FloatTy::F128,
+                    },
+                };
+                Literal::Float(value)
+            }
         };
         Ok(RawConstantExpr::Literal(lit))
     }

charon/src/bin/generate-ml/main.rs

@@ -40,7 +40,17 @@ fn make_ocaml_ident(name: &str) -> String {
     let mut name = name.to_case(Case::Snake);
     if matches!(
         &*name,
-        "virtual" | "bool" | "char" | "struct" | "type" | "let" | "fun" | "open" | "rec" | "assert"
+        "virtual"
+            | "bool"
+            | "char"
+            | "struct"
+            | "type"
+            | "let"
+            | "fun"
+            | "open"
+            | "rec"
+            | "assert"
+            | "float"
     ) {
         name += "_";
     }
@@ -846,6 +856,7 @@ fn main() -> Result<()> {
                     "UnOp",
                     "BinOp",
                     "Literal",
+                    "FloatValue",
                     "BuiltinFunId",
                     "BuiltinIndexOp",
                     "FunId",

charon/src/pretty/fmt_with_ctx.rs

@@ -1589,6 +1589,7 @@ impl std::fmt::Display for Literal {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
         match self {
             Literal::Scalar(v) => write!(f, "{v}"),
+            Literal::Float(v) => write!(f, "{v}"),
             Literal::Bool(v) => write!(f, "{v}"),
             Literal::Char(v) => write!(f, "{v}"),
             Literal::Str(v) => write!(f, "\"{v}\""),
@@ -1672,6 +1673,18 @@ impl std::fmt::Display for ScalarValue {
     }
 }
 
+impl std::fmt::Display for FloatValue {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
+        let v = &self.value;
+        match self.ty {
+            FloatTy::F16 => write!(f, "{v} : f16"),
+            FloatTy::F32 => write!(f, "{v} : f32"),
+            FloatTy::F64 => write!(f, "{v} : f64"),
+            FloatTy::F128 => write!(f, "{v} : f128"),
+        }
+    }
+}
+
 impl std::fmt::Display for TraitItemName {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
         write!(f, "{}", self.0)

charon/tests/ui/float.out

@@ -25,5 +25,27 @@ fn test_crate::sum_float(@1: f64, @2: f64) -> f64
     return
 }
 
+fn test_crate::literal_float() -> f64
+{
+    let @0: f64; // return
+    let x@1: f64; // local
+    let y@2: f64; // local
+    let @3: f64; // anonymous local
+    let @4: f64; // anonymous local
+
+    x@1 := const (1 : f64)
+    @fake_read(x@1)
+    y@2 := const (1.5 : f64)
+    @fake_read(y@2)
+    @3 := copy (x@1)
+    @4 := copy (y@2)
+    @0 := move (@3) + move (@4)
+    drop @4
+    drop @3
+    drop y@2
+    drop x@1
+    return
+}
+
 
 

charon/tests/ui/float.rs

@@ -4,4 +4,10 @@ fn test_float(x : f64) -> f64 {
 
 fn sum_float(x : f64, y : f64) -> f64 {
     x + y
-}
+}
+
+fn literal_float () -> f64 {
+    let x = 1.0f64;
+    let y = 1.5f64;
+    x + y
+}