From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([208.118.235.92]:55699) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1TaPcK-0005Al-OQ for qemu-devel@nongnu.org; Mon, 19 Nov 2012 06:34:23 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1TaPcH-0007aH-MJ for qemu-devel@nongnu.org; Mon, 19 Nov 2012 06:34:20 -0500 Received: from relay0.mail.ox.ac.uk ([129.67.1.161]:58155) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1TaPcH-0007Xm-DM for qemu-devel@nongnu.org; Mon, 19 Nov 2012 06:34:17 -0500 Received: from smtp2.mail.ox.ac.uk ([163.1.2.205]) by relay0.mail.ox.ac.uk with esmtp (Exim 4.75) (envelope-from ) id 1TaPcF-0006zN-0w for qemu-devel@nongnu.org; Mon, 19 Nov 2012 11:34:15 +0000 Received: from mail-ia0-f173.google.com ([209.85.210.173]) by smtp2.mail.ox.ac.uk with esmtpsa (TLSv1:RC4-SHA:128) (Exim 4.69) (envelope-from ) id 1TaPcE-0005Rh-9d for qemu-devel@nongnu.org; Mon, 19 Nov 2012 11:34:15 +0000 Received: by mail-ia0-f173.google.com with SMTP id w21so2013940iac.4 for ; Mon, 19 Nov 2012 03:34:13 -0800 (PST) MIME-Version: 1.0 In-Reply-To: <50A8A1D7.9050309@redhat.com> References: <20121117144135.13758.80176.malonedeb@wampee.canonical.com> <20121117184720.23777.80355.malone@gac.canonical.com> <50A8A1D7.9050309@redhat.com> Date: Mon, 19 Nov 2012 11:34:12 +0000 Message-ID: From: Alex Horn Content-Type: multipart/mixed; boundary=14dae9340db3231ee604ced77ff5 Subject: Re: [Qemu-devel] [Bug 1080086] Re: MC146818 RTC breaks when SET bit in Register B is on. List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , To: Paolo Bonzini Cc: Thomas Melham , qemu-devel@nongnu.org, Daniel Kroening , Bug 1080086 <1080086@bugs.launchpad.net> --14dae9340db3231ee604ced77ff5 Content-Type: text/plain; charset=UTF-8 > [...] the patch is almost good for inclusion. I'd ask for two changes: > 1) please test == 0, not != REG_B_SET; > 2) please leave the fuzzicsng test last I have attached a new patch with the requested changes. This patch also improves the quality of the functional test by checking that RTC_SECONDS is equal (==) to the previously written data provided the SET flag in Register B is still enabled. This is justified by the data sheet which states that an enabled SET bit "stops an existing update" and prevents "a new one from occurring" [1, p. 15]. In contrast, once the SET flag is disabled, the RTC_SECONDS check uses an inequality (>=) as in the original test case. Out of curiosity, does anyone know how long this particular bug has been undetected or how/when it was introduced? This could help me explain to others my research interest in symbolic execution of hardware models and its application in form of automated test generation. Finally, if there is interest to improve the robustness of the RTC model, I could send a patch with several verification conditions (i.e. assertions) which can help to expose these kind of bugs in the RTC hardware model. Recall that most compiler can usually optimize these assertions away unless a developer explicitly enables them. They also serve as unambiguous code documentation. With best regards, Alex [1] http://www.freescale.com/files/microcontrollers/doc/data_sheet/MC146818.pdf On 18 November 2012 08:52, Paolo Bonzini wrote: > Il 17/11/2012 19:47, Alex Horn ha scritto: >> I have attached a patch for the most recent version of the file >> hw/mc146818rtc.c [1]. The patch also features a functional test which >> executes through the QTest framework. >> >> I would appreciate your thoughts on this. >> >> [1] >> http://git.qemu.org/?p=qemu.git;a=blob;f=hw/mc146818rtc.c;h=98839f278d93452d071054e2a017b3d909b45ab2;hb=9cb535fe4ef08b01e583ec955767a0899ff79afe#l563 >> >> ** Patch added: "register_b_set_flag.patch" >> https://bugs.launchpad.net/qemu/+bug/1080086/+attachment/3436808/+files/register_b_set_flag.patch >> > > Hi Alex, the patch is almost good for inclusion. I'd ask for two > changes: 1) please test == 0, not != REG_B_SET; 2) please leave the > fuzzing test last, because it may leave some registers in an undefined > state. > > Paolo --14dae9340db3231ee604ced77ff5 Content-Type: application/octet-stream; name="register_b_set_flag_v2.patch" Content-Disposition: attachment; filename="register_b_set_flag_v2.patch" Content-Transfer-Encoding: base64 X-Attachment-Id: f_h9phulco0 ZGlmZiAtLWdpdCBhL2h3L21jMTQ2ODE4cnRjLmMgYi9ody9tYzE0NjgxOHJ0Yy5jCmluZGV4IDk4 ODM5ZjIuLjc5YzhhYTYgMTAwNjQ0Ci0tLSBhL2h3L21jMTQ2ODE4cnRjLmMKKysrIGIvaHcvbWMx NDY4MThydGMuYwpAQCAtNTY5LDcgKzU2OSwxMSBAQCBzdGF0aWMgdm9pZCBydGNfdXBkYXRlX3Rp bWUoUlRDU3RhdGUgKnMpCiAgICAgZ3Vlc3RfbnNlYyA9IGdldF9ndWVzdF9ydGNfbnMocyk7CiAg ICAgZ3Vlc3Rfc2VjID0gZ3Vlc3RfbnNlYyAvIE5TRUNfUEVSX1NFQzsKICAgICBnbXRpbWVfcigm Z3Vlc3Rfc2VjLCAmcmV0KTsKLSAgICBydGNfc2V0X2Ntb3MocywgJnJldCk7CisKKyAgICAvKiBJ cyBTRVQgZmxhZyBvZiBSZWdpc3RlciBCIGRpc2FibGVkPyAqLworICAgIGlmICgocy0+Y21vc19k YXRhW1JUQ19SRUdfQl0gJiBSRUdfQl9TRVQpID09IDApIHsKKyAgICAgICAgcnRjX3NldF9jbW9z KHMsICZyZXQpOworICAgIH0KIH0KIAogc3RhdGljIGludCB1cGRhdGVfaW5fcHJvZ3Jlc3MoUlRD U3RhdGUgKnMpCmRpZmYgLS1naXQgYS90ZXN0cy9ydGMtdGVzdC5jIGIvdGVzdHMvcnRjLXRlc3Qu YwppbmRleCA3ZmRjOTRhLi4wMmVkYmY1IDEwMDY0NAotLS0gYS90ZXN0cy9ydGMtdGVzdC5jCisr KyBiL3Rlc3RzL3J0Yy10ZXN0LmMKQEAgLTMyNyw2ICszMjcsNDUgQEAgc3RhdGljIHZvaWQgZnV6 el9yZWdpc3RlcnModm9pZCkKICAgICB9CiB9CiAKK3N0YXRpYyB2b2lkIHJlZ2lzdGVyX2Jfc2V0 X2ZsYWcodm9pZCkKK3sKKyAgICAvKiBFbmFibGUgYmluYXJ5LWNvZGVkIGRlY2ltYWwgKEJDRCkg bW9kZSBhbmQgU0VUIGZsYWcgaW4gUmVnaXN0ZXIgQiovCisgICAgY21vc193cml0ZShSVENfUkVH X0IsIChjbW9zX3JlYWQoUlRDX1JFR19CKSAmIH5SRUdfQl9ETSkgfCBSRUdfQl9TRVQpOworCisg ICAgY21vc193cml0ZShSVENfUkVHX0EsIDB4NzYpOworICAgIGNtb3Nfd3JpdGUoUlRDX1lFQVIs IDB4MTEpOworICAgIGNtb3Nfd3JpdGUoUlRDX0NFTlRVUlksIDB4MjApOworICAgIGNtb3Nfd3Jp dGUoUlRDX01PTlRILCAweDAyKTsKKyAgICBjbW9zX3dyaXRlKFJUQ19EQVlfT0ZfTU9OVEgsIDB4 MDIpOworICAgIGNtb3Nfd3JpdGUoUlRDX0hPVVJTLCAweDAyKTsKKyAgICBjbW9zX3dyaXRlKFJU Q19NSU5VVEVTLCAweDA0KTsKKyAgICBjbW9zX3dyaXRlKFJUQ19TRUNPTkRTLCAweDU4KTsKKyAg ICBjbW9zX3dyaXRlKFJUQ19SRUdfQSwgMHgyNik7CisKKyAgICAvKiBTaW5jZSBTRVQgZmxhZyBp cyBzdGlsbCBlbmFibGVkLCB0aGVzZSBhcmUgZXF1YWxpdHkgY2hlY2tzLiAqLworICAgIGdfYXNz ZXJ0X2NtcGludChjbW9zX3JlYWQoUlRDX0hPVVJTKSwgPT0sIDB4MDIpOworICAgIGdfYXNzZXJ0 X2NtcGludChjbW9zX3JlYWQoUlRDX01JTlVURVMpLCA9PSwgMHgwNCk7CisgICAgZ19hc3NlcnRf Y21waW50KGNtb3NfcmVhZChSVENfU0VDT05EUyksID09LCAweDU4KTsKKyAgICBnX2Fzc2VydF9j bXBpbnQoY21vc19yZWFkKFJUQ19EQVlfT0ZfTU9OVEgpLCA9PSwgMHgwMik7CisgICAgZ19hc3Nl cnRfY21waW50KGNtb3NfcmVhZChSVENfTU9OVEgpLCA9PSwgMHgwMik7CisgICAgZ19hc3NlcnRf Y21waW50KGNtb3NfcmVhZChSVENfWUVBUiksID09LCAweDExKTsKKyAgICBnX2Fzc2VydF9jbXBp bnQoY21vc19yZWFkKFJUQ19DRU5UVVJZKSwgPT0sIDB4MjApOworCisgICAgLyogRGlzYWJsZSBT RVQgZmxhZyBpbiBSZWdpc3RlciBCICovCisgICAgY21vc193cml0ZShSVENfUkVHX0IsIGNtb3Nf cmVhZChSVENfUkVHX0IpICYgflJFR19CX1NFVCk7CisKKyAgICBnX2Fzc2VydF9jbXBpbnQoY21v c19yZWFkKFJUQ19IT1VSUyksID09LCAweDAyKTsKKyAgICBnX2Fzc2VydF9jbXBpbnQoY21vc19y ZWFkKFJUQ19NSU5VVEVTKSwgPT0sIDB4MDQpOworCisgICAgLyogU2luY2UgU0VUIGZsYWcgaXMg ZGlzYWJsZWQsIHRoaXMgaXMgYW4gaW5lcXVhbGl0eSBjaGVjay4KKyAgICAgKiBXZSAocmVhc29u YWJseSkgYXNzdW1lIHRoYXQgbm8gKHNleGFnZXNpbWFsKSBvdmVyZmxvdyBvY2N1cnMuICovCisg ICAgZ19hc3NlcnRfY21waW50KGNtb3NfcmVhZChSVENfU0VDT05EUyksID49LCAweDU4KTsKKyAg ICBnX2Fzc2VydF9jbXBpbnQoY21vc19yZWFkKFJUQ19EQVlfT0ZfTU9OVEgpLCA9PSwgMHgwMik7 CisgICAgZ19hc3NlcnRfY21waW50KGNtb3NfcmVhZChSVENfTU9OVEgpLCA9PSwgMHgwMik7Cisg ICAgZ19hc3NlcnRfY21waW50KGNtb3NfcmVhZChSVENfWUVBUiksID09LCAweDExKTsKKyAgICBn X2Fzc2VydF9jbXBpbnQoY21vc19yZWFkKFJUQ19DRU5UVVJZKSwgPT0sIDB4MjApOworfQorCiBp bnQgbWFpbihpbnQgYXJnYywgY2hhciAqKmFyZ3YpCiB7CiAgICAgUVRlc3RTdGF0ZSAqcyA9IE5V TEw7CkBAIC0zNDIsNiArMzgxLDcgQEAgaW50IG1haW4oaW50IGFyZ2MsIGNoYXIgKiphcmd2KQog ICAgIHF0ZXN0X2FkZF9mdW5jKCIvcnRjL2FsYXJtLXRpbWUiLCBhbGFybV90aW1lKTsKICAgICBx dGVzdF9hZGRfZnVuYygiL3J0Yy9zZXQteWVhci8yMHh4Iiwgc2V0X3llYXJfMjB4eCk7CiAgICAg cXRlc3RfYWRkX2Z1bmMoIi9ydGMvc2V0LXllYXIvMTk4MCIsIHNldF95ZWFyXzE5ODApOworICAg IHF0ZXN0X2FkZF9mdW5jKCIvcnRjL3JlZ2lzdGVyX2Jfc2V0X2ZsYWciLCByZWdpc3Rlcl9iX3Nl dF9mbGFnKTsKICAgICBxdGVzdF9hZGRfZnVuYygiL3J0Yy9mdXp6LXJlZ2lzdGVycyIsIGZ1enpf cmVnaXN0ZXJzKTsKICAgICByZXQgPSBnX3Rlc3RfcnVuKCk7CiAK --14dae9340db3231ee604ced77ff5--