(datatype FuncT (Func String))
(datatype StmtT (Stmt String))
(datatype ExprT (Expr String))
(datatype FieldT (Field String))
(datatype TypeT (Type String))
(datatype AllocT (Alloc AllocT) (AllocVar ExprT))

(relation func (FuncT ExprT TypeT TypeT))
(relation func-stmt (FuncT StmtT))
(relation assign (StmtT TypeT ExprT ExprT))
(relation field-assign (StmtT ExprT FieldT ExprT))
(relation store (StmtT ExprT ExprT))
(relation expr (StmtT ExprT))
(relation return (StmtT ExprT))
(relation eq (ExprT ExprT ExprT))
(relation call (ExprT FuncT ExprT))
(relation add (ExprT ExprT ExprT))
(relation field (ExprT ExprT FieldT))
(relation struct-lit-field (ExprT FieldT ExprT))
(relation addr (ExprT ExprT FieldT))
(relation load (ExprT ExprT))
(relation malloc (ExprT TypeT))

;; typedef struct s {
;;   int x;
;;   int y;
;; } s;

;; int mul(struct s q) { ... }

;; int fact(int i) {
;;   int c = i == 0;
;;   if (c) {
;;     return 1;
;;   } else {
;;     int j = i + -1;
;;     int r = fact(j);
;;     int prod = mul((struct s){i, r});
;;     return prod;
;;   }
;; }
;; (func (Func "fact") (Expr "i") (Type "int") (Type "int"))
;; (func-stmt (Func "fact") (Stmt "int c = i == 0;"))
;; (func-stmt (Func "fact") (Stmt "if ..."))
;; (func-stmt (Func "fact") (Stmt "return 1"))
;; (func-stmt (Func "fact") (Stmt "int j = i + -1"))
;; (func-stmt (Func "fact") (Stmt "int r = fact(j)"))
;; (func-stmt (Func "fact") (Stmt "int prod = mul({ x: i, y: r })"))
;; (func-stmt (Func "fact") (Stmt "return prod"))
;; (assign (Stmt "int c = i == 0") (Type "int") (Expr "c") (Expr "i == 0"))
;; (assign (Stmt "int j = i + -1") (Type "int") (Expr "j") (Expr "i + -1"))
;; (assign (Stmt "int r = fact(j)") (Type "int") (Expr "r") (Expr "fact(j)"))
;; (assign (Stmt "int prod = mul({ x: i, y: r })") (Type "int") (Expr "prod") (Expr "mul({ x: i, y: r })"))
;; (eq (Expr "i == 0") (Expr "i") (Expr "0"))
;; (add (Expr "i + -1") (Expr "i") (Expr "-1"))
;; (call (Expr "fact(j)") (Func "fact") (Expr "j"))
;; (call (Expr "mul({ x: i, y: r })") (Func "mul") (Expr "{ x: i, y: r }"))
;; (return (Stmt "return prod") (Expr "prod"))

;; typedef struct s {
;;   int *x;
;;   int *y;
;; } s;

;; void swap(struct s *r) {
;;   int **xp = &(r->x);
;;   int **yp = &(r->y);
;;   int *a = *xp;
;;   int *b = *yp;
;;   *xp = a;
;;   *yp = b;
;; }

;; int f(int i) {
;;   struct s *sp = malloc(sizeof(struct s));
;;   int *u = malloc(sizeof(int));
;;   int *v = malloc(sizeof(int));
;;   *u = i;
;;   *v = i;
;;   *sp = (struct s){u, v};
;;   swap(sp);
;;   int **zpp = &(sp->x);
;;   int *zp = *zpp;
;;   return *zp;
;; }
(func (Func "swap") (Expr "r") (Type "void") (Type "{int *x; int *y;}*"))
;; statements
(func-stmt (Func "swap") (Stmt "int **xp = &(r->x)"))
(func-stmt (Func "swap") (Stmt "int **yp = &(r->y)"))
(func-stmt (Func "swap") (Stmt "int *z = *xp"))
(func-stmt (Func "swap") (Stmt "int *w = *yp"))
(func-stmt (Func "swap") (Stmt "*xp = a"))
(func-stmt (Func "swap") (Stmt "*yp = b"))
(assign (Stmt "int **xp = &(r->x)") (Type "int **") (Expr "xp") (Expr "&(r->x)"))
(assign (Stmt "int **yp = &(r->x)") (Type "int **") (Expr "yp") (Expr "&(r->y)"))
(assign (Stmt "int *a = *xp") (Type "int *") (Expr "a") (Expr "*xp"))
(assign (Stmt "int *b = *yp") (Type "int *") (Expr "b") (Expr "*yp"))
(store (Stmt "*xp = a") (Expr "xp") (Expr "a"))
(store (Stmt "*yp = b") (Expr "yp") (Expr "b"))
;; expressions
(addr (Expr "&(r->x)") (Expr "r") (Field "x"))
(addr (Expr "&(r->y)") (Expr "r") (Field "y"))
(load (Expr "*xp") (Expr "xp"))
(load (Expr "*yp") (Expr "yp"))

(func (Func "f") (Expr "i") (Type "int") (Type "int"))
;; statements
(func-stmt (Func "f") (Stmt "struct s *sp = malloc(sizeof(struct s))"))
(func-stmt (Func "f") (Stmt "int *u = malloc(sizeof(int))"))
(func-stmt (Func "f") (Stmt "int *v = malloc(sizeof(int))"))
(func-stmt (Func "f") (Stmt "*u = i"))
(func-stmt (Func "f") (Stmt "*v = i"))
(func-stmt (Func "f") (Stmt "*sp = (struct s){u, v}"))
(func-stmt (Func "f") (Stmt "swap(sp)"))
(func-stmt (Func "f") (Stmt "int **zpp = &(sp->x)"))
(func-stmt (Func "f") (Stmt "int *zp = *zpp"))
(func-stmt (Func "f") (Stmt "return *zp"))
(assign (Stmt "struct s *sp = malloc(sizeof(struct s))") (Type "struct s*") (Expr "sp") (Expr "malloc(sizeof(struct s))"))
(assign (Stmt "int *u = malloc(sizeof(int))") (Type "int *") (Expr "u") (Expr "malloc(sizeof(int))"))
(assign (Stmt "int *v = malloc(sizeof(int))") (Type "int *") (Expr "v") (Expr "malloc(sizeof(int))"))
(store (Stmt "*u = i") (Expr "u") (Expr "i"))
(store (Stmt "*v = i") (Expr "v") (Expr "i"))
(store (Stmt "*sp = (struct s){u, v}") (Expr "sp") (Expr "(struct s){u, v}"))
(expr (Stmt "swap(sp)") (Expr "swap(sp)"))
(assign (Stmt "int **zpp = &(sp->x)") (Type "int **") (Expr "zpp") (Expr "&(sp->x)"))
(assign (Stmt "int *zp = *zpp") (Type "int *") (Expr "zp") (Expr "*zpp"))
(return (Stmt "return *zp") (Expr "*zp"))
;; expressions
(malloc (Expr "malloc(sizeof(struct s))") (Type "struct s"))
(malloc (Expr "malloc(sizeof(int))") (Type "int"))
(struct-lit-field (Expr "(struct s){u, v}") (Field "x") (Expr "u"))
(struct-lit-field (Expr "(struct s){u, v}") (Field "y") (Expr "v"))
(call (Expr "swap(sp)") (Func "swap") (Expr "sp"))
(addr (Expr "&(sp->x)") (Expr "sp") (Field "x"))
(load (Expr "*zpp") (Expr "zpp"))
(load (Expr "*zp") (Expr "zp"))

;; a variable points to its allocation
(function expr-points-to (ExprT) AllocT)
(function ptr-points-to (AllocT) AllocT)

;; If `v = malloc(...)`, then `v -> alloc[v]`.
(rule (
    (assign s t1 v c)
    (malloc c t2)
)(
    (union (expr-points-to v) (AllocVar v))
))

;; If `t v = e` and `e -> a`, then `v -> a`.
(rule (
    (assign s t v e)
    (= (expr-points-to e) a)
)(
    (union (expr-points-to v) a)
))

;; If `*v = u`, `v -> a`, and `u -> b`, then `a -> b`.
(rule (
    (store s v u)
    (= (expr-points-to v) a)
    (= (expr-points-to u) b)
)(
    (union (ptr-points-to a) b)
))

;; If `e.f -> a` then `e -> a`.
(rule (
    (field ef e f)
    (= (expr-points-to ef) a)
)(
    (union (expr-points-to e) a)
))

;; If `e -> a` then `e.f -> a`.
(rule (
    (= (expr-points-to e) a)
    (field ef e f)
)(
    (union (expr-points-to ef) a)    
))

;; If `u -> a` and `a -> b`, then `&(u->f) -> b`.
(rule (
    (= (expr-points-to u) a)
    (= (ptr-points-to a) b)
    (addr e u f)
)(
    (union (expr-points-to e) b)
))

;; If `u -> a` and `&(u->f) -> b`, then `a -> b`.
(rule (
    (= (expr-points-to u) a)
    (addr e u f)
    (= (expr-points-to e) b)
)(
    (union (ptr-points-to a) b)
))

;; If `(struct t){..., x, ...}` and `x -> b`, then `(struct t){..., x, ...} -> b`.
(rule (
    (struct-lit-field l f x)
    (= (expr-points-to x) b)
)(
    (union (expr-points-to l) b)    
))

;; If `f(t* x)`, `f(v)`, and `v -> a`, then `x -> a`.
(rule (
    (func f x in out)
    (call e f v)
    (= (expr-points-to v) a)
)(
    (union (expr-points-to x) a)  
))

;; If `return u` in `f` and `u -> a`, then `f(z) -> a`.
(rule (
    (call e f v)
    (func-stmt f s)
    (return s u)
    (= (expr-points-to u) a)
)(
    (union (expr-points-to e) a)    
))

;; store rule
(rule (
    (load e u)
    (= (expr-points-to u) a)
    (= (ptr-points-to a) b)
)(
    (union (expr-points-to e) b)
))

(run 40)

(check (= (AllocVar (Expr "v")) (AllocVar (Expr "u"))))
(check (!= (AllocVar (Expr "v")) (AllocVar (Expr "sp"))))

(query-extract :variants 100 (AllocVar (Expr "u")))
(query-extract :variants 100 (AllocVar (Expr "sp")))