From c112330b83c0abd6e413ed984e54be2c394282e4 Mon Sep 17 00:00:00 2001 From: Daniel Sainati Date: Wed, 28 Aug 2024 09:33:38 -0400 Subject: [PATCH] Squash commit for ptr_eq PR: replace function_sig in compile.ml with LogicalFunctions.definition Merge github.com:rems-project/cerberus reset to origin master append builtin cn functions to ail_functions in core_to_mucore add builtin flag to translate_cn_expr WIP: replace ptr_eq with cn_function version also don't warn on inequal for builtins replace ptr_eq with a cn function rewrite is_null translate addr_eq and prov_eq refactor Merge branch 'master' of github.com:rems-project/cerberus revert to using LogicalFunctions.definition for compile.ml refactor builtins to use logicalfunctions.definition remove unused function add min and max bits to builtin defs add comment respond to review Merge branch 'master' of github.com:rems-project/cerberus use old function_sig type in compile.ml fix addr_eq Merge branch 'rems-project:master' into master respond to review --- backend/cn/lib/builtins.ml | 209 ++++++++++++++------------- backend/cn/lib/compile.ml | 10 +- backend/cn/lib/core_to_mucore.ml | 9 +- backend/cn/lib/indexTerms.ml | 4 +- tests/cn/ptr_eq_arg_checking.error.c | 4 + 5 files changed, 135 insertions(+), 101 deletions(-) create mode 100644 tests/cn/ptr_eq_arg_checking.error.c diff --git a/backend/cn/lib/builtins.ml b/backend/cn/lib/builtins.ml index abcf6c6da..c411e0af8 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,62 @@ 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) + +let has_alloc_id_def : builtin_fn_def = + mk_builtin_arg1 "has_alloc_id" BT.Loc (fun (sym, bt) -> + hasAllocId_ (sym_ (sym, bt, loc)) 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 +180,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 +198,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 = + [ 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 + ] + + +let builtin_fun_defs = 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 - ] + @ [ not_def; has_alloc_id_def; is_null_def; ptr_eq_def; prov_eq_def; addr_eq_def ] let apply_builtin_funs fsym args loc = @@ -225,4 +234,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/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..7eadf633b 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