Miscellaneous code-generation procedures

Value computation and shifting is straightforward; the only detail is that signed values have to be masked to remove the high-order (sign) bits. 
<*>= [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
Defines signedval, unsignedval (links are to index).

Signed and unsigned values are stored in fieldval 

<*>+= [<-D->]
procedure init_tests()
  <init>
  return
end
global fieldval
Defines fieldval, 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
Defines unsignedcond, 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
Defines signedcond, signedtest (links are to index).

<*>+= [<-D->]
global fieldconds, fieldtests
Defines fieldconds, 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
Defines testcondition (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
Defines hex_prefix, mask, tworaised (links are to index).

<*>+= [<-D]
procedure indent(n)
    initial /sindent := 2
    return repl(" ", sindent + (\n | 0))
end
Defines indent (links are to index).