Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Frangel v2 #27

Open
wants to merge 15 commits into
base: dev
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Project.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,13 @@ authors = ["Tilman Hinnerichs <[email protected]>", "Jaap de Jong <jaapd
version = "0.1.3"

[deps]
DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
HerbCore = "2b23ba43-8213-43cb-b5ea-38c12b45bd45"
HerbGrammar = "4ef9e186-2fe5-4b24-8de7-9f7291f24af7"
HerbSpecification = "6d54aada-062f-46d8-85cf-a1ceaf058a06"

[compat]
DataStructures = "0.17,0.18"
HerbCore = "^0.3.0"
HerbGrammar = "^0.3.0"
HerbSpecification = "^0.1.0"
Expand Down
23 changes: 22 additions & 1 deletion src/HerbInterpret.jl
Original file line number Diff line number Diff line change
@@ -1,15 +1,36 @@
module HerbInterpret

using DataStructures # Queue

using HerbCore
using HerbGrammar
using HerbSpecification

include("interpreter.jl")

include("angelic_conditions/bit_trie.jl")
include("angelic_conditions/angelic_config.jl")
include("angelic_conditions/execute_angelic.jl")

export
SymbolTable,
interpret,

execute_on_input
execute_on_input,
update_✝γ_path,
CodePath,

create_angelic_expression,
ConfigAngelic,
execute_angelic_on_input,
get_code_paths!,

BitTrie,
BitTrieNode,
trie_add!,
trie_contains,

passes_the_same_tests_or_more,
update_passed_tests!

end # module HerbInterpret
20 changes: 20 additions & 0 deletions src/angelic_conditions/angelic_config.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
"""
struct ConfigAngelic

A configuration struct for angelic conditions. Includes both generation- and evaluation-specific parameters.

# Fields
- `max_time::Float16`: The maximum time allowed for resolving a single angelic expression.
- `boolean_expr_max_depth::Int`: The maximum depth of boolean expressions when resolving angelic conditions.
- `max_execute_attempts::Int`: The maximal attempts of executing the program with angelic evaluation.
- `max_allowed_fails::Float16`: The maximum allowed fraction of failed tests during evaluation before short-circuit failure.
- `angelic_rulenode::Union{Nothing,RuleNode}`: The angelic rulenode. Used to replace angelic conditions/holes right before evaluation.

"""
Base.@kwdef mutable struct ConfigAngelic
max_time::Float16 = 0.1
boolean_expr_max_depth::Int64 = 3
max_execute_attempts::Int = 55
max_allowed_fails::Float16 = 0.75
angelic_rulenode::Union{Nothing,RuleNode} = nothing
end
62 changes: 62 additions & 0 deletions src/angelic_conditions/bit_trie.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
"""
An implementation of a bare-bones trie data structure
https://en.wikipedia.org/wiki/Trie

This trie does not store values associated to the nodes, and the paths are built using bitstrings instead of regular strings.

The trie is used to store code paths that have been traversed, and check if a given path is a prefix of any of the stored paths.

"""
Base.@kwdef mutable struct BitTrieNode
left::Union{BitTrieNode,Nothing} = nothing
right::Union{BitTrieNode,Nothing} = nothing
is_leaf::Bool = false
end

Base.@kwdef mutable struct BitTrie
root::Union{BitTrieNode,Nothing} = BitTrieNode()
size::Int = 0
end

# Adds nodes to the trie to represent the given path
function trie_add!(trie::BitTrie, path::BitVector)
curr = trie.root
for i in eachindex(path)
if path[i]
if curr.right === nothing
curr.right = BitTrieNode()
end
curr = curr.right
else
if curr.left === nothing
curr.left = BitTrieNode()
end
curr = curr.left
end
if curr.is_leaf
return
end
end
if !curr.is_leaf
trie.size += 1
curr.is_leaf = true
end
end

# Checks if the trie contains the given path - used for
function trie_contains(trie::BitTrie, path::BitVector)
curr = trie.root
if curr.is_leaf
return true

Check warning on line 50 in src/angelic_conditions/bit_trie.jl

View check run for this annotation

Codecov / codecov/patch

src/angelic_conditions/bit_trie.jl#L50

Added line #L50 was not covered by tests
end
for i in eachindex(path)
curr = path[i] ? curr.right : curr.left
if curr === nothing
return false
end
if curr.is_leaf
return true
end
end
false
end
141 changes: 141 additions & 0 deletions src/angelic_conditions/execute_angelic.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,141 @@
"""
execute_angelic_on_input(
symboltable::SymbolTable, program::RuleNode, grammar::AbstractGrammar, input::Dict{Symbol,Any},
expected_output::Any, angelic_rulenode::RuleNode, max_attempts::Int, angelic_conditions::Dict{UInt16,UInt8})::Bool

Run test case `input` on `program` containing angelic conditions. This is done by optimistically evaluating the program, by generating different code paths
and checking if any of them make the program pass the test case.

# Arguments
- `symboltable`: The symbol table containing the program's symbols.
- `program`: The program to be executed.
- `grammar`: The grammar rules of the program.
- `input`: A dictionary where each key is a symbol used in the expression, and the value is the corresponding value to be used in the expression's evaluation.
- `expected_output`: The expected output of the program.
- `angelic_rulenode`: The angelic rulenode. It is used to replace angelified conditions.
- `max_attempts`: The maximum number of attempts before assuming the angelic program cannot be resolved.
- `angelic_conditions`: A dictionary mapping indices of angelic condition candidates, to the child index that may be changed.

# Returns
Whether the output of running `program` on `input` matches `output` within `max_attempts` attempts.

"""
function execute_angelic_on_input(
symboltable::SymbolTable,
program::RuleNode,
grammar::AbstractGrammar,
input::Dict{Symbol,Any},
expected_output::Any,
angelic_rulenode::RuleNode,
max_attempts::Int,
angelic_conditions::Dict{UInt16,UInt8}
)::Bool
num_true, attempts = 0, 0
# We check traversed code paths by prefix -> trie is efficient for this
visited = BitTrie()
expr = create_angelic_expression(program, grammar, angelic_rulenode, angelic_conditions)
while num_true < max_attempts
code_paths = Vector{BitVector}()
get_code_paths!(num_true, BitVector(), visited, code_paths, max_attempts - attempts)
# Terminate if we generated max_attempts, or impossible to generate further paths
if isempty(code_paths)
return false

Check warning on line 42 in src/angelic_conditions/execute_angelic.jl

View check run for this annotation

Codecov / codecov/patch

src/angelic_conditions/execute_angelic.jl#L42

Added line #L42 was not covered by tests
end
for code_path in code_paths
# println("Attempt: ", code_path)
actual_code_path = BitVector()
try
output = execute_on_input(symboltable, expr, input, CodePath(code_path, 0), actual_code_path)
# println("Actual path: ", actual_code_path)
if output == expected_output
return true
end
catch

Check warning on line 53 in src/angelic_conditions/execute_angelic.jl

View check run for this annotation

Codecov / codecov/patch

src/angelic_conditions/execute_angelic.jl#L53

Added line #L53 was not covered by tests
# Mark as visited and count attempt
finally
trie_add!(visited, actual_code_path)
attempts += 1
end
end
num_true += 1
end
false

Check warning on line 62 in src/angelic_conditions/execute_angelic.jl

View check run for this annotation

Codecov / codecov/patch

src/angelic_conditions/execute_angelic.jl#L59-L62

Added lines #L59 - L62 were not covered by tests
end

"""
get_code_paths!(num_true::Int, curr::BitVector, visited::BitTrie, code_paths::Vector{BitVector}, max_length::Int)

Generate code paths to be used for angelic evaluation, and stores them in `code_paths`. The function recursively explores different sequences of `true` and `false`
values, which represent whether the next control statement will be skipped or not. Makes sure that the returned paths do not share prefix with visited paths.

# Arguments
- `num_true`: The number of `true` values in the code path.
- `curr`: The current code path being generated.
- `visited`: The visited code paths.
- `code_paths`: The vector to store the generated code paths.
- `max_length`: The maximum length of a code path allowed.

"""
function get_code_paths!(
num_true::Int,
curr::BitVector,
visited,
code_paths::Vector{BitVector},
max_length::Int
)
# If enough code paths, or visited a prefix-path, return
if (length(code_paths) >= max_length || trie_contains(visited, curr))
return
end
# Add current one if enough 'true' values
if num_true == 0
push!(code_paths, deepcopy(curr))
return
end
# Continue with 'true' and build all paths
push!(curr, true)
get_code_paths!(num_true - 1, curr, visited, code_paths, max_length)
# Continue with 'false' and build all paths
curr[end] = false
get_code_paths!(num_true, curr, visited, code_paths, max_length)
pop!(curr)
end

"""
create_angelic_expression(program::RuleNode, grammar::AbstractGrammar, angelic_rulenode::RuleNode, angelic_conditions::Dict{UInt16,UInt8})::Expr

Create an angelic expression, i.e. replace all remaining holes with angelic rulenode trees so that the tree can be parsed and executed.

# Arguments
- `program`: The program to turn into an angelic expression.
- `grammar`: The grammar rules of the program.
- `angelic_rulenode`: The angelic rulenode. It is used to replace angelified conditions.
- `angelic_conditions`: A dictionary mapping indices of angelic condition candidates, to the child index that may be changed.

# Returns
The generated angelic expression.

"""
function create_angelic_expression(
program::RuleNode,
grammar::AbstractGrammar,
angelic_rulenode::RuleNode,
angelic_conditions::Dict{UInt16,UInt8}
)::Expr
new_program = deepcopy(program)
# BFS traversal
queue = DataStructures.Queue{AbstractRuleNode}()
enqueue!(queue, new_program)
while !isempty(queue)
node = dequeue!(queue)
angelic_idx = get(angelic_conditions, node.ind, -1)
for (child_index, child) in enumerate(node.children)
if angelic_idx == child_index && child isa AbstractHole
node.children[child_index] = angelic_rulenode
else
enqueue!(queue, child)
end
end
end
rulenode2expr(new_program, grammar)
end
Loading
Loading