Simplified model of the store-cache I use in symbolic execution

store-cache.rkt

#lang racket/base

(require racket/set
         racket/list
         racket/match
         racket/syntax
         redex)

(define-language L
  ;; Syntax
  ;; λ-calculus augmented with integers, mutation, and `begin`
  [#|Expressions|# e ::= u x (e e) (begin e e ...) (if e e e) (set! x e) (add1 e)]
  [#|Values     |# u ::= (λ (x) e) n]
  [#|Numbers    |# n ::= integer]
  [#|Variables  |# x ::= variable-not-otherwise-mentioned]
  
  ;; Semantics
  ;; These are hard-coded for a mono-variant analysis, so:
  ;; - no environment
  ;; - syntactic values are (abstract) semantic values
  ;; 
  ;; The only non-standard things are:
  ;; - Store cache ($) : an environment-like structure that maps each variable location
  ;;   to the value it must hold, or "don't know".
  ;;   This store-cache allows strong updates, and undoes some of the non-determinism
  ;;   introduced from shared store location.
  ;; - Evaluation context frame (rt [ ]): manages store-cache entries
  ;;   at run-time when jumping between callers and callees.
  ;;   For each variable `x` across a caller/callee pair, one of 3 cases must be true:
  ;;   (1) `x` provably references distinct locations across caller and callee:
  ;;       ==> allocate new entry in cache when calling, and restore when returning
  ;;   (2) `x` provably references the same locations between caller and callee:
  ;;       ==> share the same cache entry between them
  ;;   (3) `x` may be the same or different locations between caller and callee:
  ;;       ==> invalidate cache entry for `x` both when calling and returning
  ;; (2) is not in this model for succinctness, but doable.
  ;;
  ;; There can be no alias at the level of set!. This simplifies this model.
  ;; If we view boxes as closures with set!, this model trivially handles boxes soundly
  ;; (but imprecisely).
  ;; Precise handling of mutable boxes is possible, but requires more stuff in the model.
  [#|Runtime Exprs |# E ::= v x (E E) (begin E E ...) (if E E E) (set! x E) (add1 E)
                            (rt (x ...) (x ?v) a E)]
  [#|Runtime Values|# v ::= u ℤ]
  [#|Value Stores  |# σ ::= (side-condition (name σ any) (hash? (term σ)))] ; x → ℘(V)
  [#|Kont  Stores  |# K ::= (side-condition (name K any) (hash? (term K)))] ; α → ℘(ℰ)
  [#|Store Caches  |# $ ::= (side-condition (name $ any) (hash? (term $)))] ; x → V + #f
  [#|Contexts      |# ℰ ::= hole (ℰ E) (v ℰ) (set! x ℰ) (begin ℰ E ...) (if ℰ E E) (add1 ℰ)
                            (rt (x ...) (x ?v) a ℰ)]
  [#|Kont Addrs    |# a ::= any] ; ≃ (E $)
  [#|States        |# ς ::= (E $ σ K)]

  ;; Unimportant helpers
  [?v ::= v #f]
  )

(define-metafunction L
  inj : e -> ς
  [(inj e) (e ,(hash) ,(hash) ,(hash))])

(define-syntax-rule (viz e) (traces -> (term (inj e))))
(define-syntax-rule (ev e) (apply-reduction-relation* -> (term (inj e)) #:cache-all? #t))

;; "context-closure" over ->v
(define ->
  (reduction-relation
   L #:domain ς
   ;; Intra-procedural
   [--> ((in-hole ℰ E_1) $_1 σ_1 K)
        ((in-hole ℰ E_2) $_2 σ_2 K)
        (computed-name (term any_name))
        (where {_ ... (any_name (E_2 $_2 σ_2)) _ ...}
               ,(apply-reduction-relation/tag-with-names ->v (term (E_1 $_1 σ_1))))]
   ;; Jumping
   [--> ((in-hole ℰ ((λ (x) e) v)) $   σ   K  )
        ((rt (x_0 ...) (x ?v) a e) $_1 σ_1 K_1)
        App
        (where (x_0 ...) (-- (fv e) x))
        ;; free `x_0...` will be in-scope, so worst-case ambiguous. Need to invalidate.
        (where $_0 ,(hash-set (term $) (term x) (term v)))
        ;; bound `x` is fresh for any concrete execution, hence keep separate entries
        (where $_1 ,(hash-remove-keys (term $_0) (term (x_0 ...))))
        (where ?v ,(hash-ref (term $) (term x) #f))
        ;; weakly update store as standard
        (where σ_1 (⊔ σ x v))
        ;; push to continuation store
        (where a ,(intern (term (e $_1))))
        (where K_1 (⊔ K a ℰ))]
   ;; Returning
   [--> ((rt (x_0 ...) (x ?v) a v) $   σ K)
        ((in-hole ℰ             v) $_1 σ K)
        Rt
        ;; Invalidate ambiguous locations `x_0...`
        (where $_0 ,(hash-remove-keys (term $) (term (x_0 ...))))
        ;; Restore distinct location `x`
        (where $_1 ,(if (term ?v)
                        (hash-set (term $_0) (term x) (term ?v))
                        (hash-remove (term $_0) (term x))))
        (where {_ ... ℰ _ ...} ,(set->list (hash-ref (term K) (term a))))]))

;; Reduction on "states" whose the control component is only a redex
(define ->v
  (reduction-relation
   L #:domain (E $ σ)
   ;; Cached lookup
   [--> (x $ σ)
        (v $ σ)
        Var
        (judgment-holds (lookup σ $ x v))]

   ;; Begin
   [--> ((begin v E_1 E ...) $ σ)
        ((begin   E_1 E ...) $ σ)
        Begin]
   [--> ((begin v) $ σ)
        (       v  $ σ)
        End]

   ;; Conditionals
   [--> ((if v E _) $ σ)
        (      E    $ σ)
        If-T
        (where #t (maybe-true? v))]
   [--> ((if v _ E) $ σ)
        (        E  $ σ)
        If-F
        (where #t (maybe-false? v))]

   ;; Mutation
   [--> ((set! x v) $   σ  )
        (1          $_1 σ_1)
        Set
        ;; Strongly update store cache
        (where $_1 ,(hash-set (term $) (term x) (term v)))
        ;; Weakly update store
        (where σ_1 (⊔ σ x v))]

   ;; The only primitive
   [--> ((add1 _) $ σ) ; sloppy
        (ℤ       $ σ)
        Add1]
   ))

(define-judgment-form L
  #:contract (lookup σ $ x v)
  #:mode     (lookup I I I O)
  [(where v ,(hash-ref (term $) (term x) #f))
   -----------------------------------------------------"lookup-hit"
   (lookup _ $ x v)]
  [(where #f ,(hash-ref (term $) (term x) #f))
   (where {_ ... v _ ...} ,(set->list (hash-ref (term σ) (term x))))
   -----------------------------------------------------"lookup-miss"
   (lookup σ $ x v)])

(define-metafunction L
  ⊔ : any any any -> σ
    [(⊔ any_m any_k any_v)
     ,(hash-update (term any_m) (term any_k) (λ (vs) (set-add vs (term any_v))) set)])

(define-metafunction L
  fv : e -> (x ...)
  [(fv n) ()]
  [(fv (λ (x) e)) (-- (fv e) x)]
  [(fv x) (x)]
  [(fv (e_1 e_2)) ,(remove-duplicates (term (x_1 ... x_2 ...)))
   (where (x_1 ...) (fv e_1))
   (where (x_2 ...) (fv e_2))]
  [(fv (begin e ...)) ,(remove-duplicates (term (x ... ...)))
   (where ((x ...) ...) ((fv e) ...))]
  [(fv (if e e_1 e_2)) ,(remove-duplicates (term (x ... x_1 ... x_2 ...)))
   (where (x   ...) (fv e  ))
   (where (x_1 ...) (fv e_1))
   (where (x_2 ...) (fv e_2))]
  [(fv (set! x e)) (x)]
  [(fv (add1 e)) (fv e)])

(define-metafunction L
  -- : (any ...) any -> (any ...)
  [(-- (any_1 ... any any_2 ...) any) (any_1 ... any_2 ...)]
  [(-- any_xs _) any_xs]) ; assume no duplicate

(define-relation L
  maybe-true? ⊆ v
  [(maybe-true? (λ (_) _))]
  [(maybe-true? n)
   (side-condition (not (zero? (term n))))]
  [(maybe-true? ℤ)])
(define-relation L
  maybe-false? ⊆ v
  [(maybe-false? 0)]
  [(maybe-false? ℤ)])

(define (hash-remove-keys m xs)
  (for/fold ([m m]) ([x (in-list xs)])
    (hash-remove m x)))

(define intern
  (let ([m (make-hash)])
    (λ (x)
      (hash-ref! m x (λ () (format-symbol "αₖ_~a" (hash-count m)))))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Macros
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-metafunction L
  -let : [x e] e -> e
  [(-let [x e_x] e) ((λ (x) e) e_x)])

(define-metafunction L
  -let* : ([x e] ...) e -> e
  [(-let* () e) e]
  [(-let* ([x_0 e_0] any ...) e)
   (-let [x_0 e_0] (-let* (any ...) e))])


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Examples
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-term ex-1
  (-let* ([id (-let [x 0]
                (λ (n) (begin (set! x n) x)))]
          [id* (id id)]
          [y (id* 1)]
          [z (id* 2)])
   z))

;; (viz ex-1)

(define-term tom-1 ((λ (x) (x x)) (λ (y) (y y))))

(define-term tom-2
  (-let* ([Y (λ (f) ((λ (x) (f (λ (v) ((x x) v))))
                     (λ (y) (f (λ (u) ((y y) u))))))]
          [loop
           (Y (λ (rec)
                (λ (n) (if n n (rec (add1 n))))))])
    (loop 0)))

(define-term wrap
  (-let* ([id (-let [x 0]
                    (λ (n) (begin (set! x n) x)))]
          [id1 (λ (x1) (id x1))]
          [id2 (λ (x2) (id x2))]
          [m (id2 42)]
          [n (id2 43)])
    n))