		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-identifier-rules

Rules related to C identifiers.

During symbolic execution, C identifiers in the computation state have the canonical form (ident <string>), where <string> is a quoted string constant. To keep them in this form, we leave ident disabled. Since the symbolic execution sometimes applies ident-fix to identifiers, we enable ident-fix-when-identp and identp-of-ident, so that ident-fix can be rewritten away. Sometimes the symbolic execution produces equalities over identifiers: we introduce a rule that reduces those to equalities over strings. Since the latter equalities involve the string fixer, we enable its executable counterpart. Similarly, sometimes the symbolic execution produces calls of << over identifiers: we introduce a rule that reduces those to << over strings.

In the course of symbolic execution, terms appears of the form (exec-fun <ident> ...), where <ident> is a quoted identifier constant, obtained by the C ASTs being executed. This <ident> does not have the form (ident <string>); we introduce and enable a rule to turn <ident> into (ident <string> when it appears in exec-fun. We introduce similar rules for terms of the same form, but with different functions from exec-fun.

Definitions and Theorems

Theorem: equal-of-ident-and-const

(defthm equal-of-ident-and-const
  (implies (and (syntaxp (and (quotep x) (quotep c)))
                (identp c))
           (equal (equal (ident x) c)
                  (equal (str-fix x) (ident->name c)))))

Theorem: equal-of-const-and-ident

(defthm equal-of-const-and-ident
  (implies (and (syntaxp (and (quotep x) (quotep c)))
                (identp c))
           (equal (equal c (ident x))
                  (equal (str-fix x) (ident->name c)))))

Theorem: equal-of-ident-and-ident

(defthm equal-of-ident-and-ident
  (equal (equal (ident x) (ident y))
         (equal (str-fix x) (str-fix y))))

Theorem: <<-of-ident-and-ident

(defthm <<-of-ident-and-ident
  (equal (<< (ident x) (ident y))
         (<< (str-fix x) (str-fix y))))

Theorem: exec-fun-of-const-identifier

(defthm exec-fun-of-const-identifier
  (implies (and (syntaxp (quotep fun))
                (identp fun))
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun (ident (ident->name fun))
                            args compst fenv limit))))

Theorem: read-static-var-of-const-identifier

(defthm read-static-var-of-const-identifier
  (implies (and (syntaxp (quotep var))
                (identp var))
           (equal (read-static-var var compst)
                  (read-static-var (ident (ident->name var))
                                   compst))))

Theorem: create-var-of-const-identifier

(defthm create-var-of-const-identifier
  (implies (and (syntaxp (quotep var))
                (identp var))
           (equal (create-var var val compst)
                  (create-var (ident (ident->name var))
                              val compst))))

Theorem: read-var-of-const-identifier

(defthm read-var-of-const-identifier
  (implies (and (syntaxp (quotep var))
                (identp var))
           (equal (read-var var compst)
                  (read-var (ident (ident->name var))
                            compst))))

Theorem: write-var-of-const-identifier

(defthm write-var-of-const-identifier
  (implies (and (syntaxp (quotep var))
                (identp var))
           (equal (write-var var val compst)
                  (write-var (ident (ident->name var))
                             val compst))))

Theorem: write-static-var-of-const-identifier

(defthm write-static-var-of-const-identifier
  (implies (and (syntaxp (quotep var))
                (identp var))
           (equal (write-static-var var val compst)
                  (write-static-var (ident (ident->name var))
                                    val compst))))

Theorem: type-struct-of-const-identifier

(defthm type-struct-of-const-identifier
  (implies (and (syntaxp (quotep tag))
                (identp tag))
           (equal (type-struct tag)
                  (type-struct (ident (ident->name tag))))))

Theorem: exec-member-of-const-identifier

(defthm exec-member-of-const-identifier
  (implies (and (syntaxp (quotep mem))
                (identp mem))
           (equal (exec-member val mem)
                  (exec-member val (ident (ident->name mem))))))

Theorem: exec-memberp-of-const-identifier

(defthm exec-memberp-of-const-identifier
  (implies (and (syntaxp (quotep mem))
                (identp mem))
           (equal (exec-memberp val mem compst)
                  (exec-memberp val (ident (ident->name mem))
                                compst))))

Theorem: exec-arrsub-of-member-of-const-identifier

(defthm exec-arrsub-of-member-of-const-identifier
  (implies
       (and (syntaxp (quotep mem))
            (identp mem))
       (equal (exec-arrsub-of-member str mem sub compst)
              (exec-arrsub-of-member str (ident (ident->name mem))
                                     sub compst))))

Theorem: exec-arrsub-of-memberp-of-const-identifier

(defthm exec-arrsub-of-memberp-of-const-identifier
  (implies
       (and (syntaxp (quotep mem))
            (identp mem))
       (equal (exec-arrsub-of-memberp str mem sub compst)
              (exec-arrsub-of-memberp str (ident (ident->name mem))
                                      sub compst))))

Theorem: objdesign-of-var-of-const-identifier

(defthm objdesign-of-var-of-const-identifier
  (implies (and (syntaxp (quotep var))
                (identp var))
           (equal (objdesign-of-var var compst)
                  (objdesign-of-var (ident (ident->name var))
                                    compst))))