jpf

Documentation

Overview

Package jpf is the Java Pathfinder verification system's implementation of an Impendulo tool. See http://babelfish.arc.nasa.gov/trac/jpf/ for more information.

Index

• Constants
• func Allowed(key string) bool
• func JPFBytes(config map[string][]string) (ret []byte, err error)
• type ChoiceGenerator
• type Class
  • func GetClasses(tipe, fname string) ([]*Class, error)
  • func Listeners() ([]*Class, error)
  • func Searches() ([]*Class, error)
• type Config
  • func NewConfig(projectId bson.ObjectId, target *tool.Target, data []byte) *Config
  • func (this *Config) String() string
• type Error
• type Frame
• type Instruction
• type Report
  • func NewReport(id bson.ObjectId, data []byte) (r *Report, e error)
  • func (r *Report) ErrorCount() int
  • func (r *Report) Lines() []*result.Line
  • func (r *Report) String() string
  • func (r *Report) Success() bool
• type Result
  • func NewResult(fileId bson.ObjectId, data []byte) (res *Result, err error)
  • func (r *Result) ChartVals() []*result.ChartVal
  • func (r *Result) GetFileId() bson.ObjectId
  • func (r *Result) GetId() bson.ObjectId
  • func (r *Result) GetName() string
  • func (r *Result) GetTestId() bson.ObjectId
  • func (r *Result) GetType() string
  • func (r *Result) Lines() []*result.Line
  • func (r *Result) OnGridFS() bool
  • func (r *Result) Reporter() result.Reporter
  • func (r *Result) SetReport(report result.Reporter)
  • func (r *Result) String() string
  • func (r *Result) Success() bool
  • func (r *Result) Template() string
• type Statistics
  • func (s *Statistics) String() string
• type Thread
• type Tool
  • func New(cfg *Config, jpfDir string) (*Tool, error)
  • func (t *Tool) Lang() tool.Language
  • func (t *Tool) Name() string
  • func (t *Tool) Run(fileId bson.ObjectId, target *tool.Target) (result.Tooler, error)
• type Transition
  • func (t *Transition) String() string

Constants

const (
	NAME = "JPF"
)

Functions

func Allowed

func Allowed(key string) bool

Allowed checks whether a JPF property is allowed to be configured.

func JPFBytes

func JPFBytes(config map[string][]string) (ret []byte, err error)

JPFBytes converts a map of JPF properties to a byte array which can be used when running JPF.

Types

type ChoiceGenerator

type ChoiceGenerator struct {
	Class  string `xml:"class,attr"`
	Choice string `xml:"choice,attr"`
}

ChoiceGenerator is what is used to explore the state space. Here we can see what choice was made to reach a certain state. See gov.nasa.jpf.vm.ChoiceGenerator

type Class

type Class struct {
	Name    string
	Package string
}

Class represents properties of a Java class, specifically its name and package.

func GetClasses

func GetClasses(tipe, fname string) ([]*Class, error)

GetClasses retrieves an array of classes matching a specific type and writes them to a provided output file for future use.

func Listeners

func Listeners() ([]*Class, error)

Listeners retrieves all JPF Listener classes.

func Searches

func Searches() ([]*Class, error)

Searches retrieves all JPF Search classes.

type Config

type Config struct {
	Id        bson.ObjectId `bson:"_id"`
	ProjectId bson.ObjectId `bson:"projectid"`
	Time      int64         `bson:"time"`
	Target    *tool.Target  `bson:"target"`
	//Contains configured JPF properties
	Data []byte `bson:"data"`
}

Config represents a JPF configuration. This means that it contains configured JPF properties specific to running a certain project.

func NewConfig

func NewConfig(projectId bson.ObjectId, target *tool.Target, data []byte) *Config

NewConfig creates a new JPF configuration for a certain project.

func (*Config) String

func (this *Config) String() string

String

type Error

type Error struct {
	Property string    `xml:"property"`
	Details  string    `xml:"details"`
	Threads  []*Thread `xml:"threads>thread"`
}

Error represents a JPF Error. It contains the property which was violated as well as a more detailed error message. See gov.nasa.jpf.Error

type Frame

type Frame struct {
	Id      string `xml:"frameid,attr"`
	Line    int    `xml:"line,attr"`
	Details string `xml:",innerxml"`
}

Frame represents a thread's stack frame See gov.nasa.jpf.vm.StackFrame

type Instruction

type Instruction struct {
	Source string `xml:"src,attr"`
	Value  string `xml:",innerxml"`
}

Instruction corresponds to an executed JPF bytecode instruction. See gov.nasa.jpf.vm.Step and gov.nasa.jpf.vm.Instruction

type Report

type Report struct {
	Id      bson.ObjectId
	Version string      `xml:"jpf-version"`
	Stats   *Statistics `xml:"statistics"`
	Errors  []*Error    `xml:"errors>error"`
	Total   int         `xml:"errors>total"`
	//The execution trace is recorded here.
	//See gov.nasa.jpf.vm.Path
	Trace []*Transition `xml:"trace>transition"`
}

Report is the top level structure extracted from the XML generated by JPF. It provides statistics, errors, Threads (the state when an error occurred) and a Trace of how an error came about.

func NewReport

func NewReport(id bson.ObjectId, data []byte) (r *Report, e error)

NewReport generates a new Report from the provided XML data.

func (*Report) ErrorCount

func (r *Report) ErrorCount() int

Errors provided the number of errors found by JPF.

func (*Report) Lines

func (r *Report) Lines() []*result.Line

func (*Report) String

func (r *Report) String() string

String

func (*Report) Success

func (r *Report) Success() bool

Success is true if JPF found no errors.

type Result

type Result struct {
	Id     bson.ObjectId `bson:"_id"`
	FileId bson.ObjectId `bson:"fileid"`
	Name   string        `bson:"name"`
	Report *Report       `bson:"report"`
	GridFS bool          `bson:"gridfs"`
	Type   string        `bson:"type"`
}

func NewResult

func NewResult(fileId bson.ObjectId, data []byte) (res *Result, err error)

NewResult creates a new JPF result. The data []byte is in XML format and therefore allows us to generate a JPF report from it.

func (*Result) ChartVals

func (r *Result) ChartVals() []*result.ChartVal

ChartVals

func (*Result) GetFileId

func (r *Result) GetFileId() bson.ObjectId

GetFileId

func (*Result) GetId

func (r *Result) GetId() bson.ObjectId

GetId

func (*Result) GetName

func (r *Result) GetName() string

GetName

func (*Result) GetTestId

func (r *Result) GetTestId() bson.ObjectId

func (*Result) GetType

func (r *Result) GetType() string

func (*Result) Lines

func (r *Result) Lines() []*result.Line

func (*Result) OnGridFS

func (r *Result) OnGridFS() bool

OnGridFS determines whether r structure is partially stored on the GridFS.

func (*Result) Reporter

func (r *Result) Reporter() result.Reporter

GetReport

func (*Result) SetReport

func (r *Result) SetReport(report result.Reporter)

SetReport is used to change r result's report. R comes in handy when putting data into/getting data out of GridFS

func (*Result) String

func (r *Result) String() string

String allows us to print r struct nicely.

func (*Result) Success

func (r *Result) Success() bool

Success is true if no errors were found.

func (*Result) Template

func (r *Result) Template() string

type Statistics

type Statistics struct {
	Time              int64 `xml:"elapsed-time"`
	NewStates         int   `xml:"new-states"`
	VisitedStates     int   `xml:"visited-states"`
	BacktrackedStates int   `xml:"backtracked-states"`
	EndStates         int   `xml:"end-states"`
	Memory            int   `xml:"max-memory"`
}

Statistics is a simple structure which holds captured information relating to JPF's execution. See gov.nasa.jpf.report.Statistics

func (*Statistics) String

func (s *Statistics) String() string

String

type Thread

type Thread struct {
	Id   int    `xml:"id,attr"`
	Name string `xml:"name,attr"`
	//This thread's state: NEW, RUNNING, BLOCKED, UNBLOCKED, WAITING, TIMEOUT_WAITING,
	//NOTIFIED, INTERRUPTED, TIMEDOUT, TERMINATED, SLEEPING
	Status       string   `xml:"status,attr"`
	Frames       []*Frame `xml:"frame"`
	RequestLocks []string `xml:"lock-request object,attr"`
	//Lock objects this thread owns
	OwnedLocks []string `xml:"lock-owned object,attr"`
}

Thread represents a live thread at the time when an error occurred. See gov.nasa.jpf.vm.ThreadInfo

type Tool

type Tool struct {
	// contains filtered or unexported fields
}

Tool is an implementation of tool.T which runs a JPF on a Java source file. It makes use of runner.JPFRunner to configure and run JPF on a file and runner.ImpenduloPublisher to output the results as XML.

func New

func New(cfg *Config, jpfDir string) (*Tool, error)

New creates a new JPF instance for a given submission. jpfDir is where the Java JPF runner files should be stored for this JPF instance. jpfConfig is the JPF configuration associated with the submission's project.

func (*Tool) Lang

func (t *Tool) Lang() tool.Language

Lang is Java

func (*Tool) Name

func (t *Tool) Name() string

Name is JPF

func (*Tool) Run

func (t *Tool) Run(fileId bson.ObjectId, target *tool.Target) (result.Tooler, error)

Run runs JPF on a specified Java source file. It uses the Java class runner.JPFRunner to actually run JPF on the source file. If the command was successful, the results are read in from a xml file.

type Transition

type Transition struct {
	Id       int              `xml:"frameid,attr"`
	ThreadId int              `xml:"thread,attr"`
	CG       *ChoiceGenerator `xml:"cg"`
	Insns    []*Instruction   `xml:"insn"`
}

Transition is used to store an execution path. See gov.nasa.jpf.vm.Transition

func (*Transition) String

func (t *Transition) String() string

String