Skip to content

Commit

Permalink
Retrieve correct types out of sizeof during memcpy
Browse files Browse the repository at this point in the history
  • Loading branch information
@R1kM
R1kM committed Jan 16, 2025
1 parent dfc8394 commit 0d55cdd
Show file tree
Hide file tree
Showing 2 changed files with 136 additions and 128 deletions.
28 changes: 16 additions & 12 deletions lib/ClangToAst.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,9 @@ let is_trivial_false (e: Ast.expr) = match e.node with
| EApp ({node = EOp (Neq, _); _ }, [e1; e2]) when e1 = e2 -> true
| _ -> false

let extract_sizeof_ty = function
| ArgumentExpr _ -> failwith "ArgumentExpr not supported"
| ArgumentType ty -> translate_typ ty

(* Translate expression [e], with expected type [t] *)
let rec translate_expr' (env: env) (t: typ) (e: expr) : expr' = match e.desc with
Expand Down Expand Up @@ -266,21 +269,22 @@ let rec translate_expr' (env: env) (t: typ) (e: expr) : expr' = match e.desc wit
remaining in dst. We omit it during the translation *)
| [dst; src; len; _] ->
(* TODO: The type returned by clangml for the arguments is void*.
Hardcoding it to TBuf uint32 to make progress, but to fix
However, clang-analyzer is able to find the correct type, so it should be possible to get the correct type through clangml
In particular, clang-analyzer is able to find the correct type.
If we cannot get it through clangml, we could alternatively retrieve the type
from the sizeof multiplication
In the meantime, we extract it from the sizeof call
*)
let dst = translate_expr env (TBuf (Helpers.uint32, false)) dst in
let src = translate_expr env (TBuf (Helpers.uint32, false)) src in
begin match len.desc with
let len, ty = match len.desc with
(* We recognize the case `len = lhs * sizeof (_)` *)
| BinaryOperator {lhs; kind = Mul; rhs = { desc = UnaryExpr {kind = SizeOf; _}; _}} ->
let len = translate_expr env Helpers.usize lhs in
EBufBlit (src, Helpers.zerou32, dst, Helpers.zerou32, len)
| _ -> failwith "ill-formed memcpy"
end
| BinaryOperator {lhs; kind = Mul; rhs = { desc = UnaryExpr {kind = SizeOf; argument}; _}} ->
let len = translate_expr env Helpers.usize lhs in
let ty = extract_sizeof_ty argument in
len, ty
| _ -> failwith "ill-formed memcpy"
in
let dst = translate_expr env (TBuf (ty, false)) dst in
let src = translate_expr env (TBuf (ty, false)) src in
EBufBlit (src, Helpers.zerou32, dst, Helpers.zerou32, len)

| _ -> failwith "memcpy does not have the right number of arguments"
end

Expand Down
236 changes: 120 additions & 116 deletions test.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,119 +87,123 @@ static inline void chacha20_core(uint32_t *k, uint32_t *ctx, uint32_t ctr)
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);
// }
//
uint32_t load32_le(uint8_t* s) { return 0 }

void store32_le(uint8_t* s, uint32_t n) { }

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 = 0U; // TODO: Uncomment 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 0d55cdd

Please sign in to comment.