package gov.nasa.jpf.listener;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.PropertyListenerAdapter;
import gov.nasa.jpf.vm.ElementInfo;
import gov.nasa.jpf.vm.VM;
import gov.nasa.jpf.vm.MethodInfo;
import gov.nasa.jpf.vm.ThreadInfo;
import gov.nasa.jpf.vm.bytecode.FieldInstruction;
import gov.nasa.jpf.vm.Instruction;
import gov.nasa.jpf.report.ConsolePublisher;
import gov.nasa.jpf.report.Publisher;
import java.io.PrintWriter;
import java.util.Collections;
import gov.nasa.jpf.util.VarSpec;
import gov.nasa.jpf.util.FieldSpec;
import java.util.Set;
import gov.nasa.jpf.vm.FieldInfo;
import gov.nasa.jpf.jvm.bytecode.ASTORE;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.StackFrame;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.List;
public class NonNullChecker extends PropertyListenerAdapter {
// TO-DO: incluir declaraci ́on de dos arrays (o estructura de
//        datos similar):
//        * cuyos elementos sean FieldSpec, para almacenar los
//          campos de inter ́es (recogido del .jpf)
//        * cuyos elementos sean VarSpec, para almacenar las
//          variables de inter ́es (recogidas del .jpf)
    private FieldSpec[] fspec;
    private VarSpec[] vspec;
// TO-DO: incluir declaraci ́on del array (o estructura de datos
//        similar) para los errores
    private List<String> errors;

    public NonNullChecker (Config conf, JPF jpf){
        extractFields(conf);
        extractVars(conf);
        errors = new ArrayList<>();
        jpf.addPublisherExtension(ConsolePublisher.class, this);
    }
    int num_error = 0;
    VM vm;

    private void extractFields(Config conf) {
        Set<String> spec = conf.getStringSet("nonnull.fields");
        if (spec == null)
            spec = Collections.emptySet();
        fspec = new FieldSpec[spec.size()];
        int i = -1;
        for (String field : spec)
            fspec[++i] = FieldSpec.createFieldSpec(field);
    }

    private void extractVars(Config conf) {
        Set<String> spec = conf.getStringSet("nonnull.vars");
        if (spec == null)
            spec = Collections.emptySet();
        vspec = new VarSpec[spec.size()];
        int i = -1;
        for (String var : spec)
            vspec[++i] = VarSpec.createVarSpec(var);
    }

    private void checkFieldInsn(FieldInstruction insn, ThreadInfo ti, VM vm) {
        if (isRelevantField(insn)) {
            if (isNullFieldStore(insn,ti)) {
                // TO-DO: c ́odigo para almacenar en el array de errores un
                //        String con el error detectado
                errors.add("Error en el campo " + insn.getFieldName() +
                        " en linea " + insn.getLineNumber() );
                num_error++;
                vm.backtrack();
            }
        }
    }

    private boolean isRelevantField(FieldInstruction insn) {
        if (!insn.isReferenceField())
            return false;
        FieldInfo fi = insn.getFieldInfo();
        for (FieldSpec fs : fspec) {
            if (fs.matches(fi))
                return true;
        }
        return false;
    }

    private boolean isNullFieldStore(FieldInstruction insn, ThreadInfo ti) {
        FieldInfo fi = insn.getFieldInfo();
        ElementInfo ei = insn.getElementInfo(ti);
        return ei.getFieldValueObject(fi.getName()) == null;
    }

    @Override
    public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){
        // TO-DO:
        // Si se trata de una instrucci´on FieldInstruction
        // entonces llama al m´etodo de comprobaci´on para campos
        // Sugerencia: usar (instanceof) para comprobar si insn
        // es de la clase requerida
        if (insn instanceof FieldInstruction){
            checkFieldInsn((FieldInstruction) insn, ti, vm);
        }
        if(insn instanceof ASTORE){
            checkLocalVarInsn((ASTORE) insn, ti, vm);
        }
    }

    private boolean isRelevantVar(ASTORE insn) {
        int slotIdx = insn.getLocalVariableIndex();
        MethodInfo mi = insn.getMethodInfo();
        int pc = insn.getPosition() + 1;
        for (VarSpec varSpec : vspec) {
            if (varSpec.getMatchingLocalVarInfo(mi, pc, slotIdx) != null)
                return true;
        }
        return false;
    }
    private boolean isNullVarStore(ASTORE insn, ThreadInfo ti) {
        String vn = insn.getLocalVariableName();
        StackFrame frame = ti.getTopFrame();
        return (!(frame.getLocalOrFieldValue(vn) == null));
    }

    private void checkLocalVarInsn(ASTORE insn, ThreadInfo ti, VM vm) {
        // TO-DO: completar c´odigo
        if(isRelevantVar(insn)){
            if(isNullVarStore(insn, ti)){
                errors.add("Error en la variable " + insn.getLocalVariableName() +
                        " en linea " + insn.getLineNumber() );
                num_error++;
                vm.backtrack();
            }
        }
    }

    @Override
    public boolean check(Search search, VM vm) {
        return errors.isEmpty();
    }

    @Override
    public void reset() {
        errors = new ArrayList<>();
    }


    @Override
    public String getErrorMessage() {
        if (!errors.isEmpty()){
            StringWriter sw = new StringWriter();
            PrintWriter pw = new PrintWriter(sw);
            errors.forEach(it -> pw.println(it));
            pw.flush();
            return sw.toString();

        } else {
            return null;
        }
    }


}