Statically add coefficients for pointer offsets

clangml-transforms/for_memcad.ml

@@ -148,6 +148,11 @@ let is_integer_type (t : Clang.Ast.qual_type) =
       true
   | _ -> false
 
+let rec remove_casts (expr : Clang.Ast.expr) =
+  match expr with
+  | { desc = Cast { kind = CStyle; operand; _ }; _ } -> remove_casts operand
+  | _ -> expr
+
 let transform = object (self)
   inherit [_] Clangml_visitors.mapreduce as super
   inherit [_] Free_monoid.free_monoid as monoid
@@ -266,8 +271,30 @@ let transform = object (self)
     let lhs, lhs_value = self#visit_expr lhs_env lhs in
     let kind, kind_value = self#visit_binary_operator_kind env kind in
     let rhs, rhs_value = self#visit_expr rhs_env rhs in
-    BinaryOperator { lhs; kind; rhs },
-    monoid#plus lhs_value (monoid#plus kind_value rhs_value)
+    let delayed_stmts =
+      monoid#plus lhs_value (monoid#plus kind_value rhs_value) in
+    match
+      match kind with
+      | Add | Sub ->
+          begin match Clang.Type.of_node lhs with
+          | { desc = Pointer pointee_type; _ } -> Some pointee_type
+          | _ -> None
+          end
+      | _ -> None
+    with
+    | None ->
+        BinaryOperator { lhs; kind; rhs }, delayed_stmts
+    | Some pointee_type ->
+        let size = Clang.Type.get_size_of pointee_type in
+        let lhs = remove_casts lhs in
+        let rhs =
+          if size = 1 then rhs
+          else
+            { rhs with desc = BinaryOperator {
+              lhs = integer_literal size;
+              kind = Mul;
+              rhs }} in
+        BinaryOperator { lhs; kind; rhs }, delayed_stmts
 
   method! visit_UnaryOperator env kind operand =
     let operand_env =
@@ -344,8 +371,10 @@ let transform = object (self)
             field = FieldName { desc = {
               name = IdentifierName field_name; _ }; _}}; _}; _}; _}}
       when is_integer_type integer_type ->
-        integer_literal (Clang.type_get_offset_of named_type.cxtype field_name),
-        monoid#zero
+        let offset = Clang.type_get_offset_of named_type.cxtype field_name in
+        if offset mod 8 <> 0 then
+          failwith "Bitfields are not supported!";
+        integer_literal (offset / 8), monoid#zero
     | Cast { operand; _ } ->
         self#visit_expr env { expr with desc = operand.desc }
     (* liftConditionals *)