Re: [Qemu-devel] [Bug 1080086] Re: MC146818 RTC breaks when SET bit in Register B is on.

[Alex Horn <alex.horn@cs.ox.ac.uk>]

[-- Attachment #1: Type: text/plain, Size: 2336 bytes --]

> [...] 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 <pbonzini@redhat.com> 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

[-- Attachment #2: register_b_set_flag_v2.patch --]
[-- Type: application/octet-stream, Size: 2775 bytes --]

diff --git a/hw/mc146818rtc.c b/hw/mc146818rtc.c
index 98839f2..79c8aa6 100644
--- a/hw/mc146818rtc.c
+++ b/hw/mc146818rtc.c
@@ -569,7 +569,11 @@ static void rtc_update_time(RTCState *s)
     guest_nsec = get_guest_rtc_ns(s);
     guest_sec = guest_nsec / NSEC_PER_SEC;
     gmtime_r(&guest_sec, &ret);
-    rtc_set_cmos(s, &ret);
+
+    /* Is SET flag of Register B disabled? */
+    if ((s->cmos_data[RTC_REG_B] & REG_B_SET) == 0) {
+        rtc_set_cmos(s, &ret);
+    }
 }
 
 static int update_in_progress(RTCState *s)
diff --git a/tests/rtc-test.c b/tests/rtc-test.c
index 7fdc94a..02edbf5 100644
--- a/tests/rtc-test.c
+++ b/tests/rtc-test.c
@@ -327,6 +327,45 @@ static void fuzz_registers(void)
     }
 }
 
+static void register_b_set_flag(void)
+{
+    /* Enable binary-coded decimal (BCD) mode and SET flag in Register B*/
+    cmos_write(RTC_REG_B, (cmos_read(RTC_REG_B) & ~REG_B_DM) | REG_B_SET);
+
+    cmos_write(RTC_REG_A, 0x76);
+    cmos_write(RTC_YEAR, 0x11);
+    cmos_write(RTC_CENTURY, 0x20);
+    cmos_write(RTC_MONTH, 0x02);
+    cmos_write(RTC_DAY_OF_MONTH, 0x02);
+    cmos_write(RTC_HOURS, 0x02);
+    cmos_write(RTC_MINUTES, 0x04);
+    cmos_write(RTC_SECONDS, 0x58);
+    cmos_write(RTC_REG_A, 0x26);
+
+    /* Since SET flag is still enabled, these are equality checks. */
+    g_assert_cmpint(cmos_read(RTC_HOURS), ==, 0x02);
+    g_assert_cmpint(cmos_read(RTC_MINUTES), ==, 0x04);
+    g_assert_cmpint(cmos_read(RTC_SECONDS), ==, 0x58);
+    g_assert_cmpint(cmos_read(RTC_DAY_OF_MONTH), ==, 0x02);
+    g_assert_cmpint(cmos_read(RTC_MONTH), ==, 0x02);
+    g_assert_cmpint(cmos_read(RTC_YEAR), ==, 0x11);
+    g_assert_cmpint(cmos_read(RTC_CENTURY), ==, 0x20);
+
+    /* Disable SET flag in Register B */
+    cmos_write(RTC_REG_B, cmos_read(RTC_REG_B) & ~REG_B_SET);
+
+    g_assert_cmpint(cmos_read(RTC_HOURS), ==, 0x02);
+    g_assert_cmpint(cmos_read(RTC_MINUTES), ==, 0x04);
+
+    /* Since SET flag is disabled, this is an inequality check.
+     * We (reasonably) assume that no (sexagesimal) overflow occurs. */
+    g_assert_cmpint(cmos_read(RTC_SECONDS), >=, 0x58);
+    g_assert_cmpint(cmos_read(RTC_DAY_OF_MONTH), ==, 0x02);
+    g_assert_cmpint(cmos_read(RTC_MONTH), ==, 0x02);
+    g_assert_cmpint(cmos_read(RTC_YEAR), ==, 0x11);
+    g_assert_cmpint(cmos_read(RTC_CENTURY), ==, 0x20);
+}
+
 int main(int argc, char **argv)
 {
     QTestState *s = NULL;
@@ -342,6 +381,7 @@ int main(int argc, char **argv)
     qtest_add_func("/rtc/alarm-time", alarm_time);
     qtest_add_func("/rtc/set-year/20xx", set_year_20xx);
     qtest_add_func("/rtc/set-year/1980", set_year_1980);
+    qtest_add_func("/rtc/register_b_set_flag", register_b_set_flag);
     qtest_add_func("/rtc/fuzz-registers", fuzz_registers);
     ret = g_test_run();