Gavin/ptr chunk v2

[ggwg]

Pattern match based on the type of the chunk

Test Program 1

struct IntPtrWrapper {
    int *age;
};

int *getPtrFromStruct(struct IntPtrWrapper *a) {
    int *age = a->age;
    return age;
}

Test Program 2

typedef struct node_s {
    int val;
    struct node_s *next;
    struct node_s *prev;
} Node;

typedef struct list_s {
    Node *head;
    Node *tail;
} List;

int test(List *list) {
    Node *node = list->head;
    // Node *next = node->next;
    // return next->val;
    return 0;
}

---

Example Output of load operation with matched pointer type

--test: 2--
TIME: 0.059568
CMD: gvar__1 := "i__loadv"("ptr", gvar__0)
LOC: unknown loc
PROCS: [test]
LOOPS: [] ++ []
BRANCHING: 0

• Note: the loaded type is a "ptr", which will then be changed to Chunk.Mptr type.

[ggwg]

TODO:

• Apply the right fix for Mptr type

  | Mfloat32 ->
          (Expr.EList [ Expr.string single_type; new_var_e ], Type.NumberType)
      | Mfloat64 ->
          (Expr.EList [ Expr.string float_type; new_var_e ], Type.NumberType)
      | Mint64 ->
          (Expr.EList [ Expr.string long_type; new_var_e ], Type.IntType)
      (* TODO: Change this *)
      | Mptr ->
          if Compcert.Archi.ptr64 then
            (Expr.EList [ Expr.string long_type; new_var_e ], Type.IntType)
          else (Expr.EList [ Expr.string int_type; new_var_e ], Type.IntType)
      | _ -> (Expr.EList [ Expr.string int_type; new_var_e ], Type.IntType)

Things to double check

• Correctness of pattern matching:

  (* Lookup type of variable using Clight program to determine whether it is a pointer *)
    let chunk =
      match compcert_chunk with
      (* Check whether chunk is a pointer - Mint64 or Mint32 can be pointer types *)
      | Mint64 | Mint32 -> (
          let typ =
            match expp with
            (* Get the id of the variable from CSharpMinor *)
            | Ebinop (_, Evar id, _) ->
                let open Clight in
                let rec find_var var_list =
                  match var_list with
                  | (var_id, var_typ) :: vs ->
                      if var_id == id then var_typ else find_var vs
                  | _ ->
                      failwith
                        (Printf.sprintf
                           "Variable with ident %d was not found inside \
                            function %s of Clight"
                           (num_to_integer id) fname)
                in
                let clight_fun =
                  Gil_logic_gen.get_clight_fun clight_prog fid
                in
                find_var
                  (clight_fun.fn_params @ clight_fun.fn_vars
                 @ clight_fun.fn_temps)
            | _ -> failwith (Printf.sprintf "Unexpected type")
          in
          match typ with
          | Tpointer _ -> Chunk.Mptr
          | _ -> Chunk.of_compcert_ast_chunk compcert_chunk)
      | _ -> Chunk.of_compcert_ast_chunk compcert_chunk

[ggwg]

Thank you so much for reviewing on the bank holiday!