{"push_id":957789601,"size":1,"distinct_size":1,"ref":"refs/heads/pagingUtils","head":"0a96c020c538b6c14042e4192a355ce7452b34de","before":"ae407653fb2c8a96fe0503d30bf7ee3fda2ac435","commits":[{"sha":"0a96c020c538b6c14042e4192a355ce7452b34de","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"x86isa: Rewrite all rm*/wm* calls to rb/wb, when possible, in the system-level mode\n\nThe x86isa books provide various top-level linear memory read (rm08\nthrough rm128) and write (wm08 through wm128,\nwrite-canonical-address-to-memory) functions. During reasoning, these\nfunctions simply open up to rb and wb in the programmer-level mode,\nthus giving us a canonical way of looking at memory accesses and\nupdates. However, in the system-level mode, it's not so simple because\nwell-formedness of paging structures should also be considered.\n\nThe motivation for this change is to make reasoning about memory in\nsystem-level mode close to what it is in the programmer-level\nmode. The new rules that rewrite rm*/wm* to rb/wb in the system-level\nmode have the well-formedness of the paging structures as the\npre-condition. We force the hypotheses of these rules because we will\nalmost always be reasoning in a state where the paging structures are\nwell-formed.","distinct":true,"url":"https://api.github.com/repos/shigoel/acl2/commits/0a96c020c538b6c14042e4192a355ce7452b34de"}]}