in impl/src/tooling/verifier/smtdecls_emitter.ts [857:1160]
private initializeSMTAssembly(assembly: MIRAssembly, entrypoint: MIRInvokeKey, callsafety: Map<MIRInvokeKey, { safe: boolean, trgt: boolean }>) {
const cinits = [...assembly.constantDecls].map((cdecl) => cdecl[1].ivalue);
const apicons: MIRInvokeKey[] = [];
[...assembly.entityDecls].forEach((edecl) => {
if(edecl[1] instanceof MIRConstructableEntityTypeDecl && this.temitter.assembly.subtypeOf(this.temitter.getMIRType(edecl[0]), this.temitter.getMIRType("NSCore::APIType")) && edecl[1].usingcons !== undefined) {
apicons.push(edecl[1].usingcons);
}
else if(edecl[1] instanceof MIRObjectEntityTypeDecl && this.temitter.assembly.subtypeOf(this.temitter.getMIRType(edecl[0]), this.temitter.getMIRType("NSCore::APIType")) && edecl[1].consfunc !== undefined) {
apicons.push(edecl[1].consfunc);
}
else {
//nothing needs to be done
}
});
const cginfo = constructCallGraphInfo([entrypoint, ...apicons, ...cinits], assembly);
const rcg = [...cginfo.topologicalOrder].reverse();
for (let i = 0; i < rcg.length; ++i) {
const cn = rcg[i];
const cscc = cginfo.recursive.find((scc) => scc.has(cn.invoke));
let worklist = cscc !== undefined ? [...cscc].sort() : [cn.invoke];
for (let mi = 0; mi < worklist.length; ++mi) {
const ikey = worklist[mi];
const idcl = (assembly.invokeDecls.get(ikey) || assembly.primitiveInvokeDecls.get(ikey)) as MIRInvokeDecl;
const finfo = this.bemitter.generateSMTInvoke(idcl);
this.processVirtualInvokes();
this.processVirtualEntityUpdates();
if (finfo !== undefined) {
if (finfo instanceof SMTFunction) {
this.assembly.functions.push(finfo);
}
else {
this.assembly.uninterpfunctions.push(finfo);
}
}
}
}
assembly.typeMap.forEach((tt) => {
const restype = this.temitter.getSMTTypeFor(tt);
if (this.assembly.resultTypes.find((rtt) => rtt.ctype.name === restype.name) === undefined) {
this.assembly.resultTypes.push(({ hasFlag: false, rtname: tt.typeID, ctype: restype }));
}
});
this.bemitter.requiredLoadVirtualTupleIndex.forEach((rvlt) => this.assembly.functions.push(this.bemitter.generateLoadTupleIndexVirtual(rvlt)));
this.bemitter.requiredLoadVirtualRecordProperty.forEach((rvlr) => this.assembly.functions.push(this.bemitter.generateLoadRecordPropertyVirtual(rvlr)));
this.bemitter.requiredLoadVirtualEntityField.forEach((rvle) => this.assembly.functions.push(this.bemitter.generateLoadEntityFieldVirtual(rvle)));
this.bemitter.requiredProjectVirtualTupleIndex.forEach((rvpt) => this.assembly.functions.push(this.bemitter.generateProjectTupleIndexVirtual(rvpt)));
this.bemitter.requiredProjectVirtualRecordProperty.forEach((rvpr) => this.assembly.functions.push(this.bemitter.generateProjectRecordPropertyVirtual(rvpr)));
this.bemitter.requiredProjectVirtualEntityField.forEach((rvpe) => this.assembly.functions.push(this.bemitter.generateProjectEntityFieldVirtual(rvpe)));
this.bemitter.requiredUpdateVirtualTuple.forEach((rvut) => this.assembly.functions.push(this.bemitter.generateUpdateTupleIndexVirtual(rvut)));
this.bemitter.requiredUpdateVirtualRecord.forEach((rvur) => this.assembly.functions.push(this.bemitter.generateUpdateRecordPropertyVirtual(rvur)));
const mirep = assembly.invokeDecls.get(entrypoint) as MIRInvokeDecl;
const iargs = mirep.params.map((param, i) => {
const mirptype = this.temitter.getMIRType(param.type);
const vname = this.bemitter.varStringToSMT(param.name).vname;
let ufuncs: SMTFunctionUninterpreted[] = [];
this.walkAndGenerateHavocType(mirptype, this.assembly.havocfuncs, []);
ufuncs.forEach((uf) => {
if(this.assembly.uninterpfunctions.find((f) => SMTFunctionUninterpreted.areDuplicates(f, uf)) === undefined) {
this.assembly.uninterpfunctions.push(uf);
}
});
const vexp = this.temitter.generateHavocConstructorCall(mirptype, new SMTCallSimple("seq.unit", [this.bemitter.numgen.int.emitSimpleNat(0)]), this.bemitter.numgen.int.emitSimpleNat(i));
return { vname: vname, vtype: this.temitter.generateResultType(mirptype), vinit: vexp, vchk: this.temitter.generateResultIsSuccessTest(mirptype, new SMTVar(vname)), callexp: this.temitter.generateResultGetSuccess(mirptype, new SMTVar(vname)) };
});
const restype = this.temitter.getMIRType(mirep.resultType);
let ufuncs: SMTFunctionUninterpreted[] = [];
this.walkAndGenerateHavocType(restype, this.assembly.havocfuncs, ufuncs);
ufuncs.forEach((uf) => {
if(this.assembly.uninterpfunctions.find((f) => SMTFunctionUninterpreted.areDuplicates(f, uf)) === undefined) {
this.assembly.uninterpfunctions.push(uf);
}
});
const resvexp = this.temitter.generateHavocConstructorCall(restype, new SMTConst("(as seq.empty (Seq BNat))"), this.bemitter.numgen.int.emitSimpleNat(1));
const rarg = { vname: "_@smtres@_arg", vtype: this.temitter.generateResultType(restype), vinit: resvexp, vchk: this.temitter.generateResultIsSuccessTest(restype, new SMTVar("_@smtres@_arg")), callexp: this.temitter.generateResultGetSuccess(restype, new SMTVar("_@smtres@_arg")) };
assembly.entityDecls.forEach((edcl) => {
const mirtype = this.temitter.getMIRType(edcl.tkey);
const ttag = this.temitter.getSMTTypeFor(mirtype).smttypetag;
if (!this.assembly.typeTags.includes(ttag)) {
this.assembly.typeTags.push(ttag);
}
if (!this.assembly.keytypeTags.includes(ttag)) {
if (assembly.subtypeOf(mirtype, this.temitter.getMIRType("NSCore::KeyType"))) {
this.assembly.keytypeTags.push(ttag);
}
}
if (edcl instanceof MIRPrimitiveListEntityTypeDecl) {
this.processListTypeDecl(edcl);
}
else {
if (edcl instanceof MIRObjectEntityTypeDecl) {
this.processEntityDecl(edcl);
}
else {
this.processSpecialEntityDecl(edcl);
}
}
});
this.bemitter.requiredSubtypeTagChecks.forEach((stc) => {
const occ = stc.oftype.options[0] as MIRConceptType;
for(let i = 0; i < occ.ckeys.length; ++i) {
const atname = `AbstractTypeTag_${this.temitter.getSMTTypeFor(this.temitter.getMIRType(occ.ckeys[i]))}`;
if(!this.assembly.abstractTypes.includes(atname)) {
this.assembly.abstractTypes.push(atname);
}
assembly.typeMap.forEach((mtype) => {
if(this.temitter.isUniqueType(mtype) && assembly.subtypeOf(mtype, stc.t)) {
const ttag = this.temitter.getSMTTypeFor(mtype).smttypetag;
if(this.assembly.subtypeRelation.find((ee) => ee.ttype === ttag && ee.atype === atname) === undefined) {
const issub = assembly.subtypeOf(mtype, stc.oftype);
this.assembly.subtypeRelation.push({ttype: ttag, atype: atname, value: issub});
}
}
});
}
});
this.bemitter.requiredIndexTagChecks.forEach((itc) => {
const itag = `TupleIndexTag_${itc.idx}`;
if(!this.assembly.indexTags.includes(itag)) {
this.assembly.indexTags.push(itag);
}
assembly.typeMap.forEach((mtype) => {
if (this.temitter.isUniqueType(mtype) && assembly.subtypeOf(mtype, itc.oftype)) {
const ttype = mtype.options[0] as MIRTupleType;
const ttag = `TypeTag_${this.temitter.getSMTTypeFor(mtype).name}`;
if (this.assembly.hasIndexRelation.find((ee) => ee.idxtag === itag && ee.atype === ttag) === undefined) {
const hasidx = itc.idx < ttype.entries.length;
this.assembly.hasIndexRelation.push({ idxtag: itag, atype: ttag, value: hasidx });
}
}
});
});
this.bemitter.requiredRecordTagChecks.forEach((rtc) => {
const ptag = `RecordPropertyTag_${rtc.pname}`;
if(!this.assembly.propertyTags.includes(ptag)) {
this.assembly.propertyTags.push(ptag);
}
assembly.typeMap.forEach((mtype) => {
if (this.temitter.isUniqueType(mtype) && assembly.subtypeOf(mtype, rtc.oftype)) {
const ttype = mtype.options[0] as MIRRecordType;
const ttag = `TypeTag_${this.temitter.getSMTTypeFor(mtype).name}`;
if (this.assembly.hasPropertyRelation.find((ee) => ee.pnametag === ptag && ee.atype === ttag) === undefined) {
const haspname = ttype.entries.find((entry) => entry.pname === rtc.pname) !== undefined;
this.assembly.hasPropertyRelation.push({ pnametag: ptag, atype: ttag, value: haspname });
}
}
});
});
assembly.tupleDecls.forEach((ttup) => {
const mirtype = this.temitter.getMIRType(ttup.typeID);
const ttag = `TypeTag_${this.temitter.getSMTTypeFor(mirtype).name}`;
const iskey = assembly.subtypeOf(mirtype, this.temitter.getMIRType("NSCore::KeyType"));
this.assembly.typeTags.push(ttag);
if(iskey) {
this.assembly.keytypeTags.push(ttag);
}
ttup.entries.map((entry) => {
const etype = this.temitter.getSMTTypeFor(entry);
if (this.assembly.resultTypes.find((rtt) => rtt.ctype.name === etype.name) === undefined) {
this.assembly.resultTypes.push(({ hasFlag: true, rtname: entry.typeID, ctype: etype }));
}
});
const smttype = this.temitter.getSMTTypeFor(mirtype);
const ops = this.temitter.getSMTConstructorName(mirtype);
const consargs = ttup.entries.map((entry, i) => {
return { fname: this.temitter.generateTupleIndexGetFunction(ttup, i), ftype: this.temitter.getSMTTypeFor(entry) };
});
this.assembly.tupleDecls.push(new SMTTupleDecl(iskey, smttype.name, ttag, { cname: ops.cons, cargs: consargs }, ops.box, ops.bfield));
});
assembly.recordDecls.forEach((trec) => {
const mirtype = this.temitter.getMIRType(trec.typeID);
const ttag = `TypeTag_${this.temitter.getSMTTypeFor(mirtype).name}`;
const iskey = assembly.subtypeOf(mirtype, this.temitter.getMIRType("NSCore::KeyType"));
this.assembly.typeTags.push(ttag);
if(iskey) {
this.assembly.keytypeTags.push(ttag);
}
trec.entries.map((entry) => {
const etype = this.temitter.getSMTTypeFor(entry.ptype);
if (this.assembly.resultTypes.find((rtt) => rtt.ctype.name === etype.name) === undefined) {
this.assembly.resultTypes.push(({ hasFlag: true, rtname: entry.ptype.typeID, ctype: etype }));
}
});
const smttype = this.temitter.getSMTTypeFor(mirtype);
const ops = this.temitter.getSMTConstructorName(mirtype);
const consargs = trec.entries.map((entry) => {
return { fname: this.temitter.generateRecordPropertyGetFunction(trec, entry.pname), ftype: this.temitter.getSMTTypeFor(entry.ptype) };
});
this.assembly.recordDecls.push(new SMTRecordDecl(iskey, smttype.name, ttag, { cname: ops.cons, cargs: consargs }, ops.box, ops.bfield));
});
assembly.ephemeralListDecls.forEach((ephl) => {
const mirtype = this.temitter.getMIRType(ephl.typeID);
const smttype = this.temitter.getSMTTypeFor(mirtype);
const ops = this.temitter.getSMTConstructorName(mirtype);
const consargs = ephl.entries.map((entry, i) => {
return { fname: this.temitter.generateEphemeralListGetFunction(ephl, i), ftype: this.temitter.getSMTTypeFor(entry) };
});
this.assembly.ephemeralDecls.push(new SMTEphemeralListDecl(smttype.name, { cname: ops.cons, cargs: consargs }));
});
assembly.constantDecls.forEach((cdecl) => {
const smtname = this.temitter.lookupGlobalName(cdecl.gkey);
const consf = this.temitter.lookupFunctionName(cdecl.ivalue);
const ctype = this.temitter.getSMTTypeFor(this.temitter.getMIRType(cdecl.declaredType));
let optenumname: [string, string] | undefined = undefined;
if(cdecl.attributes.includes("enum")) {
optenumname = [cdecl.enclosingDecl as string, cdecl.gkey];
}
if((callsafety.get(cdecl.ivalue) as {safe: boolean, trgt: boolean}).safe) {
this.assembly.constantDecls.push(new SMTConstantDecl(smtname, optenumname, ctype, consf, new SMTConst(consf), undefined));
}
else {
const rconsf = this.temitter.generateResultGetSuccess(this.temitter.getMIRType(cdecl.declaredType), new SMTConst(consf));
const rcheck = this.temitter.generateResultIsSuccessTest(this.temitter.getMIRType(cdecl.declaredType), new SMTConst(consf));
this.assembly.constantDecls.push(new SMTConstantDecl(smtname, optenumname, ctype, consf, rconsf, rcheck));
}
});
this.assembly.maskSizes = this.bemitter.maskSizes;
const smtcall = this.temitter.lookupFunctionName(mirep.ikey);
const callargs = iargs.map((arg) => arg.callexp);
const issafe = (callsafety.get(entrypoint) as {safe: boolean, trgt: boolean}).safe;
let iexp: SMTExp | undefined = undefined;
let argchk: SMTExp[] | undefined = undefined;
let targeterrorcheck: SMTExp | undefined = undefined;
let isvaluecheck: SMTExp | undefined = undefined;
if(issafe) {
iexp = this.temitter.generateResultTypeConstructorSuccess(restype, new SMTCallSimple(smtcall, callargs));
targeterrorcheck = new SMTConst("false");
isvaluecheck = new SMTConst("true");
}
else {
iexp = new SMTCallGeneral(smtcall, callargs);
if(mirep.preconditions !== undefined) {
argchk = mirep.preconditions.map((pc) => {
const ispcsafe = (callsafety.get(pc) as {safe: boolean, trgt: boolean}).safe;
if(ispcsafe) {
return new SMTCallSimple(this.temitter.lookupFunctionName(pc), callargs);
}
else {
return SMTCallSimple.makeEq(new SMTCallGeneral(this.temitter.lookupFunctionName(pc), callargs), this.temitter.generateResultTypeConstructorSuccess(this.temitter.getMIRType("NSCore::Bool"), new SMTConst("true")));
}
});
}
targeterrorcheck = new SMTCallSimple("=", [new SMTVar("_@smtres@"), this.temitter.generateResultTypeConstructorError(restype, new SMTConst("ErrorID_Target"))]);
isvaluecheck = this.temitter.generateResultIsSuccessTest(restype, new SMTVar("_@smtres@"));
}
this.bemitter.requiredUFConsts.forEach((ctype) => {
const ufcc = new SMTFunctionUninterpreted(`${ctype.name}@uicons_UF`, [], ctype);
this.assembly.uninterpfunctions.push(ufcc);
});
this.assembly.model = new SMTModelState(iargs, rarg, argchk, this.temitter.generateResultType(restype), iexp, targeterrorcheck, isvaluecheck);
this.assembly.allErrors = this.bemitter.allErrors;
}