obs

package
v0.0.0-...-1dd1f65 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Feb 26, 2023 License: MIT Imports: 11 Imported by: 0

Documentation

Overview

Package obs concerns 'observations': the end result of running a test on a particular machine.

Index

Examples

Constants

This section is empty.

Variables

View Source 
var (
	// ErrBadFlag occurs when we read an unknown observation flag.
	ErrBadFlag = errors.New("bad observation flag")

	// FlagNames maps the string representation of each observation flag to its flag value.
	FlagNames = map[string]Flag{
		"sat":     Sat,
		"unsat":   Unsat,
		"undef":   Undef,
		"exist":   Exist,
		"partial": Partial,
	}
)
View Source 
var BadTag = errors.New("bad tag name")

BadTag occurs when we try to unmarshal a string that doesn't correspond to a Tag.

Functions

func AddCommonTemplates 

func AddCommonTemplates(t *template.Template, indent func(n int) string) (*template.Template, error)

AddCommonTemplates adds to t a set of templates useful for pretty-printing observations.

indent is a function that should indent observation lines n places, as well as adding any indenting needed to put the lines into context.

func Pretty 

func Pretty(w io.Writer, o Obs, m PrettyMode) error

Pretty pretty-prints an observation o onto w according to mode m.

Example (Dnf)

ExamplePretty_dnf shows the result of pretty-printing an observation to a DNF postcondition. 

package main

import (
	"fmt"
	"os"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	o := obs.Obs{
		Flags: obs.Sat,
		States: []obs.State{
			{Values: obs.Valuation{"x": "1", "y": "0"}, Tag: obs.TagCounter},
			{Values: obs.Valuation{"x": "0", "y": "0"}, Tag: obs.TagCounter},
			{Values: obs.Valuation{"x": "0", "y": "1"}, Tag: obs.TagWitness},
			{Values: obs.Valuation{"x": "1", "y": "1"}, Tag: obs.TagWitness},
		},
	}

	if err := obs.Pretty(os.Stdout, o, obs.PrettyMode{Dnf: true}); err != nil {
		fmt.Println("error:", err)
	}

}

Output:

forall (
     (x == 1 /\ y == 0)
  \/ (x == 0 /\ y == 0)
  \/ (x == 0 /\ y == 1)
  \/ (x == 1 /\ y == 1)
)
Example (Dnf_empty)

ExamplePretty_dnf_empty shows the result of pretty-printing an empty observation to a DNF postcondition. 

package main

import (
	"fmt"
	"os"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	if err := obs.Pretty(os.Stdout, (obs.Obs{}), obs.PrettyMode{Dnf: true}); err != nil {
		fmt.Println("error:", err)
	}

}

Output:

forall (
  true
)
Example (Interesting_exists)

ExamplePretty_dnf_empty shows the result of pretty-printing an interesting existential. 

package main

import (
	"fmt"
	"os"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	o := obs.Obs{
		Flags: obs.Sat | obs.Exist,
		States: []obs.State{
			{Values: obs.Valuation{"x": "1", "y": "0"}, Tag: obs.TagCounter},
			{Values: obs.Valuation{"x": "0", "y": "0"}, Tag: obs.TagCounter},
			{Values: obs.Valuation{"x": "0", "y": "1"}, Tag: obs.TagWitness},
			{Values: obs.Valuation{"x": "1", "y": "1"}, Tag: obs.TagWitness},
		},
	}

	if err := obs.Pretty(os.Stdout, o, obs.PrettyMode{Interesting: true}); err != nil {
		fmt.Println("error:", err)
	}

}

Output:

postcondition witnessed by:
  x = 0, y = 1
  x = 1, y = 1

Types

type Flag 

type Flag int

Flag is the type of observation flags. 

const (
	// Sat represents a satisfying observation.
	//
	// By default, this flag means that all states met the observation criteria.  If the Exist flag is also set,
	// it means that at least one state met the criteria.
	Sat Flag = 1 << iota
	// Unsat represents a satisfying observation.
	//
	// By default, this flag means that at least one state did not meet the observation criteria.  If the Exist flag is
	// also set, it means that no states met the criteria.
	Unsat
	// Undef represents an undefined-behaviour observation.
	Undef
	// Exist represents an existential observation (the default is for-all observations).
	Exist
	// Partial represents a partial observation.
	//
	// Usually, this means that the backend supports partial execution, and the test was interrupted before it could
	// finish.
	Partial
)

func FlagOfStrings 

func FlagOfStrings(strs ...string) (Flag, error)

FlagOfStrings reconstitutes an observation flag given a representation as a list strs of strings.

Example

ExampleFlagOfStrings is a testable example for FlagOfStrings. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	f, _ := obs.FlagOfStrings("unsat", "undef")
	fmt.Println(f.Has(obs.Sat))
	fmt.Println(f.Has(obs.Unsat))
	fmt.Println(f.Has(obs.Undef))

}

Output:

false
true
true

func (Flag) Has 

func (o Flag) Has(f Flag) bool

Has checks to see if f is present in this flagset.

func (Flag) IsExistential 

func (o Flag) IsExistential() bool

IsExistential gets whether a flag represents an existential (rather than universal) observation.

func (Flag) IsInteresting 

func (o Flag) IsInteresting() bool

IsInteresting gets whether a flag represents an 'interesting' condition.

Interesting conditions are ones that might represent a compiler bug, assuming that the test has a postcondition that either defines the allowed states universally, or one particular buggy state existentially.

func (Flag) IsPartial 

func (o Flag) IsPartial() bool

IsPartial gets whether a flag represents a partial observation.

Example

ExampleFlag_IsPartial is a testable example for Flag.IsPartial. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	fmt.Println("empty:", obs.Flag(0).IsPartial())
	fmt.Println("not-partial:", obs.Unsat.IsPartial())
	fmt.Println("partial:", obs.Partial.IsPartial())
	fmt.Println("e-partial:", (obs.Partial | obs.Exist).IsPartial())

}

Output:

empty: false
not-partial: false
partial: true
e-partial: true

func (Flag) IsSat 

func (o Flag) IsSat() bool

IsSat gets whether a flag represents a satisfying observation.

Example

ExampleFlag_IsSat is a testable example for Flag.IsSat. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	fmt.Println("empty:", obs.Flag(0).IsSat())
	fmt.Println("unsat:", obs.Unsat.IsSat())
	fmt.Println("e-sat:", (obs.Sat | obs.Exist).IsSat())

}

Output:

empty: false
unsat: false
e-sat: true

func (Flag) IsUnsat 

func (o Flag) IsUnsat() bool

IsUnsat gets whether a flag represents an unsatisfying observation.

Example

ExampleFlag_IsUnsat is a testable example for Flag.IsUnsat. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	fmt.Println("empty:", obs.Flag(0).IsUnsat())
	fmt.Println("unsat:", obs.Unsat.IsUnsat())
	fmt.Println("e-sat:", (obs.Sat | obs.Exist).IsUnsat())

}

Output:

empty: false
unsat: true
e-sat: false

func (Flag) MarshalJSON 

func (o Flag) MarshalJSON() ([]byte, error)

MarshalJSON marshals an observation flag list as a string list.

func (Flag) MarshalText 

func (o Flag) MarshalText() ([]byte, error)

MarshalText marshals an observation flag as a space-delimited string list.

func (Flag) Strings 

func (o Flag) Strings() []string

Strings expands this ObsFlag into string equivalents for each set flag.

Example

ExampleFlag_Strings is a testable example for Flag.Strings. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	for _, s := range (obs.Sat | obs.Undef).Strings() {
		fmt.Println(s)
	}

}

Output:

sat
undef

func (*Flag) UnmarshalJSON 

func (o *Flag) UnmarshalJSON(bs []byte) error

UnmarshalJSON unmarshals an observation flag list from bs by interpreting it as a string list.

func (*Flag) UnmarshalText 

func (o *Flag) UnmarshalText(bs []byte) error

UnmarshalText unmarshals an observation flag list from bs by interpreting it as a string list.

type Obs 

type Obs struct {
	// Flags contains any flags that are active on Obs.
	Flags Flag `json:"flags,omitempty"`
	// States lists all states in this observation.
	States []State `json:"states,omitempty"`
}

Obs represents an observation in C4's JSON-based format.

func (Obs) CounterExamples 

func (o Obs) CounterExamples() []State

CounterExamples gets the list of counter-example states in this observation.

func (Obs) Status 

func (o Obs) Status() status.Status

Status determines the status of an observation o.

Currently, an observation is considered to be 'ok' if it is a satisfied universal or unsatisfied existential, and 'flagged' otherwise.

Example

ExampleObs_Status is a testable example for Obs.Status. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	fmt.Println("empty:  ", (&obs.Obs{}).Status())
	fmt.Println("undef:  ", (&obs.Obs{Flags: obs.Undef}).Status())
	fmt.Println("sat:    ", (&obs.Obs{Flags: obs.Sat}).Status())
	fmt.Println("unsat:  ", (&obs.Obs{Flags: obs.Unsat}).Status())
	fmt.Println("e-sat:  ", (&obs.Obs{Flags: obs.Sat | obs.Exist}).Status())
	fmt.Println("e-unsat:", (&obs.Obs{Flags: obs.Unsat | obs.Exist}).Status())

}

Output:

empty:   Flagged
undef:   Flagged
sat:     Ok
unsat:   Flagged
e-sat:   Flagged
e-unsat: Ok

func (Obs) WithTag 

func (o Obs) WithTag(t Tag) []State

WithTag gets the list of states with tag t in this observation.

func (Obs) Witnesses 

func (o Obs) Witnesses() []State

Witnesses gets the list of witnessing states in this observation.

type PrettyMode 

type PrettyMode struct {
	// Dnf controls whether the pretty-printer prints a disjunctive-normal-form postcondition.
	Dnf bool
	// Interesting controls whether the pretty-printer prints 'interesting' state results.
	Interesting bool
}

PrettyMode controls various pieces of pretty-printer functionality.

type State 

type State struct {
	// Tag is the kind of state this is.
	Tag Tag `json:"tag,omitempty"`
	// Occurrences is the number of times this state was observed.
	// If this number is zero, there was no occurrence reporting for this state;
	// states which were observed zero times will not appear in the observation at all.
	Occurrences uint64 `json:"occurrences,omitempty"`
	// Values is the valuation for this state.
	Values Valuation `json:"values,omitempty"`
}

State represents a single state in C4's JSON-based format.

type Tag 

type Tag int

Tag classifies a state line. 

const (
	// TagUnknown represents a state that is not known to be either a witness or a counter-example.
	TagUnknown Tag = iota // unknown
	// TagWitness represents a state that validates a condition.
	TagWitness // witness
	// TagCounter represents a state that goes against a condition.
	TagCounter // counter
	// TagLast refers to the last tag.
	TagLast = TagCounter
)

func (Tag) MarshalText 

func (i Tag) MarshalText() (text []byte, err error)

MarshalText marshals a Tag into text.

func (Tag) String 

func (i Tag) String() string

func (*Tag) UnmarshalText 

func (i *Tag) UnmarshalText(text []byte) error

UnmarshalText unmarshals text into a Tag.

type Valuation 

type Valuation map[string]string

Valuation is an observed assignment of variable names to values.

func (Valuation) Vars 

func (v Valuation) Vars() []string

Vars gets a sorted list of variables bound by a state.

Example

ExampleValuation_Vars is a runnable example for State.Vars. 

package main

import (
	"fmt"

	"github.com/c4-project/c4t/internal/subject/obs"
)

func main() {
	for _, v := range (obs.Valuation{
		"x": "1",
		"a": "2",
		"b": "3",
		"y": "4",
	}).Vars() {
		fmt.Println(v)
	}

}

Output:

a
b
x
y

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.