From feb58d034d171be0b5cc39fc5135036145d808c6 Mon Sep 17 00:00:00 2001
From: Thierry Martinez <Thierry.Martinez@inria.fr>
Date: Fri, 6 Jan 2023 14:28:22 +0100
Subject: [PATCH] Convert array subscript on pointers to pointer arithmetic
---
clangml-transforms/for_memcad.ml | 20 +++++++++++++++++---
1 file changed, 17 insertions(+), 3 deletions(-)
diff --git a/clangml-transforms/for_memcad.ml b/clangml-transforms/for_memcad.ml
index d69146e..6523591 100644
--- a/clangml-transforms/for_memcad.ml
+++ b/clangml-transforms/for_memcad.ml
@@ -596,6 +596,11 @@ with type 'a Applicative.t = 'a Applicative.t = struct
{ record_decl with fields = name_anonymous_fields record_decl.fields },
Free_monoid.zero
+ let is_pointer_type (ty : Clang.Type.t) =
+ match ty.desc with
+ | Pointer _ -> true
+ | _ -> false
+
let hook :
type a . a Refl.refl -> (a -> env -> a * accu) -> (a -> env -> a * accu) =
fun refl super x env ->
@@ -624,9 +629,18 @@ with type 'a Applicative.t = 'a Applicative.t = struct
Visit.visit [%refl: Clang.Ast.expr] []
cond { env with in_condition = true } in
Call { callee; args = [cond] }, cond_stmts
- | UnaryExpr { kind = SizeOf; argument } ->
- visit_unary_expr_size_of argument env
- | _ -> super x env
+ | UnaryExpr { kind = SizeOf; argument } ->
+ visit_unary_expr_size_of argument env
+ | ArraySubscript { base; index }
+ when is_pointer_type (Clang.Type.of_node base) ->
+ let x' : Clang.Ast.expr_desc = UnaryOperator {
+ kind = Deref;
+ operand = { base with desc = BinaryOperator {
+ lhs = base;
+ kind = Add;
+ rhs = index; }}} in
+ super x' env
+ | _ -> super x env
end
| Clang.Ast.Refl_decl_desc ->
begin match x with
--
GitLab