• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
                • Atj-gen-test-method
                • Atj-shallow-code-generation
                • Atj-common-code-generation
                • Atj-shallow-quoted-constant-generation
                • Atj-pre-translation
                • Atj-gen-everything
                • Atj-name-translation
                • Atj-gen-test-cunit
                • Atj-gen-test-class
                • Atj-gen-main-file
                • Atj-post-translation
                • Atj-deep-code-generation
                  • Atj-gen-deep-term-fns
                  • Atj-gen-deep-test-code
                    • Atj-gen-deep-fndef-method
                    • Atj-gen-deep-fnapp
                    • Atj-gen-deep-env-class
                    • Atj-gen-deep-env-cunit
                    • Atj-gen-deep-lambda
                    • Atj-gen-deep-qconst
                    • Atj-gen-deep-main-class
                    • Atj-gen-deep-term
                    • Atj-gen-deep-terms
                    • Atj-gen-deep-build-method
                    • Atj-gen-deep-call-method
                    • Atj-gen-deep-main-cunit
                    • Atj-gen-deep-fndef-method-name
                    • Atj-gen-deep-fndef-methods
                    • Atj-gen-deep-fndefs
                    • Atj-gen-deep-formals
                    • Atj-gen-deep-var
                  • Atj-gen-test-methods
                  • Atj-gen-test-file
                  • Atj-gen-env-file
                  • Atj-gen-output-subdir
                • Atj-java-primitives
                • Atj-java-primitive-arrays
                • Atj-type-macros
                • Atj-java-syntax-operations
                • Atj-fn
                • Atj-library-extensions
                • Atj-java-input-types
                • Atj-test-structures
                • Aij-notions
                • Atj-macro-definition
              • Atj-tutorial
            • Aij
            • Language
          • Riscv
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Atj-deep-code-generation

    Atj-gen-deep-test-code

    Generate the code of a test method that is specific to the deep embedding approach.

    Signature
    (atj-gen-deep-test-code test-function test-inputs 
                            test-outputs comp-var java-class$) 
     
      → 
    (mv arg-block ares-block call-block jres-block comp-block)
    Arguments
    test-function — Guard (symbolp test-function).
    test-inputs — Guard (atj-test-value-listp test-inputs).
    test-outputs — Guard (atj-test-value-listp test-outputs).
    comp-var — Guard (stringp comp-var).
    java-class$ — Guard (stringp java-class$).
    Returns
    arg-block — Type (jblockp arg-block).
    ares-block — Type (jblockp ares-block).
    call-block — Type (jblockp call-block).
    jres-block — Type (jblockp jres-block).
    comp-block — Type (jblockp comp-block).

    This is used by atj-gen-test-method, which generates a Java method to run one of the tests specified in the :tests input to ATJ. Most of that method's code is the same for deep and shallow embedding. The only varying parts are the ones returned by this function, and by atj-gen-shallow-test-code for the shallow embedding.

    The first block returned by this function builds the input values of the test, and assigns them to an array variable. The block also assigns the function's name to a variable. The array and function name are both arguments to the call method (see below). They are both stored in variables, instead of passing their expressions directly to the method call, in order to accurately measure just the time of each call (see atj-gen-test-method for details), without the time needed to compute the expressions.

    The second block returned by this function builds the output value of the test and assigns it to a variable. If the test has multiple values, they are grouped into a list: in the deep embedding, mv values are always treated as lists.

    The third block returned by this function calls the call method generated by ATJ (which uses the AIJ interpreter), assigning the result to a variable. Again, in the deep embedding multi-valued functions always return a single Java value.

    The fourth block returned by this function is always empty. But we return it for uniformity with atj-gen-shallow-test-code.

    The fifth block returned by this function compares the test output with the call output for equality, assigning the boolean result to a variable. The name of this variable is passed as argument to this function, since it is also used in atj-gen-test-method, thus preventing this and that function to go out of sync in regard to this shared variable name.

    Definitions and Theorems

    Function: atj-gen-deep-test-code

    (defun atj-gen-deep-test-code
           (test-function test-inputs
                          test-outputs comp-var java-class$)
     (declare (xargs :guard (and (symbolp test-function)
                                 (atj-test-value-listp test-inputs)
                                 (atj-test-value-listp test-outputs)
                                 (stringp comp-var)
                                 (stringp java-class$))))
     (let ((__function__ 'atj-gen-deep-test-code))
      (declare (ignorable __function__))
      (b*
       (((mv arg-block arg-exprs & jvar-value-index)
         (atj-gen-test-values test-inputs "value" 1 t nil))
        (arg-block
          (append arg-block
                  (jblock-locvar
                       (jtype-array *aij-type-value*)
                       "functionArguments"
                       (jexpr-newarray-init *aij-type-value* arg-exprs))
                  (jblock-locvar *aij-type-symbol* "functionName"
                                 (atj-gen-symbol test-function t nil))))
        ((mv ares-block ares-exprs & &)
         (atj-gen-test-values test-outputs
                              "value" jvar-value-index t nil))
        (ares-expr (if (and (consp ares-exprs)
                            (not (consp (cdr ares-exprs))))
                       (car ares-exprs)
                     (jexpr-smethod *aij-type-value*
                                    "makeList" ares-exprs)))
        (ares-block (append ares-block
                            (jblock-locvar *aij-type-value*
                                           "acl2Result" ares-expr)))
        (call-expr
             (jexpr-smethod (jtype-class java-class$)
                            "call"
                            (list (jexpr-name "functionName")
                                  (jexpr-name "functionArguments"))))
        (call-block (jblock-locvar *aij-type-value*
                                   "javaResult" call-expr))
        (comp-expr (jexpr-method "acl2Result.equals"
                                 (list (jexpr-name "javaResult"))))
        (comp-block (jblock-locvar (jtype-boolean)
                                   comp-var comp-expr)))
       (mv arg-block
           ares-block call-block nil comp-block))))

    Theorem: jblockp-of-atj-gen-deep-test-code.arg-block

    (defthm jblockp-of-atj-gen-deep-test-code.arg-block
      (b* (((mv ?arg-block ?ares-block
                ?call-block ?jres-block ?comp-block)
            (atj-gen-deep-test-code test-function test-inputs
                                    test-outputs comp-var java-class$)))
        (jblockp arg-block))
      :rule-classes :rewrite)

    Theorem: jblockp-of-atj-gen-deep-test-code.ares-block

    (defthm jblockp-of-atj-gen-deep-test-code.ares-block
      (b* (((mv ?arg-block ?ares-block
                ?call-block ?jres-block ?comp-block)
            (atj-gen-deep-test-code test-function test-inputs
                                    test-outputs comp-var java-class$)))
        (jblockp ares-block))
      :rule-classes :rewrite)

    Theorem: jblockp-of-atj-gen-deep-test-code.call-block

    (defthm jblockp-of-atj-gen-deep-test-code.call-block
      (b* (((mv ?arg-block ?ares-block
                ?call-block ?jres-block ?comp-block)
            (atj-gen-deep-test-code test-function test-inputs
                                    test-outputs comp-var java-class$)))
        (jblockp call-block))
      :rule-classes :rewrite)

    Theorem: jblockp-of-atj-gen-deep-test-code.jres-block

    (defthm jblockp-of-atj-gen-deep-test-code.jres-block
      (b* (((mv ?arg-block ?ares-block
                ?call-block ?jres-block ?comp-block)
            (atj-gen-deep-test-code test-function test-inputs
                                    test-outputs comp-var java-class$)))
        (jblockp jres-block))
      :rule-classes :rewrite)

    Theorem: jblockp-of-atj-gen-deep-test-code.comp-block

    (defthm jblockp-of-atj-gen-deep-test-code.comp-block
      (b* (((mv ?arg-block ?ares-block
                ?call-block ?jres-block ?comp-block)
            (atj-gen-deep-test-code test-function test-inputs
                                    test-outputs comp-var java-class$)))
        (jblockp comp-block))
      :rule-classes :rewrite)