Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[CN-exec] Fixes for INI demo #609

Merged
merged 4 commits into from
Oct 4, 2024
Merged

[CN-exec] Fixes for INI demo #609

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a11f1a9
Add CN rem implementation and tweak to runtime script
rbanerjee20 Sep 30, 2024
93f469a
Fix recursive function stack overflow by changing translation for CN …
rbanerjee20 Oct 4, 2024
483b585
format
rbanerjee20 Oct 4, 2024
9737224
Add mod implementation to runtime library that is different from rem
rbanerjee20 Oct 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 38 additions & 12 deletions backend/cn/lib/cn_internal_to_ail.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -303,7 +303,7 @@ let cn_to_ail_binop_internal bt1 bt2 =
(A.(Arithmetic Mul), Some (get_cn_int_type_str bt1 bt2 ^ "_multiply"))
| Div | DivNoSMT -> (A.(Arithmetic Div), Some (get_cn_int_type_str bt1 bt2 ^ "_divide"))
| Exp | ExpNoSMT -> (A.And, Some (get_cn_int_type_str bt1 bt2 ^ "_pow"))
| Rem | RemNoSMT -> failwith "TODO cn_to_ail_binop: rem"
| Rem | RemNoSMT -> (A.(Arithmetic Mod), Some (get_cn_int_type_str bt1 bt2 ^ "_rem"))
| Mod | ModNoSMT -> (A.(Arithmetic Mod), Some (get_cn_int_type_str bt1 bt2 ^ "_mod"))
| BW_Xor -> (A.(Arithmetic Bxor), Some (get_cn_int_type_str bt1 bt2 ^ "_xor"))
| BW_And -> (A.(Arithmetic Band), Some (get_cn_int_type_str bt1 bt2 ^ "_bwand"))
Expand Down Expand Up @@ -686,7 +686,7 @@ let dest_with_unit_check
let return_stmt = if is_unit then A.(AilSreturnVoid) else A.(AilSreturn e) in
(b, s @ [ return_stmt ])
| AssignVar x ->
let assign_stmt = A.(AilSdeclaration [ (x, Some e) ]) in
let assign_stmt = A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident x), e)))) in
(b, s @ [ assign_stmt ])
| PassBack -> (b, s, e)

Expand Down Expand Up @@ -910,19 +910,42 @@ let rec cn_to_ail_expr_aux_internal
dest d ([], [], mk_expr ail_call_)
| OffsetOf _ -> failwith "TODO OffsetOf"
| ITE (t1, t2, t3) ->
let result_sym = Sym.fresh () in
let result_ident = A.(AilEident result_sym) in
let result_binding = create_binding result_sym (bt_to_ail_ctype (IT.bt t2)) in
let result_decl = A.(AilSdeclaration [ (result_sym, None) ]) in
let b1, s1, e1 =
cn_to_ail_expr_aux_internal const_prop pred_name dts globals t1 PassBack
in
let b2, s2, e2 =
cn_to_ail_expr_aux_internal const_prop pred_name dts globals t2 PassBack
let wrapped_cond =
A.(AilEcall (mk_expr (AilEident (Sym.fresh_pretty "convert_from_cn_bool")), [ e1 ]))
in
let b3, s3, e3 =
cn_to_ail_expr_aux_internal const_prop pred_name dts globals t3 PassBack
let b2, s2 =
cn_to_ail_expr_aux_internal
const_prop
pred_name
dts
globals
t2
(AssignVar result_sym)
in
let ail_expr_ =
A.(AilEcall (mk_expr (AilEident (Sym.fresh_pretty "cn_ite")), [ e1; e2; e3 ]))
let b3, s3 =
cn_to_ail_expr_aux_internal
const_prop
pred_name
dts
globals
t3
(AssignVar result_sym)
in
let ite_stat =
A.(
AilSif
( mk_expr wrapped_cond,
mk_stmt (AilSblock (b2, List.map mk_stmt s2)),
mk_stmt (AilSblock (b3, List.map mk_stmt s3)) ))
in
dest d (b1 @ b2 @ b3, s1 @ s2 @ s3, mk_expr ail_expr_)
dest d (result_binding :: b1, (result_decl :: s1) @ [ ite_stat ], mk_expr result_ident)
| EachI ((r_start, (sym, bt'), r_end), t) ->
(*
Input:
Expand Down Expand Up @@ -2942,11 +2965,12 @@ let rec cn_to_ail_lat_internal ?(is_toplevel = true) dts pred_sym_opt globals pr
| LAT.Define ((name, it), info, lat) ->
let ctype = bt_to_ail_ctype (IT.bt it) in
let binding = create_binding name ctype in
let decl = A.(AilSdeclaration [ (name, None) ]) in
let b1, s1 =
cn_to_ail_expr_internal_with_pred_name pred_sym_opt dts globals it (AssignVar name)
in
let b2, s2 = cn_to_ail_lat_internal ~is_toplevel dts pred_sym_opt globals preds lat in
(b1 @ b2 @ [ binding ], s1 @ s2)
(b1 @ b2 @ [ binding ], (decl :: s1) @ s2)
| LAT.Resource ((name, (ret, bt)), (loc, str_opt), lat) ->
let b1, s1 =
cn_to_ail_resource_internal ~is_pre:true ~is_toplevel name dts globals preds loc ret
Expand Down Expand Up @@ -3085,9 +3109,10 @@ let rec cn_to_ail_post_aux_internal dts globals preds = function
Core_to_mucore.fn_spec_instrumentation_sym_subst_lrt (name, IT.bt it, new_name) t
in
let binding = create_binding new_name (bt_to_ail_ctype (IT.bt it)) in
let decl = A.(AilSdeclaration [ (new_name, None) ]) in
let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar new_name) in
let b2, s2 = cn_to_ail_post_aux_internal dts globals preds new_lrt in
(b1 @ b2 @ [ binding ], s1 @ s2)
(b1 @ b2 @ [ binding ], (decl :: s1) @ s2)
| LRT.Resource ((name, (re, bt)), (loc, str_opt), t) ->
let new_name = generate_sym_with_suffix ~suffix:"_cn" name in
let b1, s1 =
Expand Down Expand Up @@ -3214,6 +3239,7 @@ let rec cn_to_ail_lat_internal_2 with_ownership_checking dts globals preds c_ret
in
(* let ctype = mk_ctype C.(Pointer (empty_qualifiers, ctype)) in *)
let binding = create_binding new_name ctype in
let decl = A.(AilSdeclaration [ (new_name, None) ]) in
let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar new_name) in
let ail_executable_spec =
cn_to_ail_lat_internal_2
Expand All @@ -3224,7 +3250,7 @@ let rec cn_to_ail_lat_internal_2 with_ownership_checking dts globals preds c_ret
c_return_type
new_lat
in
prepend_to_precondition ail_executable_spec (binding :: b1, s1)
prepend_to_precondition ail_executable_spec (binding :: b1, decl :: s1)
| LAT.Resource ((name, (ret, bt)), (loc, str_opt), lat) ->
let new_name = generate_sym_with_suffix ~suffix:"_cn" name in
let b1, s1 =
Expand Down
13 changes: 13 additions & 0 deletions runtime/libcn/include/cn-executable/utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,8 +259,20 @@ cn_bool *cn_pointer_gt(cn_pointer *i1, cn_pointer *i2);
return CNTYPE##_gt(i1, i2) ? i1 : i2;\
}

/* TODO: Account for UB: https://stackoverflow.com/a/20638659 */
#define CN_GEN_MOD(CTYPE, CNTYPE)\
static inline CNTYPE *CNTYPE##_mod(CNTYPE *i1, CNTYPE *i2) {\
CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\
res->val = i1->val % i2->val;\
if (res->val < 0) {\
res->val = (i2->val < 0) ? res->val - i2->val : res->val + i2->val;\
}\
return res;\
}


#define CN_GEN_REM(CTYPE, CNTYPE)\
static inline CNTYPE *CNTYPE##_rem(CNTYPE *i1, CNTYPE *i2) {\
CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\
res->val = i1->val % i2->val;\
return res;\
Expand Down Expand Up @@ -421,6 +433,7 @@ cn_bool *default_cn_bool(void);
CN_GEN_MIN(CNTYPE) \
CN_GEN_MAX(CNTYPE) \
CN_GEN_MOD(CTYPE, CNTYPE) \
CN_GEN_REM(CTYPE, CNTYPE) \
CN_GEN_XOR(CTYPE, CNTYPE) \
CN_GEN_BWAND(CTYPE, CNTYPE) \
CN_GEN_BWOR(CTYPE, CNTYPE) \
Expand Down
Loading