<*>= [D->] procedure unsignedval(f, val) constant(val) = 0 | return Cshift(val, "left", f.lo) end procedure signedval(f, val) constant(val) = 0 | return Cshift(Cmask(val, fwidth(f)), "left", f.lo) end
Definessignedval
,unsignedval
(links are to index).
Signed and unsigned values are stored in fieldval
<*>+= [<-D->] procedure init_tests() <init> return end global fieldval
Definesfieldval
,init_tests
(links are to index).
<init>= (<-U) [D->] fieldvals := table() fieldvals["field"] := unsignedval; fieldvals["extended"] := signedval
Size testing is straightforward but tedious. Constants, which usually come from constraints in disjuncts, are tested at generation time. Unsigned values require a single test; signed values require two (i.e. a range test).
<*>+= [<-D->] procedure unsignedtest(outfile, f, value, inputs) bits := fwidth(f) bits >= f.class.size | if v := constant(value) then v < 2^bits | error("spec forces ", f.name, " = ", v, ", which won't fit in ", bits, " bits") else { value := eqntoC(value, inputs, 1) write(outfile, indent(), "if ((unsigned)(", value, ") > ", mask(bits), ")\n", indent(2), "(*fail)(", image(f.name || " = %d won't fit in " || bits || " bits"), ", ", value, ");") } return end procedure unsignedcond(f, value, inputs) bits := fwidth(f) value := eqntoC(value, inputs, 1) return "((unsigned)(" || value || ") <= " || mask(bits) || ")" end
Definesunsignedcond
,unsignedtest
(links are to index).
<*>+= [<-D->] procedure signedtest(outfile, f, value, inputs) bits := fwidth(f) bits >= f.class.size | if v := constant(value) then -(2^(bits-1)) <= v < 2^(bits-1) | error("spec forces ", f.name, " = ", v, ", which won't fit in ", bits, " signed bits") else { value := eqntoC(value, inputs, 1) write(outfile, indent(), "if ((int)(", value, ") < -", tworaised(bits-1), " ||\n", indent(2), "(int)(", value, ") >= ", tworaised(bits-1), ")\n", indent(2), "(*fail)(", image(f.name || " = %d won't fit in "|| bits || " signed bits"), ", ", value, ");") } return end procedure signedcond(f, value, inputs) bits := fwidth(f) value := eqntoC(value, inputs, 1) return "((int)(" || value || ") >= -" || tworaised(bits-1) || " && \n" || "(int)(" || value || ") < " || tworaised(bits-1) || ")" end
Definessignedcond
,signedtest
(links are to index).
<*>+= [<-D->] global fieldconds, fieldtests
Definesfieldconds
,fieldtests
(links are to index).
<init>+= (<-U) [<-D] every fieldconds | fieldtests := table() fieldconds["field"] := unsignedcond; fieldconds["extended"] := signedcond fieldtests["field"] := unsignedtest; fieldtests["extended"] := signedtest
testcondition
generates code to test an arbitrary condition generated by the solver.
<*>+= [<-D->] procedure testcondition(outfile, cond, inputs) write(outfile, indent(), "if (!(", eqntoC(cond, inputs, 1), "))\n", indent(2), "(*fail)(\"Condition ", expimage(cond), " not satisified.\");") end
Definestestcondition
(links are to index).
These functions compute the constants against which values are tested.
<*>+= [<-D->] global hex_prefix procedure mask(bits) return hex_prefix || ((0 ~= (2^(bits % 4) - 1)) | "") || repl("f", bits / 4) end procedure tworaised(bits) return hex_prefix || (2^(bits % 4)) || repl("0", bits / 4) end
Defineshex_prefix
,mask
,tworaised
(links are to index).
<*>+= [<-D] procedure indent(n) initial /sindent := 2 return repl(" ", sindent + (\n | 0)) end
Definesindent
(links are to index).