Fix for printf modifiers (#185)

* added unit tests for printf %x format modifier

* slightly modified %d format specifier test case to cover precision format specifier

* modified handling of %d specifer to handle precision, added propert handling of %x format specifier

* adjusted spacing

* changed the flawed merge of Train's fix

* fixed handling of octal print specifier

* fixed handling of octal print specifier

* added a test case for unsigned printf format specifiers

* added printf format specifier handling for unsigned

* refactored the common code for width and precision specifiers; added handling for 0 value / 0 precision

* fixed default precision semantics for d,i,x,X,o,u

* fixed a bug due to an evaluation order

* fixed code alignment

semantics/library/stdio.k

@@ -79,7 +79,7 @@ module LIBC-STDIO
           => Int2String(B) +String " @ "
           +String "auto(" +String Int2String(Th) +String ")"
           [structural]
- 
+
 
      rule [pointerToString-done]:
           pointerToString(NullPointer) => "NullPointer"
@@ -370,9 +370,20 @@ module LIBC-STDIO
 
      rule <k> formatter-aux(_) ...</k>
           <format> ListItem(C:String) ...</format>
+          <format-precision> P:String </format-precision>
+          <format-state> "%." => "%" </format-state>
+          requires P =/=K ""
+               andBool (ordChar(C) <Int ordChar("0")
+               orBool ordChar(C) >Int ordChar("9"))
+          [structural]
+
+     rule <k> formatter-aux(_) ...</k>
+          <format> ListItem(C:String) ...</format>
+          <format-precision> P:String => "0" </format-precision>
           <format-state> "%." => "%" </format-state>
-          requires ordChar(C) <Int ordChar("0")
-               orBool ordChar(C) >Int ordChar("9")
+          requires P ==K ""
+               andBool (ordChar(C) <Int ordChar("0")
+               orBool ordChar(C) >Int ordChar("9"))
           [structural]
 
 
@@ -387,11 +398,23 @@ module LIBC-STDIO
      characters.}
      \end{description}
      */
+
+     rule <k> formatter-aux(_) ...</k>
+          <format> ListItem(S:String) ...</format>
+          <format-precision> P:String => "1" </format-precision>
+          <format-state> "%" </format-state>
+          requires P ==K ""
+               andBool (S ==String "d" orBool S ==String "i" orBool S ==String "u"
+                        orBool S ==String "x" orBool S ==String "X"
+                        orBool S ==String "o")
+          [structural]
+
      rule [format-%d-start]:
           <k> formatter-aux(Args:List) => formatter-next(Args) ...</k>
           <format> ListItem(S:String) => .List ...</format>
+          <format-precision> P:String </format-precision>
           <format-state> "%" => "%d" </format-state>
-          requires S ==String "d" orBool S ==String "i"
+          requires P =/=K "" andBool S ==String "d" orBool S ==String "i"
           [structural]
 
      rule <k> formatter-aux(_) ...</k>
@@ -404,11 +427,15 @@ module LIBC-STDIO
 
      rule <k> formatter-aux(_) ...</k>
           <format-arg> D:Int => .K </format-arg>
+          <format-precision> P:String </format-precision>
           <format-pad-zero> Z:Bool </format-pad-zero>
           <format-field-width> W:String </format-field-width>
           <format-result>...
-               .List => ListItem(pad(Int2String(D), String2Int(W),
-                  #if Z #then "0" #else " " #fi:>String))
+               .List => ListItem(
+                        formatPrecisionWidth(Int2String(D:Int),
+                                             String2Int(P),
+                                             Z,
+                                             String2Int(W)))
           </format-result>
           <format-state> "%d" => "reset" </format-state>
           [structural]
@@ -430,52 +457,88 @@ module LIBC-STDIO
      rule [format-%o-start]:
           <k> formatter-aux(Args:List) => formatter-next(Args) ...</k>
           <format> ListItem("o") => .List ...</format>
+          <format-precision> P:String </format-precision>
           <format-state> "%" => "%o" </format-state>
+          requires P =/=K ""
           [structural]
      rule [format-%o]:
           <k> formatter-aux(_) ...</k>
           <format-arg> D:Int => .K </format-arg>
+          <format-precision> P:String </format-precision>
+          <format-pad-zero> Z:Bool </format-pad-zero>
+          <format-field-width> W:String </format-field-width>
           <format-result>...
-               .List => ListItem(Base2String(D:Int, 8))
+               .List => ListItem(
+                        formatPrecisionWidth(Base2String(D:Int, 8),
+                                             String2Int(P),
+                                             Z,
+                                             String2Int(W)))
           </format-result>
           <format-state> "%o" => "reset" </format-state>
           [structural]
      rule [format-%u-start]:
           <k> formatter-aux(Args:List) => formatter-next(Args) ...</k>
           <format> ListItem("u") => .List ...</format>
+          <format-precision> P:String </format-precision>
           <format-state> "%" => "%u" </format-state>
+          requires P =/=K ""
           [structural]
      rule [format-%u]:
           <k> formatter-aux(_) ...</k>
           <format-arg> D:Int => .K </format-arg>
+          <format-precision> P:String </format-precision>
+          <format-pad-zero> Z:Bool </format-pad-zero>
+          <format-field-width> W:String </format-field-width>
           <format-result>...
-               .List => ListItem(Int2String(D:Int))
+               .List => ListItem(
+                        formatPrecisionWidth(Int2String(D:Int),
+                                             String2Int(P),
+                                             Z,
+                                             String2Int(W)))
           </format-result>
           <format-state> "%u" => "reset" </format-state>
           [structural]
      rule [format-%x-start]:
           <k> formatter-aux(Args:List) => formatter-next(Args) ...</k>
           <format> ListItem("x") => .List ...</format>
+          <format-precision> P:String </format-precision>
           <format-state> "%" => "%x" </format-state>
+          requires P =/=K ""
           [structural]
      rule [format-%x]:
           <k> formatter-aux(_) ...</k>
           <format-arg> D:Int => .K </format-arg>
+          <format-precision> P:String </format-precision>
+          <format-pad-zero> Z:Bool </format-pad-zero>
+          <format-field-width> W:String </format-field-width>
           <format-result>...
-               .List => ListItem(Base2String(D:Int, 16))
+               .List => ListItem(
+                        formatPrecisionWidth(Base2String(D:Int, 16),
+                                             String2Int(P),
+                                             Z,
+                                             String2Int(W)))
           </format-result>
           <format-state> "%x" => "reset" </format-state>
           [structural]
      rule [format-%X-start]:
           <k> formatter-aux(Args:List) => formatter-next(Args) ...</k>
           <format> ListItem("X") => .List ...</format>
+          <format-precision> P:String </format-precision>
           <format-state> "%" => "%X" </format-state>
+          requires P =/=K ""
           [structural]
      rule [format-%X]:
           <k> formatter-aux(_) ...</k>
           <format-arg> D:Int => .K </format-arg>
+          <format-precision> P:String </format-precision>
+          <format-pad-zero> Z:Bool </format-pad-zero>
+          <format-field-width> W:String </format-field-width>
           <format-result>...
-               .List => ListItem(toUpperCase(Base2String(D:Int, 16)))
+               .List => ListItem(
+                        formatPrecisionWidth(toUpperCase(Base2String(D:Int, 16)),
+                                             String2Int(P),
+                                             Z,
+                                             String2Int(W)))
           </format-result>
           <format-state> "%X" => "reset" </format-state>
           [structural]
@@ -891,6 +954,27 @@ module LIBC-STDIO
      rule pad'(X::String, W::Int, _) => X
           requires W ==Int 0
 
+    syntax String ::= "formatPrecisionWidth" "(" String "," Int "," Bool "," Int ")" [function]
+                    | "formatPrecisionWidth'" "(" String "," Int "," Bool "," Int ")" [function]
+                    | "formatPrecisionWidth''" "(" String "," Int "," Int "," String ")" [function]
+
+    rule formatPrecisionWidth(V::String, P::Int, Z::Bool, W::Int)
+         => formatPrecisionWidth'(V, P, Z, W)
+         requires V =/=String "0" orBool P =/=Int 0
+    rule formatPrecisionWidth(V::String, P::Int, Z::Bool, W::Int)
+         => formatPrecisionWidth'("", P, Z, W)
+         requires V ==String "0" andBool P ==Int 0
+
+    rule formatPrecisionWidth'(V::String, P::Int, Z::Bool, W::Int)
+         => formatPrecisionWidth''(V, P, W, "0")
+         requires Z ==Bool true
+    rule formatPrecisionWidth'(V::String, P::Int, Z::Bool, W::Int)
+         => formatPrecisionWidth''(V, P, W, " ")
+         requires Z ==Bool false
+
+    rule formatPrecisionWidth''(V::String, P::Int, W::Int, PZ::String)
+         => pad(pad(V, P, "0"), W, PZ)
+
      syntax Int ::= signInt(Int) [function]
      rule signInt(X::Int) => X /Int absInt(X)
 

tests/unit-pass/printf-field-width-hex.c

@@ -0,0 +1,16 @@
+#include <stdio.h>
+
+
+int main() {
+      printf("------------------------\n");
+			unsigned int c = 12;
+      printf("Hex 0: |%.x|\n", (unsigned)0);
+      printf("Hex 1: |%x|\n", c);
+      printf("Hex 2: |%0x|\n", c);
+      printf("Hex 3: |%02x|\n", c);
+      printf("Hex 3: |%-2x|\n", c);
+      printf("Hex 4: |%15x|\n", c);
+      printf("Hex 5: |%15.4x|\n", c);
+      printf("Hex 6: |%015x|\n", c);
+      printf("------------------------\n");
+}

tests/unit-pass/printf-field-width-oct.c

@@ -0,0 +1,16 @@
+#include <stdio.h>
+
+
+int main() {
+      printf("------------------------\n");
+			int c = 42;
+      printf("Oct 1: |%.o|\n", 0);
+      printf("Oct 1: |%o|\n", c);
+      printf("Oct 2: |%0o|\n", c);
+      printf("Oct 4: |%-2o|\n", c);
+      printf("Oct 3: |%08o|\n", c);
+      printf("Oct 5: |%15o|\n", c);
+      printf("Oct 6: |%15.4o|\n", c);
+      printf("Oct 7: |%015o|\n", c);
+      printf("------------------------\n");
+}

tests/unit-pass/printf-field-width-unsigned.c

@@ -0,0 +1,18 @@
+#include <stdio.h>
+
+
+int main() {
+      printf("------------------------\n");
+			unsigned int c = 7;
+      printf("Unsigned 1: |%.u|\n", (unsigned)42);
+      printf("Unsigned 2: |%u|\n", c);
+      printf("Unsigned 3: |%0u|\n", c);
+      printf("Unsigned 4: |%04u|\n", c);
+      printf("Unsigned 5: |%-4u|\n", c);
+      printf("Unsigned 6: |%15u|\n", c);
+      printf("Unsigned 7: |%15.4u|\n", c);
+      printf("Unsigned 8: |%015u|\n", c);
+      printf("Unsigned 9: |%15.0u|\n", (unsigned)0);
+      printf("Unsigned 9: |%15.2u|\n", (unsigned)0);
+      printf("------------------------\n");
+}

tests/unit-pass/printf-field-width.c

@@ -3,14 +3,18 @@
 
 int main() {
       printf("------------------------\n");
-      printf("Int 1: |%d|\n", 123);
-      printf("Int 2: |%0d|\n", 123);
-      printf("Int 3: |%15d|\n", 123);
-      printf("Int 4: |%-15d|\n", 123);
-      printf("Int 5: |%15.2d|\n", 123);
-      printf("Int 6: |%-15.2d|\n", 123);
-      printf("Int 7: |%015d|\n", 123);
-      printf("Int 8: |%0-15d|\n", 123);
-      printf("Int 9: |%0-15.2d|\n", 123);
+      printf("Int -1: |%.d|\n", 0);
+      printf("Int  0: |%.d|\n", 42);
+      printf("Int  1: |%d|\n", 123);
+      printf("Int  2: |%0d|\n", 123);
+      printf("Int  3: |%15d|\n", 123);
+      printf("Int  4: |%-15d|\n", 123);
+      printf("Int  5: |%15.5d|\n", 123);
+      printf("Int  6: |%-15.2d|\n", 123);
+      printf("Int  7: |%015d|\n", 123);
+//      printf("Int  8: |%015.0d|\n", 123);
+      printf("Int  9: |%15.0d|\n", 0);
+//      printf("Int 10: |%015.4d|\n", 0);
+      printf("Int 11: |%0-15d|\n", 123);
       printf("------------------------\n");
 }