[acl2/acl2] 941ea5: x86isa: rm08 and wm08 are also defined in terms of...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 941ea58fdf845328f2124a6639f3cbc2bc5e42dc
https://github.com/acl2/acl2/commit/941ea58fdf845328f2124a6639f3cbc2bc5e42dc
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-07-26 (Tue, 26 Jul 2016)

Changed paths:
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/proofs/factorial/fact-inductive-assertions.lisp
M books/projects/x86isa/proofs/factorial/fact-wormhole-abstraction.lisp
M books/projects/x86isa/proofs/utilities/general-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/programmer-level-mode/programmer-level-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-top.lisp
M books/projects/x86isa/proofs/wordCount/wc.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp

Log Message:
-----------
x86isa: rm08 and wm08 are also defined in terms of rb and wb now

Lemmas rm08-to-rb and wm08-to-wb don't need to exist anymore.


Commit: 923b256cd63ad2ef946b50eed9eef213c1091493
https://github.com/acl2/acl2/commit/923b256cd63ad2ef946b50eed9eef213c1091493
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-07-26 (Tue, 26 Jul 2016)

Changed paths:
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/portcullis/sharp-dot-constants.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp
A books/projects/x86isa/tools/execution/examples/nop-sequence/acl2-customization.lsp
A books/projects/x86isa/tools/execution/examples/nop-sequence/cert.acl2
A books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp
M books/projects/x86isa/utils/decoding-utilities.lisp
M books/projects/x86isa/utils/utilities.lisp

Log Message:
-----------
x86isa: Fixed incorrect counting of the total number of prefixes (thanks, Dmitry Nadezhin!)

Previously, if redundant prefixes were present in a legal x86
instruction, the function get-prefixes did not count the total number
of prefixes correctly. Thanks to an example sent over by Dmitry that
helped me find and fix this bug!

Also added a concrete execution example
tools/execution/examples/nop-sequence/nop.lsp that checks if the
recommended multi-byte sequence of NOP (Intel Vol. 2B, NOP
Instruction-Set Reference) is supported by the x86isa books (it is).


Commit: a780c279d941e0fe2dbb01c26d45a7f10d1c6060
https://github.com/acl2/acl2/commit/a780c279d941e0fe2dbb01c26d45a7f10d1c6060
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-07-26 (Tue, 26 Jul 2016)

Changed paths:
M acl2-fns.lisp
M acl2.lisp
M axioms.lisp
M basis-a.lisp
M basis-b.lisp
M books/centaur/misc/hons-extra.lisp
R books/kestrel/general/alists-tests.lisp
R books/kestrel/general/alists.lisp
M books/kestrel/general/testing.lisp
M books/kestrel/general/top.lisp
A books/kestrel/general/types.lisp
M books/kestrel/soft/implementation.lisp
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/fresh-names-tests.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
A books/kestrel/system/verify-guards-program-tests.acl2
A books/kestrel/system/verify-guards-program-tests.lisp
M books/kestrel/system/verify-guards-program.lisp
M books/kestrel/system/world-queries.lisp
M books/misc/check-acl2-exports.lisp
M books/std/util/defconsts.lisp
M books/system/doc/acl2-doc.lisp
M defthm.lisp
M doc.lisp
M history-management.lisp
M hons-raw.lisp
M hons.lisp
M installation/windows7.html
M interface-raw.lisp
M ld.lisp
M other-events.lisp
M rewrite.lisp
M simplify.lisp
M type-set-b.lisp

Log Message:
-----------
Merge


Commit: bcd05cc98cf7ebb6cdf499b85e6d78fdeaefbd50
https://github.com/acl2/acl2/commit/bcd05cc98cf7ebb6cdf499b85e6d78fdeaefbd50
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2016-07-26 (Tue, 26 Jul 2016)

Changed paths:
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/portcullis/sharp-dot-constants.lisp
M books/projects/x86isa/proofs/factorial/fact-inductive-assertions.lisp
M books/projects/x86isa/proofs/factorial/fact-wormhole-abstraction.lisp
M books/projects/x86isa/proofs/utilities/general-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/programmer-level-mode/programmer-level-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-top.lisp
M books/projects/x86isa/proofs/wordCount/wc.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
A books/projects/x86isa/tools/execution/examples/nop-sequence/acl2-customization.lsp
A books/projects/x86isa/tools/execution/examples/nop-sequence/cert.acl2
A books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp
M books/projects/x86isa/utils/decoding-utilities.lisp
M books/projects/x86isa/utils/utilities.lisp

Log Message:
-----------
Merge pull request #624 from shigoel/cleanup

x86isa: Fixed incorrect counting of the total number of prefixes


Compare: https://github.com/acl2/acl2/compare/49282cfdf598...bcd05cc98cf7

[GitHub]

Branch: refs/heads/master