Compiler Bug: At this point in the compilation typechecking should not infer new types anymore, but it did.

[fruffy]

Hello again,
after commit 1159ced we encounter the compiler bug in the title for specific programs. I attached an example.
The exact command is p4c/build/p4c -v bad_type_checking.p4.
bad_type_checking.p4.txt

[mihaibudiu]

We should only add the numbers if they have the same type.

[jafingerhut]

A question about this strength reduction transformation that sometimes changes ((a >> b) >> c) to (a>> (b + c)). Could the transformation be done if the type of the expression (b+c) is bit<W>, and the addition of (b+c) wraps around? It seems that the original ((a >> b) >> c) might have a correct result of 0, whereas if (b+c) wrapped around to 1, (a >> (b+c)) could be a non-0 (a >> 1) value.

[mihaibudiu]

Yes, with the current code this can happen.
We could also only do it if both b and c are InfInt.

[mihaibudiu]

Please file another issue.

[mihaibudiu]

Or perhaps let's fix it in this PR, just request changes.

[mihaibudiu]

@fruffy can you catch this overflow bug?

[fruffy]

Yes, I tested it on the branch. I attached a sample program and stf file.
The overflow causes the shift to turn to zero.
addition_overflow.p4.txt
addition_overflow.stf.txt

[fruffy]

Output of the tool once it detected a difference is something like this:

FrontEnd_13_BindTypeVariables:
mk_Parsed_packet(
	mk_ethernet_t(
		dstAddr(eth(hdr(ingress_0))),
		srcAddr(eth(hdr(ingress_0))),
		etherType(eth(hdr(ingress_0)))),
	 mk_H(
		 0, <--- value of hdr.h.a
		 b(h(hdr(ingress_0))))
	)
)

FrontEnd_17_StrengthReduction:
mk_Parsed_packet(
	mk_ethernet_t(
		dstAddr(eth(hdr(ingress_0))),
		srcAddr(eth(hdr(ingress_0))),
		etherType(eth(hdr(ingress_0)))),
	 mk_H(
		 1, <--- value of hdr.h.a
		 b(h(hdr(ingress_0))))
	)
)

So the value of hdr.h.a after running through the control pipeline is 1 instead of 0.