Generate a Java method to run one of the specified tests.
(atj-gen-test-method test$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld) → method
This is generated only if the
This is a private static method that prints the name of the test, builds the input values (zero or more) of the test, builds the output value(s) of the test, calls (the Java representation of) the function on the inupt values, compares the obtained result value(s) with the output value(s) of the test, and prints a message of success or failure. It also sets the failures field to true if the test fails.
This method also measures the time of the Java call, by taking the current time just before and just after the call, and subtracting them. It does that for the number of repetitions specified by the integer argument of the method. It stores the times of each call in an array, and calculates the minimum, maximum, and sum of all the times. At the end, it prints all the times, along with minimum, maximum, and average (where the average is obtained from the sum). To prevent unwanted JIT optimizations, a boolean flag is used to cumulatively check that all the repeated calls succeed (in the sense of computing the same result as ACL2); since the code is deterministic, we expect that either they will all succeed or they will all fail.
As a special case, if the integer parameter of the method is 0,
times are not collected,
no minimum/maximum/sum is calculated,
and no time information is printed.
We use a
The code is slightly different based on whether we are using the deep or shallow embedding approach. The differences are factored into the functions atj-gen-deep-test-code and atj-gen-shallow-test-code.
Examining any generated instance of this method should make the above documentation, and the implementation of this code generation function, much clearer.
Function:
(defun atj-gen-test-method (test$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld) (declare (xargs :guard (and (atj-testp test$) (booleanp deep$) (booleanp guards$) (booleanp no-aij-types$) (stringp java-class$) (booleanp verbose$) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (plist-worldp wrld)))) (let ((__function__ 'atj-gen-test-method)) (declare (ignorable __function__)) (b* (((atj-test test) test$) ((unless (consp test.outputs)) (prog2$ (raise "Internal error: the test ~x0 has no outputs." test$) (ec-call (jmethod-fix :irrelevant)))) ((run-when verbose$) (cw " ~s0~%" test.name)) (method-name (atj-gen-test-method-name test.name)) (comp-var "resultsMatch") ((mv arg-block ares-block call-block jres-block comp-block) (if deep$ (atj-gen-deep-test-code test.function test.inputs test.outputs comp-var java-class$) (atj-gen-shallow-test-code test.function test.inputs test.outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld))) (current-time-expr (jexpr-smethod (jtype-class "System") "currentTimeMillis" nil)) (n!=0-expr (jexpr-binary (jbinop-ne) (jexpr-name "n") (jexpr-literal-0))) (method-body (append (jblock-imethod (jexpr-name "System.out") "print" (list (atj-gen-jstring (str::cat "Testing '" test.name "'...")))) arg-block ares-block (jblock-locvar (jtype-boolean) "pass" (jexpr-literal-true)) (jblock-locvar (jtype-array (jtype-long)) "times" (jexpr-cond n!=0-expr (jexpr-newarray (jtype-long) (jexpr-name "n")) (jexpr-literal-null))) (jblock-locvar (jtype-long) "minTime" (jexpr-literal-0)) (jblock-locvar (jtype-long) "maxTime" (jexpr-literal-0)) (jblock-locvar (jtype-long) "sumTime" (jexpr-literal-0)) (jblock-locvar (jtype-int) "i" (jexpr-literal-0)) (jblock-do (append (jblock-locvar (jtype-long) "startTime" current-time-expr) call-block (jblock-locvar (jtype-long) "endTime" current-time-expr) jres-block comp-block (jblock-asg (jexpr-name "pass") (jexpr-binary (jbinop-condand) (jexpr-name "pass") (jexpr-name comp-var))) (jblock-if n!=0-expr (append (jblock-locvar (jtype-long) "time" (jexpr-binary (jbinop-sub) (jexpr-name "endTime") (jexpr-name "startTime"))) (jblock-asg (jexpr-array (jexpr-name "times") (jexpr-name "i")) (jexpr-name "time")) (jblock-asg (jexpr-name "sumTime") (jexpr-binary (jbinop-add) (jexpr-name "sumTime") (jexpr-name "time"))) (jblock-if (jexpr-binary (jbinop-condor) (jexpr-binary (jbinop-eq) (jexpr-name "i") (jexpr-literal-0)) (jexpr-binary (jbinop-lt) (jexpr-name "time") (jexpr-name "minTime"))) (jblock-asg (jexpr-name "minTime") (jexpr-name "time"))) (jblock-if (jexpr-binary (jbinop-gt) (jexpr-name "time") (jexpr-name "maxTime")) (jblock-asg (jexpr-name "maxTime") (jexpr-name "time"))))) (jblock-expr (jexpr-unary (junop-preinc) (jexpr-name "i")))) (jexpr-binary (jbinop-lt) (jexpr-name "i") (jexpr-name "n"))) (jblock-ifelse (jexpr-name "pass") (jblock-imethod (jexpr-name "System.out") "println" (list (atj-gen-jstring " PASS"))) (append (jblock-imethod (jexpr-name "System.out") "println" (list (atj-gen-jstring " FAIL"))) (jblock-asg-name "failures" (jexpr-literal-true)))) (jblock-if n!=0-expr (append (jblock-imethod (jexpr-name "System.out") "println" (list (jexpr-literal-string " Times:"))) (jblock-for (jexpr-binary (jbinop-asg) (jexpr-name "i") (jexpr-literal-0)) (jexpr-binary (jbinop-lt) (jexpr-name "i") (jexpr-name "n")) (jexpr-unary (junop-preinc) (jexpr-name "i")) (jblock-imethod (jexpr-name "System.out") "format" (list (jexpr-literal-string " %.3f%n") (jexpr-binary (jbinop-div) (jexpr-array (jexpr-name "times") (jexpr-name "i")) (jexpr-literal-floating 1000))))) (jblock-imethod (jexpr-name "System.out") "format" (list (jexpr-literal-string " Minimum: %.3f%n") (jexpr-binary (jbinop-div) (jexpr-name "minTime") (jexpr-literal-floating 1000)))) (jblock-imethod (jexpr-name "System.out") "format" (list (jexpr-literal-string " Average: %.3f%n") (jexpr-binary (jbinop-div) (jexpr-binary (jbinop-div) (jexpr-name "sumTime") (jexpr-literal-floating 1000)) (jexpr-name "n")))) (jblock-imethod (jexpr-name "System.out") "format" (list (jexpr-literal-string " Maximum: %.3f%n") (jexpr-binary (jbinop-div) (jexpr-name "maxTime") (jexpr-literal-floating 1000)))) (jblock-imethod (jexpr-name "System.out") "println" nil)))))) (make-jmethod :access (jaccess-private) :abstract? nil :static? t :final? nil :synchronized? nil :native? nil :strictfp? nil :result (jresult-void) :name method-name :params (list (make-jparam :final? nil :type (jtype-int) :name "n")) :throws (and (not no-aij-types$) (list *aij-class-undef-pkg-exc*)) :body method-body))))
Theorem:
(defthm jmethodp-of-atj-gen-test-method (b* ((method (atj-gen-test-method test$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld))) (jmethodp method)) :rule-classes :rewrite)