diff --git a/backend/cn/lib/builtins.ml b/backend/cn/lib/builtins.ml index abcf6c6da..cd9c327d2 100644 --- a/backend/cn/lib/builtins.ml +++ b/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 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 diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 77afa79b0..16b5d2ae7 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/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, diff --git a/backend/cn/lib/compile.ml b/backend/cn/lib/compile.ml index cb84b4831..440da2600 100644 --- a/backend/cn/lib/compile.ml +++ b/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; diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml index 401097691..9e3ee86f1 100644 --- a/backend/cn/lib/core_to_mucore.ml +++ b/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 diff --git a/backend/cn/lib/indexTerms.ml b/backend/cn/lib/indexTerms.ml index 52483086c..c0da968e6 100644 --- a/backend/cn/lib/indexTerms.ml +++ b/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) diff --git a/tests/cn/ptr_eq_arg_checking.error.c b/tests/cn/ptr_eq_arg_checking.error.c new file mode 100644 index 000000000..cc5b294a9 --- /dev/null +++ b/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; @*/ +{ } \ No newline at end of file