diff --git a/ivette/api/generated/kernel/ast/index.ts b/ivette/api/generated/kernel/ast/index.ts index eaaf033326b4ba7835ba5f16fc80c302180a1fee..2a910fb94ae5a99b0f515c71fca9aff3bfa3da03 100644 --- a/ivette/api/generated/kernel/ast/index.ts +++ b/ivette/api/generated/kernel/ast/index.ts @@ -129,8 +129,8 @@ export interface markerInfoData { name: string; /** Marker declaration or description */ descr: string; - /** Marker position */ - position: source; + /** Source location */ + sloc: source; } /** Loose decoder for `markerInfoData` */ @@ -142,7 +142,7 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> = var: jMarkerVarSafe, name: Json.jFail(Json.jString,'String expected'), descr: Json.jFail(Json.jString,'String expected'), - position: jSourceSafe, + sloc: jSourceSafe, }); /** Safe decoder for `markerInfoData` */ @@ -153,13 +153,13 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> = export const byMarkerInfoData: Compare.Order<markerInfoData> = Compare.byFields <{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar, - name: string, descr: string, position: source }>({ + name: string, descr: string, sloc: source }>({ key: Compare.string, kind: byMarkerKind, var: byMarkerVar, name: Compare.alpha, descr: Compare.string, - position: bySource, + sloc: bySource, }); /** Signal for array [`markerInfo`](#markerinfo) */ @@ -302,6 +302,8 @@ export interface functionsData { builtin?: boolean; /** Has the function been analyzed by Eva */ eva_analyzed?: boolean; + /** Source location */ + sloc: source; } /** Loose decoder for `functionsData` */ @@ -316,6 +318,7 @@ export const jFunctionsData: Json.Loose<functionsData> = stdlib: Json.jBoolean, builtin: Json.jBoolean, eva_analyzed: Json.jBoolean, + sloc: jSourceSafe, }); /** Safe decoder for `functionsData` */ @@ -327,7 +330,7 @@ export const byFunctionsData: Compare.Order<functionsData> = Compare.byFields <{ key: Json.key<'#functions'>, name: string, signature: string, main?: boolean, defined?: boolean, stdlib?: boolean, - builtin?: boolean, eva_analyzed?: boolean }>({ + builtin?: boolean, eva_analyzed?: boolean, sloc: source }>({ key: Compare.string, name: Compare.alpha, signature: Compare.string, @@ -336,6 +339,7 @@ export const byFunctionsData: Compare.Order<functionsData> = stdlib: Compare.defined(Compare.boolean), builtin: Compare.defined(Compare.boolean), eva_analyzed: Compare.defined(Compare.boolean), + sloc: bySource, }); /** Signal for array [`functions`](#functions) */ diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx index 4fe544585aa989357a7ae9f6216f48d1a7a90714..3d6d82e4b316940218b02d7c3121d84b220f59c8 100644 --- a/ivette/src/renderer/ASTview.tsx +++ b/ivette/src/renderer/ASTview.tsx @@ -10,28 +10,15 @@ import * as Utils from 'frama-c/utils'; import * as Dome from 'dome'; import * as Json from 'dome/data/json'; -import * as Settings from 'dome/data/settings'; import { RichTextBuffer } from 'dome/text/buffers'; import { Text } from 'dome/text/editors'; -import { IconButton } from 'dome/controls/buttons'; import { Component, TitleBar } from 'frama-c/LabViews'; import * as AST from 'frama-c/api/kernel/ast'; import * as Properties from 'frama-c/api/kernel/properties'; import { getCallers, getDeadCode } from 'frama-c/api/plugins/eva/general'; import { getWritesLval, getReadsLval } from 'frama-c/api/plugins/studia/studia'; -import 'codemirror/mode/clike/clike'; -import 'codemirror/theme/ambiance.css'; -import 'codemirror/theme/solarized.css'; - -import { Theme, FontSize } from './Preferences'; - -const THEMES = [ - { id: 'default', label: 'Default' }, - { id: 'ambiance', label: 'Ambiance' }, - { id: 'solarized light', label: 'Solarized Light' }, - { id: 'solarized dark', label: 'Solarized Dark' }, -]; +import * as Preferences from './Preferences'; // -------------------------------------------------------------------------- // --- Pretty Printing (Browser Console) @@ -152,16 +139,19 @@ const ASTview = () => { const printed = React.useRef<string | undefined>(); const [selection, updateSelection] = States.useSelection(); const multipleSelections = selection?.multiple.allSelections; - const [theme, setTheme] = Settings.useGlobalSettings(Theme); - const [fontSize, setFontSize] = Settings.useGlobalSettings(FontSize); - const [wrapText, flipWrapText] = Dome.useFlipSettings('ASTview.wrapText'); - const markersInfo = States.useSyncArray(AST.markerInfo); - const theFunction = selection?.current?.function; const theMarker = selection?.current?.marker; + const { buttons: themeButtons, theme, fontSize, wrapText } = + Preferences.useThemeButtons({ + target: 'Internal AST', + theme: Preferences.AstTheme, + fontSize: Preferences.AstFontSize, + wrapText: Preferences.AstWrapText, + disabled: !theFunction, + }); + const markersInfo = States.useSyncArray(AST.markerInfo); const deadCode = States.useRequest(getDeadCode, theFunction); - const propertyStatus = States.useSyncArray(Properties.status).getArray(); const statusDict = States.useTags(Properties.propStatusTags); @@ -216,10 +206,6 @@ const ASTview = () => { if (theMarker) buffer.scroll(theMarker); }, [buffer, theMarker]); - // Callbacks - const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2); - const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2); - function onTextSelection(id: string) { if (selection.current) { const location = { ...selection.current, marker: id }; @@ -282,40 +268,11 @@ const ASTview = () => { Dome.popupMenu(items); } - // Theme Popup - const selectTheme = (id?: string) => id && setTheme(id); - const themeItem = (th: { id: string; label: string }) => ( - { checked: th.id === theme, ...th } - ); - const themePopup = () => Dome.popupMenu(THEMES.map(themeItem), selectTheme); - // Component return ( <> <TitleBar> - <IconButton - icon="ZOOM.OUT" - onClick={zoomOut} - disabled={!theFunction} - title="Decrease font size" - /> - <IconButton - icon="ZOOM.IN" - onClick={zoomIn} - disabled={!theFunction} - title="Increase font size" - /> - <IconButton - icon="PAINTBRUSH" - onClick={themePopup} - title="Choose theme" - /> - <IconButton - icon="WRAPTEXT" - selected={wrapText} - onClick={flipWrapText} - title="Wrap text" - /> + {themeButtons} </TitleBar> <Text buffer={buffer} diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx index 8582d0b50059c08e706a4ab2498344040be99998..381801a671a094310e84572fdc6867e065ff7112 100644 --- a/ivette/src/renderer/Application.tsx +++ b/ivette/src/renderer/Application.tsx @@ -23,6 +23,7 @@ import Globals, { GlobalHint, useHints } from './Globals'; import Properties from './Properties'; import Locations from './Locations'; import Values from './Values'; +import SourceCode from './SourceCode'; // -------------------------------------------------------------------------- // --- Selection Controls @@ -129,6 +130,7 @@ export default (() => { <Group id="frama-c" label="Frama-C" title="Frama-C Kernel Components"> <Controller.Console /> <Properties /> + <SourceCode /> <ASTview /> <ASTinfo /> <Locations /> diff --git a/ivette/src/renderer/Locations.tsx b/ivette/src/renderer/Locations.tsx index 2e61bdd697411a6b6f018ab1083c1e2e0b2b1cd0..b0e3f6c197ada15e1e21c12657c0a839b2dc6a07 100644 --- a/ivette/src/renderer/Locations.tsx +++ b/ivette/src/renderer/Locations.tsx @@ -36,8 +36,8 @@ const LocationsTable = () => { (loc: string) => { const markerId = (loc as Json.key<'#markerInfo'>); const info = markersInfo.getData(markerId); - const source = info?.position; - const position = `${source?.base}:${source?.line}`; + const sloc = info?.sloc; + const position = `${sloc?.base}:${sloc?.line}`; return <Label label={position} title={info?.descr} />; }; diff --git a/ivette/src/renderer/Preferences.tsx b/ivette/src/renderer/Preferences.tsx index 02a7a602d3b8f3a9a2aa3149897ae10ee35e8bbe..c8c2c4f5720f86e10ac3250f800b530921af08c2 100644 --- a/ivette/src/renderer/Preferences.tsx +++ b/ivette/src/renderer/Preferences.tsx @@ -13,47 +13,169 @@ import React from 'react'; +import { popupMenu } from 'dome'; import * as Settings from 'dome/data/settings'; import * as Forms from 'dome/layout/forms'; +import { IconButton } from 'dome/controls/buttons'; -export const Theme = new Settings.GString('ASTview.theme', 'default'); -export const FontSize = new Settings.GNumber('ASTview.fontSize', 12); +import 'codemirror/mode/clike/clike'; +import 'codemirror/theme/ambiance.css'; +import 'codemirror/theme/solarized.css'; -const ASTviewPrefs = () => { +const THEMES = [ + { id: 'default', label: 'Default' }, + { id: 'ambiance', label: 'Ambiance' }, + { id: 'solarized light', label: 'Solarized Light' }, + { id: 'solarized dark', label: 'Solarized Dark' }, +]; +// -------------------------------------------------------------------------- +// --- AST View Preferences +// -------------------------------------------------------------------------- + +export const AstTheme = new Settings.GString('ASTview.theme', 'default'); +export const AstFontSize = new Settings.GNumber('ASTview.fontSize', 12); +export const AstWrapText = new Settings.GFalse('ASTview.wrapText'); + +export const SourceTheme = new Settings.GString('SourceCode.theme', 'default'); +export const SourceFontSize = new Settings.GNumber('SourceCode.fontSize', 12); +export const SourceWrapText = new Settings.GFalse('SourceCode.wrapText'); + +export interface ThemeProps { + target: string; + theme: Settings.GlobalSettings<string>; + fontSize: Settings.GlobalSettings<number>; + wrapText: Settings.GlobalSettings<boolean>; + disabled?: boolean; +} + +// -------------------------------------------------------------------------- +// --- Icon Buttons +// -------------------------------------------------------------------------- + +export interface ThemeControls { + buttons: React.ReactNode; + theme: string; + fontSize: number; + wrapText: boolean; +} + +export function useThemeButtons(props: ThemeProps): ThemeControls { + const [theme, setTheme] = Settings.useGlobalSettings(props.theme); + const [fontSize, setFontSize] = Settings.useGlobalSettings(props.fontSize); + const [wrapText, setWrapText] = Settings.useGlobalSettings(props.wrapText); + const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2); + const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2); + const flipWrapText = () => setWrapText(!wrapText); + const selectTheme = (id?: string) => id && setTheme(id); + const themeItem = (th: { id: string; label: string }) => ( + { checked: th.id === theme, ...th } + ); + const themePopup = () => popupMenu(THEMES.map(themeItem), selectTheme); + const { disabled = false } = props; + return { + theme, + fontSize, + wrapText, + buttons: [ + <IconButton + key="zoom.out" + icon="ZOOM.OUT" + onClick={zoomOut} + disabled={disabled} + title="Decrease font size" + />, + <IconButton + key="zoom.in" + icon="ZOOM.IN" + onClick={zoomIn} + disabled={disabled} + title="Increase font size" + />, + <IconButton + key="theme" + icon="PAINTBRUSH" + onClick={themePopup} + title="Choose theme" + />, + <IconButton + key="wrap" + icon="WRAPTEXT" + selected={wrapText} + onClick={flipWrapText} + title="Wrap text" + />, + ], + }; +} + +// -------------------------------------------------------------------------- +// --- Font Forms +// -------------------------------------------------------------------------- + +function ThemeFields(props: ThemeProps) { const theme = Forms.useDefined(Forms.useValid( - Settings.useGlobalSettings(Theme), + Settings.useGlobalSettings(props.theme), )); - const font = Forms.useValid( - Settings.useGlobalSettings(FontSize), + const fontsize = Forms.useValid( + Settings.useGlobalSettings(props.fontSize), ); - + const wraptext = Forms.useValid( + Settings.useGlobalSettings(props.wrapText), + ); + const options = THEMES.map(({ id, label }) => ( + <option key={id} value={id} label={label} /> + )); + const { target } = props; return ( - <Forms.Page> - <Forms.Section label="AST View" unfold> - <Forms.SelectField - state={theme} - label="Theme" - title="Set the color theme of the AST source code" - > - <option value="default" label="Default" /> - <option value="ambiance" label="Ambiance" /> - <option value="solarized light" label="Solarized light" /> - <option value="solarized dark" label="Solarized dark" /> - </Forms.SelectField> - <Forms.SliderField - state={font} - label="Font Size" - title="Set the font size of the AST source code" - min={8} - max={32} - step={2} - /> - </Forms.Section> - </Forms.Page> + <> + <Forms.SelectField + state={theme} + label="Theme" + title={`Set the color theme of ${target}`} + > + {options} + </Forms.SelectField> + <Forms.SliderField + state={fontsize} + label="Font Size" + title={`Set the font size of ${target}`} + min={8} + max={32} + step={2} + /> + <Forms.CheckboxField + state={wraptext} + label="Wrap Text" + title={`Set long line wrapping mode of ${target}`} + /> + </> ); -}; +} + +// -------------------------------------------------------------------------- +// --- Export Components +// -------------------------------------------------------------------------- export default (() => ( - <ASTviewPrefs /> + <Forms.Page> + <Forms.Section label="AST View" unfold> + <ThemeFields + target="Internal AST" + theme={AstTheme} + fontSize={AstFontSize} + wrapText={AstWrapText} + /> + </Forms.Section> + <Forms.Section label="Source View" unfold> + <ThemeFields + target="Source Code" + theme={SourceTheme} + fontSize={SourceFontSize} + wrapText={SourceWrapText} + /> + </Forms.Section> + </Forms.Page> )); + +// -------------------------------------------------------------------------- diff --git a/ivette/src/renderer/SourceCode.tsx b/ivette/src/renderer/SourceCode.tsx new file mode 100644 index 0000000000000000000000000000000000000000..0c9f8a7dfa42d7a626938d1fe10f5d24016c76a8 --- /dev/null +++ b/ivette/src/renderer/SourceCode.tsx @@ -0,0 +1,126 @@ +// -------------------------------------------------------------------------- +// --- Source Code +// -------------------------------------------------------------------------- + +import React from 'react'; +import * as States from 'frama-c/states'; + +import * as Dome from 'dome'; +import { readFile } from 'dome/system'; +import * as Json from 'dome/data/json'; +import { RichTextBuffer } from 'dome/text/buffers'; +import { Text } from 'dome/text/editors'; +import { Component, TitleBar } from 'frama-c/LabViews'; +import { functions, markerInfo } from 'frama-c/api/kernel/ast'; +import { source } from 'frama-c/api/kernel/services'; +import * as Preferences from './Preferences'; + +import 'codemirror/addon/selection/active-line'; +import 'codemirror/addon/dialog/dialog.css'; +import 'codemirror/addon/dialog/dialog'; +import 'codemirror/addon/search/searchcursor'; +import 'codemirror/addon/search/search'; +import 'codemirror/addon/search/jump-to-line'; + +// -------------------------------------------------------------------------- +// --- Pretty Printing (Browser Console) +// -------------------------------------------------------------------------- + +const D = new Dome.Debug('Source Code'); + +// -------------------------------------------------------------------------- +// --- Source Code Printer +// -------------------------------------------------------------------------- + +const SourceCode = () => { + + // Hooks + const buffer = React.useMemo(() => new RichTextBuffer(), []); + const [selection] = States.useSelection(); + const theFunction = selection?.current?.function; + const theMarker = selection?.current?.marker; + const { buttons: themeButtons, theme, fontSize, wrapText } = + Preferences.useThemeButtons({ + target: 'Source Code', + theme: Preferences.SourceTheme, + fontSize: Preferences.SourceFontSize, + wrapText: Preferences.AstWrapText, + disabled: !theFunction, + }); + + const markersInfo = States.useSyncArray(markerInfo); + const functionsData = States.useSyncArray(functions).getArray(); + + const currentFile = React.useRef<string>(); + + React.useEffect(() => { + // Async source file loading and jump to line/location. + async function loadSourceCode(sloc?: source) { + if (sloc) { + const { file, line } = sloc; + try { + if (file !== currentFile.current) { + currentFile.current = file; + const content = await readFile(file); + buffer.setValue(content); + } + buffer.forEach((cm) => { cm.setCursor(line - 1); }); + } catch (err) { + D.error(`Fail to load source code file ${file}.`); + } + } + } + // Actual source code loading upon function or marker update. + const sloc = + /* Non-empty [selection] has defined either marker or function: we give + precedence to marker as it provides more precise source location. */ + (theMarker && + markersInfo.getData(theMarker as Json.key<'#markerInfo'>)?.sloc) + ?? + (theFunction && functionsData.find((e) => e.name === theFunction)?.sloc); + if (sloc) { + loadSourceCode(sloc); + } else { + currentFile.current = undefined; + buffer.clear(); + } + }, [buffer, functionsData, markersInfo, theFunction, theMarker]); + + // Component + return ( + <> + <TitleBar> + {themeButtons} + </TitleBar> + <Text + buffer={buffer} + mode="text/x-csrc" + theme={theme} + fontSize={fontSize} + lineWrapping={wrapText} + selection={theMarker} + lineNumbers={!!theFunction} + styleActiveLine={!!theFunction} + extraKeys={{ 'Alt-F': 'findPersistent' }} + readOnly + /> + </> + ); + +}; + +// -------------------------------------------------------------------------- +// --- Export Component +// -------------------------------------------------------------------------- + +export default () => ( + <Component + id="frama-c.sourcecode" + label="Source Code" + title="Original source code" + > + <SourceCode /> + </Component> +); + +// -------------------------------------------------------------------------- diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index a3fe97c94e4ac970d3f3c228715d63eee5af6714..264360c8f4b89cb86fd44d9d7924c701110ccbcb 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -196,8 +196,8 @@ struct in let () = States.column - ~name:"position" - ~descr:(Md.plain "Marker position") + ~name:"sloc" + ~descr:(Md.plain "Source location") ~data:(module Kernel_main.LogSource) ~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag)) model @@ -450,6 +450,11 @@ struct ~data:(module Data.Jbool) ~default:false ~get:is_eva_analyzed; + States.column model + ~name:"sloc" + ~descr:(Md.plain "Source location") + ~data:(module Kernel_main.LogSource) + ~get:(fun kf -> fst (Kernel_function.get_location kf)); States.register_array model ~package ~key ~name:"functions" diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml index e3c92e75a42f4a775c52c41233fe388559f4dfe2..f57033cb1366c7c76c3e10849634fd9e213c2261 100644 --- a/src/plugins/server/kernel_main.ml +++ b/src/plugins/server/kernel_main.ml @@ -90,10 +90,15 @@ struct let to_json p = let path = Filepath.(Normalized.to_pretty_string p.pos_path) in + let file = + if Server_parameters.has_relative_filepath () + then path + else (p.Filepath.pos_path :> string) + in `Assoc [ "dir" , `String (Filename.dirname path) ; "base" , `String (Filename.basename path) ; - "file" , `String (p.Filepath.pos_path :> string) ; + "file" , `String file ; "line" , `Int p.Filepath.pos_lnum ; ] diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml index be9b5da15c6ad6f271c9bd6cb764422eee3f0cfa..74a07c43b7f08e171044e3fd0c8c0c1d8a98adff 100644 --- a/src/plugins/server/server_parameters.ml +++ b/src/plugins/server/server_parameters.ml @@ -73,3 +73,10 @@ let wkind = register_warn_category "inconsistent-kind" let wname = register_warn_category "invalid-name" (* -------------------------------------------------------------------------- *) +(* --- Filepath Normalization --- *) +(* -------------------------------------------------------------------------- *) + +let use_relative_filepath = register_category "use-relative-filepath" +let has_relative_filepath () = is_debug_key_enabled use_relative_filepath + +(* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli index af8c6dea9d1aa600df8d3cf09bf5fd74a9a4db6c..ba41ba164c75e313f8a74a78dd710e1e5273d704 100644 --- a/src/plugins/server/server_parameters.mli +++ b/src/plugins/server/server_parameters.mli @@ -32,4 +32,6 @@ val wpage : warn_category (** Inconsistent page warning *) val wkind : warn_category (** Inconsistent category warning *) val wname : warn_category (** Invalid name warning *) +val has_relative_filepath: unit -> bool + (**************************************************************************) diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json index 3dc3730f8f4b2707777bde129a6916dcb1f94d84..a6223032cf20850343a7d0270679a14b24daee0b 100644 --- a/src/plugins/server/tests/batch/oracle/ast_services.out.json +++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json @@ -7,13 +7,25 @@ "key": "kf#24", "name": "g", "signature": "int g(int y);", - "defined": true + "defined": true, + "sloc": { + "dir": "tests/batch", + "base": "ast_services.i", + "file": "tests/batch/ast_services.i", + "line": 2 + } }, { "key": "kf#20", "name": "f", "signature": "int f(int x);", - "defined": true + "defined": true, + "sloc": { + "dir": "tests/batch", + "base": "ast_services.i", + "file": "tests/batch/ast_services.i", + "line": 1 + } } ], "removed": [], diff --git a/src/plugins/server/tests/batch/test_config b/src/plugins/server/tests/batch/test_config index 15a16cd4f95d4ced405bb04b6a13382efcd47e7f..4addf96dff82842ab79ae170fda242244765a7c0 100644 --- a/src/plugins/server/tests/batch/test_config +++ b/src/plugins/server/tests/batch/test_config @@ -1,2 +1,2 @@ LOG: @PTEST_NAME@.out.json -OPT: -no-autoload-plugins -load-module server -check -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ +OPT: -no-autoload-plugins -load-module server -check -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ -server-msg-key use-relative-filepath