[acl2/acl2] 5ab080: x86isa: Added functions to read/write 6 and 10 byt...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 5ab080ddfc25625c54c0c1af524348f4bb18b745
https://github.com/acl2/acl2/commit/5ab080ddfc25625c54c0c1af524348f4bb18b745
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-08-08 (Mon, 08 Aug 2016)

Changed paths:
M books/projects/x86isa/machine/guard-helpers.lisp
M books/projects/x86isa/machine/instructions/x86-jump-and-loop-instructions.lisp
M books/projects/x86isa/machine/x86-programmer-level-memory.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp

Log Message:
-----------
x86isa: Added functions to read/write 6 and 10 bytes of memory.

Thanks to Dmitry Nadezhin for the suggestion so that we can prove the
equality of rm/wm-size functions to rb/wb respectively, and also for
pointing out a typo in the guards of wim-size.


Commit: d9221b72a8d3c4433910d43e1c2158fab2a9ed0a
https://github.com/acl2/acl2/commit/d9221b72a8d3c4433910d43e1c2158fab2a9ed0a
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-08-08 (Mon, 08 Aug 2016)

Changed paths:
M books/projects/x86isa/machine/instructions/fp/x86-fp-arithmetic-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-bitscan-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-convert-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-logical-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mov-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mxcsr-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-shuffle-and-unpack-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-simd-integer-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-arith-and-logic-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-bit-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-conditional-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-divide-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-exchange-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-jump-and-loop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-move-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-multiply-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-push-and-pop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-rotate-and-shift-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-segmentation-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-subroutine-instructions.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp

Log Message:
-----------
x86isa: Added a memory-ptr? arg to
x86-operand-from-modr/m-and-sib-bytes and x86-operand-to-reg/mem.

This argument helps in determining the natural boundary for memory
pointer operands of size 4 (i.e., m16:16) --- in this case, the
boundary is an even address, and not an address divisible by 4.


Commit: 15d1fda3d93933f712a1b275b24dd3dea631c7a9
https://github.com/acl2/acl2/commit/15d1fda3d93933f712a1b275b24dd3dea631c7a9
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp

Log Message:
-----------
x86isa: Added the theorem that the final value of rax for zeroCopy == 1.


Commit: 93f9edd18b3ba95e585d7704f2fbd45eb1430953
https://github.com/acl2/acl2/commit/93f9edd18b3ba95e585d7704f2fbd45eb1430953
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M books/centaur/bitops/merge.lisp
A books/centaur/bitops/width-find-rule.lisp
M books/centaur/sv/svex/rewrite-rules.lisp
M books/centaur/sv/svtv/process.lisp
M books/centaur/vl/server/public/describe.js
M books/projects/x86isa/machine/x86-top-level-memory.lisp

Log Message:
-----------
x86isa: Fix conflicts.


Commit: e7f7e45fa5833af51e01d6dcb5b84a78e0278039
https://github.com/acl2/acl2/commit/e7f7e45fa5833af51e01d6dcb5b84a78e0278039
Author: David L. Rager <rag...@gmail.com>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M books/projects/x86isa/machine/guard-helpers.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-arithmetic-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-bitscan-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-convert-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-logical-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mov-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mxcsr-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-shuffle-and-unpack-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-simd-integer-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-arith-and-logic-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-bit-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-conditional-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-divide-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-exchange-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-jump-and-loop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-move-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-multiply-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-push-and-pop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-rotate-and-shift-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-segmentation-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-subroutine-instructions.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-programmer-level-memory.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp

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

Added support for checking alignment of memory operands of the form m<x>:<y>


Compare: https://github.com/acl2/acl2/compare/b4858079829f...e7f7e45fa583

[GitHub]

Branch: refs/heads/testing