Skip to content

Commit

Permalink
Support pointer arithmetic
Browse files Browse the repository at this point in the history
  • Loading branch information
@R1kM
R1kM committed Jan 10, 2025
1 parent 58786c1 commit 2ad2293
Show file tree
Hide file tree
Showing 3 changed files with 139 additions and 18 deletions.
28 changes: 19 additions & 9 deletions lib/ClangToAst.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,11 +75,14 @@ let translate_unop (kind: Clang__Clang__ast.unary_operator_kind) : K.op = match

let translate_binop (kind: Clang__Clang__ast.binary_operator_kind) : K.op = match kind with
| PtrMemD | PtrMemI -> failwith "translate_binop: ptr mem"
| Mul | Div | Rem -> failwith " translate_binop: arith expr"

(* TODO: Might need to disambiguate for pointer arithmetic *)
(* Disambiguation for pointer arithmetic must be done when calling translate_binop:
This is a deeper rewriting than just disambiguating between two K.op *)
| Add -> Add
| Sub -> Sub
| Mul -> Mult

| Div | Rem -> failwith " translate_binop: arith expr"

| Shl -> BShiftL
| Shr -> BShiftR
Expand Down Expand Up @@ -110,6 +113,7 @@ let translate_binop (kind: Clang__Clang__ast.binary_operator_kind) : K.op = matc

let translate_typ_name = function
| "size_t" -> Helpers.usize
| "uint8_t" -> Helpers.uint8
| "uint32_t" -> Helpers.uint32
| s ->
Printf.printf "type name %s is unsupported\n" s;
Expand Down Expand Up @@ -230,11 +234,17 @@ let rec translate_expr' (env: env) (t: typ) (e: expr) : expr' = match e.desc wit
let lhs = translate_expr env lhs_ty lhs in
let rhs = translate_expr env (typ_of_expr rhs) rhs in
let kind = translate_binop kind in
(* TODO: Likely need a "assert_tint_or_tbool" *)
let lhs_w = Helpers.assert_tint lhs_ty in
let op_type = Helpers.type_of_op kind (Helpers.assert_tint lhs_ty) in
let op : Ast.expr = with_type op_type (EOp (kind, lhs_w)) in
EApp (op, [lhs; rhs])
(* In case of pointer arithmetic, we need to perform a rewriting into EBufSub/Diff *)
begin match lhs_ty, kind with
| TBuf _, Add -> EBufSub (lhs, rhs)
| TBuf _, Sub -> EBufDiff (lhs, rhs)
| _ ->
(* TODO: Likely need a "assert_tint_or_tbool" *)
let lhs_w = Helpers.assert_tint lhs_ty in
let op_type = Helpers.type_of_op kind (Helpers.assert_tint lhs_ty) in
let op : Ast.expr = with_type op_type (EOp (kind, lhs_w)) in
EApp (op, [lhs; rhs])
end

| DeclRef {name; _} -> get_id_name name |> find_var env

Expand Down Expand Up @@ -413,13 +423,13 @@ let translate_fundecl (fdecl: function_decl) =
TODO: Proper handling of decls *)
let translate_decl (decl: decl) = match decl.desc with
| Function fdecl ->
let name = get_id_name fdecl.name in
(* TODO: How to handle libc? *)
let loc = Clang.Ast.location_of_node decl |> Clang.Ast.concrete_of_source_location File in
let file_loc = loc.filename in
(* TODO: Support multiple files *)
if file_loc = "test.c" then (
(* Printf.printf "Translating function %s\n" name; *)
(* let name = get_id_name fdecl.name in
Printf.printf "Translating function %s\n" name; *)
Some (translate_fundecl fdecl)
) else None
| _ -> None
Expand Down
3 changes: 2 additions & 1 deletion lib/Helpers.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ end

(* Creating AST nodes *********************************************************)

let uint8 = TInt K.UInt8
let uint32 = TInt K.UInt32
let usize = TInt K.SizeT

Expand Down Expand Up @@ -345,7 +346,7 @@ class ['self] readonly_visitor = object (self: 'self)
| EPolyComp _
| EOp _ ->
List.for_all (self#visit_expr_w ()) es
| EQualified _
| EQualified _
when is_readonly_builtin_lid e ->
List.for_all (self#visit_expr_w ()) es
| ETApp ({ node = EQualified _; _ } as e, _, _, _)
Expand Down
126 changes: 118 additions & 8 deletions test.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,7 @@
void test(uint32_t *st, uint32_t y, uint32_t z) {
uint32_t x = y + z;

int num = 0;
int sum = 0;

// for loop terminates when count exceeds num
for(int count = 1; count < num; count++)
{
sum += count;
}
uint32_t* st2 = st + 4U;
}


Expand Down Expand Up @@ -93,3 +86,120 @@ static inline void chacha20_core(uint32_t *k, uint32_t *ctx, uint32_t ctr)
os[i] = x;);
k[12U] = k[12U] + ctr_u32;
}

// void Hacl_Impl_Chacha20_chacha20_init(uint32_t *ctx, uint8_t *k, uint8_t *n, uint32_t ctr)
// {
// KRML_MAYBE_FOR4(i,
// 0U,
// 4U,
// 1U,
// uint32_t x = Hacl_Impl_Chacha20_Vec_chacha20_constants[i];
// uint32_t *os = ctx;
// os[i] = x;);
// uint32_t *uu____0 = ctx + 4U;
// KRML_MAYBE_FOR8(i,
// 0U,
// 8U,
// 1U,
// uint8_t *bj = k + i * 4U;
// uint32_t u = load32_le(bj);
// uint32_t r = u;
// uint32_t x = r;
// uint32_t *os = uu____0;
// os[i] = x;);
// ctx[12U] = ctr;
// uint32_t *uu____1 = ctx + 13U;
// KRML_MAYBE_FOR3(i,
// 0U,
// 3U,
// 1U,
// uint8_t *bj = n + i * 4U;
// uint32_t u = load32_le(bj);
// uint32_t r = u;
// uint32_t x = r;
// uint32_t *os = uu____1;
// os[i] = x;);
// }
//
// static void chacha20_encrypt_block(uint32_t *ctx, uint8_t *out, uint32_t incr, uint8_t *text)
// {
// uint32_t k[16U] = { 0U };
// chacha20_core(k, ctx, incr);
// uint32_t bl[16U] = { 0U };
// KRML_MAYBE_FOR16(i,
// 0U,
// 16U,
// 1U,
// uint8_t *bj = text + i * 4U;
// uint32_t u = load32_le(bj);
// uint32_t r = u;
// uint32_t x = r;
// uint32_t *os = bl;
// os[i] = x;);
// KRML_MAYBE_FOR16(i,
// 0U,
// 16U,
// 1U,
// uint32_t x = bl[i] ^ k[i];
// uint32_t *os = bl;
// os[i] = x;);
// KRML_MAYBE_FOR16(i, 0U, 16U, 1U, store32_le(out + i * 4U, bl[i]););
// }
//
// static inline void
// chacha20_encrypt_last(uint32_t *ctx, uint32_t len, uint8_t *out, uint32_t incr, uint8_t *text)
// {
// uint8_t plain[64U] = { 0U };
// memcpy(plain, text, len * sizeof (uint8_t));
// uint8_t plain_copy[64U] = { 0U };
// memcpy(plain_copy, plain, 64U * sizeof (uint8_t));
// chacha20_encrypt_block(ctx, plain, incr, plain_copy);
// memcpy(out, plain, len * sizeof (uint8_t));
// }
//
// void
// Hacl_Impl_Chacha20_chacha20_update(uint32_t *ctx, uint32_t len, uint8_t *out, uint8_t *text)
// {
// uint32_t rem = len % 64U;
// uint32_t nb = len / 64U;
// uint32_t rem1 = len % 64U;
// for (uint32_t i = 0U; i < nb; i++)
// {
// chacha20_encrypt_block(ctx, out + i * 64U, i, text + i * 64U);
// }
// if (rem1 > 0U)
// {
// chacha20_encrypt_last(ctx, rem, out + nb * 64U, nb, text + nb * 64U);
// }
// }
//
// void
// Hacl_Chacha20_chacha20_encrypt(
// uint32_t len,
// uint8_t *out,
// uint8_t *text,
// uint8_t *key,
// uint8_t *n,
// uint32_t ctr
// )
// {
// uint32_t ctx[16U] = { 0U };
// Hacl_Impl_Chacha20_chacha20_init(ctx, key, n, ctr);
// Hacl_Impl_Chacha20_chacha20_update(ctx, len, out, text);
// }
//
// void
// Hacl_Chacha20_chacha20_decrypt(
// uint32_t len,
// uint8_t *out,
// uint8_t *cipher,
// uint8_t *key,
// uint8_t *n,
// uint32_t ctr
// )
// {
// uint32_t ctx[16U] = { 0U };
// Hacl_Impl_Chacha20_chacha20_init(ctx, key, n, ctr);
// Hacl_Impl_Chacha20_chacha20_update(ctx, len, out, cipher);
// }
//

0 comments on commit 2ad2293

Please sign in to comment.