[CN] Fix #380 (Have ptr_eq typechecks its arguments)

backend/cn/lib/builtins.ml

@@ -5,14 +5,13 @@ open Effectful.Make (Resultat)
 
 open TypeErrors
 open IndexTerms
+module CF = Cerb_frontend
 
-(* builtin function symbols *)
-let mk_arg0 mk args loc =
-  match args with
-  | [] -> return (mk loc)
-  | _ :: _ as xs ->
-    fail { loc; msg = Number_arguments { has = List.length xs; expect = 0 } }
+type builtin_fn_def = string * Sym.t * LogicalFunctions.definition
 
+let loc = Cerb_location.other "<builtin>"
+
+(* builtin function symbols *)
 
 let mk_arg1 mk args loc =
   match args with
@@ -36,10 +35,28 @@ let mk_arg3_err mk args loc =
 
 let mk_arg3 mk = mk_arg3_err (fun tup loc -> return (mk tup loc))
 
-let mk_arg5 mk args loc =
-  match args with
-  | [ a; b; c; d; e ] -> return (mk (a, b, c, d, e) loc)
-  | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 5 } }
+let var_binop op ty ~left:(sym1, bt1) ~right:(sym2, bt2) =
+  binop op (sym_ (sym1, bt1, loc), sym_ (sym2, bt2, loc)) loc ty
+
+
+let definition name args body =
+  ( name,
+    Sym.fresh_named name,
+    LogicalFunctions.
+      { loc; emit_coq = false; args; definition = Def body; return_bt = bt body } )
+
+
+let mk_builtin_arg0 name = definition name []
+
+let mk_builtin_arg1 name bt mk : builtin_fn_def =
+  let arg = (Sym.fresh_named "arg", bt) in
+  mk arg |> definition name [ arg ]
+
+
+let mk_builtin_arg2 name (bt1, bt2) mk : builtin_fn_def =
+  let left = (Sym.fresh_named "arg1", bt1) in
+  let right = (Sym.fresh_named "arg2", bt2) in
+  mk ~left ~right |> definition name [ left; right ]
 
 
 let min_bits_def (sign, n) =
@@ -49,9 +66,7 @@ let min_bits_def (sign, n) =
     | Signed -> (Z.(neg @@ shift_left one (Int.sub n 1)), "i")
   in
   let name = "MIN" ^ letter ^ Int.to_string n in
-  ( name,
-    Sym.fresh_named name,
-    mk_arg0 (fun loc -> IT.sterm_of_term @@ num_lit_ num (BT.Bits (sign, n)) loc) )
+  num_lit_ num (BT.Bits (sign, n)) loc |> mk_builtin_arg0 name
 
 
 let max_bits_def (sign, n) =
@@ -61,11 +76,65 @@ let max_bits_def (sign, n) =
     | Signed -> (Z.(shift_left one (Int.sub n 1) - one), "i")
   in
   let name = "MAX" ^ letter ^ Int.to_string n in
-  ( name,
-    Sym.fresh_named name,
-    mk_arg0 (fun loc -> IT.sterm_of_term @@ num_lit_ num (BT.Bits (sign, n)) loc) )
+  num_lit_ num (BT.Bits (sign, n)) loc |> mk_builtin_arg0 name
+
+
+let max_min_bits =
+  let sizes = [ 8; 16; 32; 64 ] in
+  let signs = [ BT.Unsigned; Signed ] in
+  List.fold_left
+    (fun acc sign ->
+      List.fold_left
+        (fun acc size -> max_bits_def (sign, size) :: min_bits_def (sign, size) :: acc)
+        acc
+        sizes)
+    []
+    signs
+
+
+let not_def =
+  mk_builtin_arg1 "not" BT.Bool (fun (sym, bt) -> not_ (sym_ (sym, bt, loc)) loc)
+
+
+let is_null_def : builtin_fn_def =
+  mk_builtin_arg1 "is_null" BT.Loc (fun (sym, bt) ->
+    (eq__ (sym_ (sym, bt, loc)) (null_ loc)) loc)
+
+
+(* Cannot translate this to a logical function until the TODO in `cn_to_ail_expr_aux_internal` in `cn_internal_to_ail.ml` is resolved*)
+let has_alloc_id_def =
+  ( "has_alloc_id",
+    Sym.fresh_named "has_alloc_id",
+    mk_arg1 (fun p loc' -> IT.sterm_of_term @@ IT.hasAllocId_ (IT.term_of_sterm p) loc')
+  )
+
+
+let ptr_eq_def : builtin_fn_def =
+  var_binop EQ BT.Bool |> mk_builtin_arg2 "ptr_eq" (BT.Loc, BT.Loc)
 
 
+let prov_eq_def : builtin_fn_def =
+  let left = (Sym.fresh_named "arg1", BT.Loc) in
+  let right = (Sym.fresh_named "arg2", BT.Loc) in
+  let left_cast = allocId_ (sym_ (fst left, BT.Loc, loc)) loc in
+  let right_cast = allocId_ (sym_ (fst right, BT.Loc, loc)) loc in
+  let body = binop EQ (left_cast, right_cast) loc BT.Bool in
+  definition "prov_eq" [ left; right ] body
+
+
+let addr_eq_def : builtin_fn_def =
+  let left = (Sym.fresh_named "arg1", BT.Loc) in
+  let right = (Sym.fresh_named "arg2", BT.Loc) in
+  let left_cast = addr_ (sym_ (fst left, BT.Loc, loc)) loc in
+  let right_cast = addr_ (sym_ (fst right, BT.Loc, loc)) loc in
+  let body = binop EQ (left_cast, right_cast) loc BT.Bool in
+  definition "addr_eq" [ left; right ] body
+
+
+(* The remaining functions in this file, from here until array_to_list_def cannot yet be translated to
+   LogicalFunction.definition types because they implicitly require basetype polymorphism.
+   For example, the `mod` function allows inputs of any sign and size, but such a function cannot be defined
+   yet with an index term *)
 let mul_uf_def = ("mul_uf", Sym.fresh_named "mul_uf", mk_arg2 mul_no_smt_)
 
 let div_uf_def = ("div_uf", Sym.fresh_named "div_uf", mk_arg2 div_no_smt_)
@@ -114,8 +183,6 @@ let rem_def = ("rem", Sym.fresh_named "rem", mk_arg2 rem_)
 
 let mod_def = ("mod", Sym.fresh_named "mod", mk_arg2 mod_)
 
-let not_def = ("not", Sym.fresh_named "not", mk_arg1 not_)
-
 let nth_list_def = ("nth_list", Sym.fresh_named "nth_list", mk_arg3 nthList_)
 
 let array_to_list_def =
@@ -134,87 +201,32 @@ let array_to_list_def =
       | Some (_, bt) -> return (array_to_list_ (arr, i, len) bt loc)) )
 
 
-let is_null_def =
-  ( "is_null",
-    Sym.fresh_named "is_null",
-    mk_arg1 (fun p loc' ->
-      IT.sterm_of_term IT.(eq_ (IT.term_of_sterm p, null_ loc') loc')) )
-
-
-let has_alloc_id_def =
-  ( "has_alloc_id",
-    Sym.fresh_named "has_alloc_id",
-    mk_arg1 (fun p loc' -> IT.sterm_of_term @@ IT.hasAllocId_ (IT.term_of_sterm p) loc')
-  )
-
-
-let ptr_eq_def =
-  ( "ptr_eq",
-    Sym.fresh_named "ptr_eq",
-    mk_arg2 (fun (p1, p2) loc' ->
-      IT.(sterm_of_term @@ eq_ (term_of_sterm p1, term_of_sterm p2) loc')) )
-
-
-let prov_eq_def =
-  ( "prov_eq",
-    Sym.fresh_named "prov_eq",
-    mk_arg2 (fun (p1, p2) loc' ->
-      IT.(
-        sterm_of_term
-        @@ eq_ (allocId_ (term_of_sterm p1) loc', allocId_ (term_of_sterm p2) loc') loc'))
-  )
-
-
-let addr_eq_def =
-  ( "addr_eq",
-    Sym.fresh_named "addr_eq",
-    mk_arg2 (fun (p1, p2) loc' ->
-      IT.(
-        sterm_of_term
-        @@ eq_ (addr_ (term_of_sterm p1) loc', addr_ (term_of_sterm p2) loc') loc')) )
-
-
-let max_min_bits =
-  let sizes = [ 8; 16; 32; 64 ] in
-  let signs = [ BT.Unsigned; Signed ] in
-  List.fold_left
-    (fun acc sign ->
-      List.fold_left
-        (fun acc size -> max_bits_def (sign, size) :: min_bits_def (sign, size) :: acc)
-        acc
-        sizes)
-    []
-    signs
-
-
 let builtin_funs =
-  max_min_bits
-  @ [ mul_uf_def;
-      div_uf_def;
-      power_uf_def;
-      rem_uf_def;
-      mod_uf_def;
-      xor_uf_def;
-      bw_and_uf_def;
-      bw_or_uf_def;
-      bw_clz_uf_def;
-      bw_ctz_uf_def;
-      bw_ffs_uf_def;
-      bw_fls_uf_def;
-      shift_left_def;
-      shift_right_def;
-      power_def;
-      rem_def;
-      mod_def;
-      not_def;
-      nth_list_def;
-      array_to_list_def;
-      is_null_def;
-      has_alloc_id_def;
-      prov_eq_def;
-      ptr_eq_def;
-      addr_eq_def
-    ]
+  [ mul_uf_def;
+    div_uf_def;
+    power_uf_def;
+    rem_uf_def;
+    mod_uf_def;
+    xor_uf_def;
+    bw_and_uf_def;
+    bw_or_uf_def;
+    bw_clz_uf_def;
+    bw_ctz_uf_def;
+    bw_ffs_uf_def;
+    bw_fls_uf_def;
+    shift_left_def;
+    shift_right_def;
+    power_def;
+    rem_def;
+    mod_def;
+    nth_list_def;
+    array_to_list_def;
+    has_alloc_id_def
+  ]
+
+
+let builtin_fun_defs =
+  max_min_bits @ [ not_def; is_null_def; ptr_eq_def; prov_eq_def; addr_eq_def ]
 
 
 let apply_builtin_funs fsym args loc =
@@ -225,4 +237,8 @@ let apply_builtin_funs fsym args loc =
     return (Some t)
 
 
-let cn_builtin_fun_names = List.map (fun (str, sym, _) -> (str, sym)) builtin_funs
+(* This list of names is later passed to the frontend in bin/main.ml so that these are available in the elaboration,
+   so it should include all builtin function names *)
+let cn_builtin_fun_names =
+  List.map (fun (str, sym, _) -> (str, sym)) builtin_funs
+  @ List.map (fun (str, sym, _) -> (str, sym)) builtin_fun_defs

backend/cn/lib/cn_internal_to_ail.ml

@@ -2849,8 +2849,13 @@ let cn_to_ail_function_internal
         Sym.equal cn_fun.cn_func_name fn_sym)
       cn_functions
   in
-  (* Unsafe - check if list has an element *)
-  let loc = (List.nth matched_cn_functions 0).cn_func_magic_loc in
+  (* If the function is user defined, grab its location from the cn_function associated with it.
+     Otherwise, the location is builtin *)
+  let loc =
+    match List.nth_opt matched_cn_functions 0 with
+    | Some fn -> fn.cn_func_magic_loc
+    | None -> Builtins.loc
+  in
   (* Generating function declaration *)
   let decl =
     ( fn_sym,

backend/cn/lib/compile.ml

@@ -47,10 +47,18 @@ type env =
   }
 
 let init_env tagDefs fetch_enum_expr fetch_typedef =
+  let builtins =
+    List.fold_left
+      (fun acc ((_, sym, def) : Builtins.builtin_fn_def) ->
+        let fsig = { args = def.args; return_bty = def.return_bt } in
+        SymMap.add sym fsig acc)
+      SymMap.empty
+      Builtins.builtin_fun_defs
+  in
   { computationals = SymMap.empty;
     logicals = SymMap.empty;
     predicates = SymMap.empty;
-    functions = SymMap.empty;
+    functions = builtins;
     datatypes = SymMap.empty;
     datatype_constrs = SymMap.empty;
     tagDefs;

backend/cn/lib/core_to_mucore.ml

@@ -1527,6 +1527,8 @@ let normalise_file ~inherit_loc ((fin_markers_env : CAE.fin_markers_env), ail_pr
   let fin_d_st = CAE.{ inner = Pmap.find fin_marker markers_env; markers_env } in
   let env = C.init_env tagDefs (fetch_enum fin_d_st) (fetch_typedef fin_d_st) in
   let@ env = C.add_datatype_infos env ail_prog.cn_datatypes in
+  (* This registers only user defined functions. Builtin functions that can
+     be expressed as index terms are registered in compile.ml in init_env *)
   let@ env = C.register_cn_functions env ail_prog.cn_functions in
   let@ lfuns = ListM.mapM (C.translate_cn_function env) ail_prog.cn_functions in
   let env = C.register_cn_predicates env ail_prog.cn_predicates in
@@ -1572,6 +1574,9 @@ let normalise_file ~inherit_loc ((fin_markers_env : CAE.fin_markers_env), ail_pr
   in
   let stdlib_syms = SymSet.of_list (List.map fst (Pmap.bindings_list file.mi_stdlib)) in
   let datatypes = List.map (translate_datatype env) ail_prog.cn_datatypes in
+  let builtin_lfuns =
+    List.map (fun (_, sym, def) -> (sym, def)) Builtins.builtin_fun_defs
+  in
   let file =
     { mu_main = file.mi_main;
       mu_tagDefs = tagDefs;
@@ -1581,7 +1586,9 @@ let normalise_file ~inherit_loc ((fin_markers_env : CAE.fin_markers_env), ail_pr
       mu_stdlib_syms = stdlib_syms;
       mu_mk_functions = mk_functions;
       mu_resource_predicates = preds;
-      mu_logical_predicates = lfuns;
+      (* Add user defined functions here along with certain builtins that can be
+         easily expressed with index terms *)
+      mu_logical_predicates = builtin_lfuns @ lfuns;
       mu_datatypes = datatypes;
       mu_lemmata = lemmata;
       mu_call_funinfo

backend/cn/lib/indexTerms.ml

@@ -628,7 +628,9 @@ let intToReal_ it loc = IT (Cast (Real, it), BT.Real, loc)
 
 let realToInt_ it loc = IT (Cast (Integer, it), BT.Integer, loc)
 
-let arith_binop op (it, it') loc = IT (Binop (op, it, it'), bt it, loc)
+let binop op (it, it') loc ret = IT (Binop (op, it, it'), ret, loc)
+
+let arith_binop op (it, it') loc = bt it |> binop op (it, it') loc
 
 let arith_unop op it loc = IT (Unop (op, it), bt it, loc)
 

tests/cn/ptr_eq_arg_checking.error.c

@@ -0,0 +1,4 @@
+void f(unsigned int *x, unsigned int y)
+/*@ requires ptr_eq(x,y);
+   ensures true; @*/
+{ }